Alliage - Traitement de quantificateurs universels illimités

Question

Bon après-midi,

J'ai rencontré un problème avec Alloy lorsque je traitais des quantificateurs universels non bornés. Comme expliqué dans le livre 'Software Abstractions' de Daniel Jackson (Section 5.3 'Unbounded Universal Quantifiers'), Alloy a une limitation subtile concernant les quantificateurs universels et la vérification des assertions. Alliage produit des contre-parasites dans certains cas, comme la suivante pour vérifier que les ensembles sont fermés par union (montré dans le livre mentionné ci-dessus):

sig Set { 
    elements: set Element 
} 
sig Element {} 

assert Closed { 
    all s0, s1: Set | some s2: Set | 
    s2.elements = s0.elements + s1.elements 
} 
check Closed for 3 

La production d'un contre-exemple:

Set = {(S0),(S1)} 
Element = {(E0),(E1)} 
s0 = {(S0)} 
s1 = {(S1)} 
elements = {(S0,E0), (S1,E1)} 

où l'analyseur n'a pas peuplé Set avec suffisamment de valeurs (un atome Set absent, S2, contenant l'union de S0 et S1).

Deux solutions à ce problème général sont alors suggéré dans le livre:

1) Déclarer un axiome de générateur de force en alliage pour générer tous les cas possibles. Par exemple:

fact SetGenerator{ 
    some s: Set | no s.elements 
    all s: Set, e: Element | 
    some s': Set | s'.elements = s.elements + e 
} 

Cette solution, cependant, produit une explosion de portée et peut également conduire à des incohérences.

2) Omettre l'axiome du générateur et utiliser la forme bornée universelle pour les contraintes. Autrement dit, l'expression englobante de la variable quantifiée ne mentionne pas les noms des signatures générées. Cependant, toutes les assertions ne peuvent pas être exprimées sous une telle forme.

Ma question est: existe-t-il une règle spécifique pour choisir l'une de ces solutions? Ce n'est pas clair pour moi du livre.

Merci.

Answer 1

Non, il n'y a pas de règle spécifique (ou du moins aucune que j'ai trouvée). En pratique, cela ne se produit pas très souvent, alors je traiterais chaque cas au fur et à mesure. Avez-vous un exemple en tête? Notez également que vous pouvez parfois formuler votre problème avec un quantificateur d'ordre supérieur (par exemple, un quantificateur sur un ensemble ou une relation). Dans ce cas, vous pouvez utiliser Alloy *, une extension d'Alloy qui prend en charge l'analyse d'ordre supérieur. .