Die Teile - h1 und - r1.~contains in
|
all h1 : HierarchicalStates | let n1 = h1.contains | all h2 : HistoryNodes & n1 | |
|
no (Flows <: from).h2 and h2 in (Flows <: from).(Nodes - h1 - n1).to |
|
implies one (StartNodes & n1) |
|
all r1 : Regions | let n1 = r1.contains | all h1 : HistoryNodes & n1 | |
|
no (Flows <: from).h1 and h1 in (Flows <: from).(Nodes - r1.~contains - n1).to |
|
implies one (StartNodes & n1) |
sind vielleicht überflüssig.
Denn es kann sein, dass selbst ohne sie kein Unterschied hinsichtlich der beschriebenen Diagramme entsteht, da insbesondere wegen anderer Erreichbarkeitsforderungen die relevanten Fälle anderweitig ausscheiden.
Und insbesondere der - r1.~contains Teil scheint zu einer recht deutlichen Verlängerung der Instanzsuche zu sorgen (in einer leichten Variation des radioClock Beispiels, die den Effekt genau dieses Ausschlusses zu provozieren versuchte).
Die Teile
- h1und- r1.~containsinsd-generate/alloy/sd/reachability_rules.als
Lines 52 to 57 in 5f4dc64
Denn es kann sein, dass selbst ohne sie kein Unterschied hinsichtlich der beschriebenen Diagramme entsteht, da insbesondere wegen anderer Erreichbarkeitsforderungen die relevanten Fälle anderweitig ausscheiden.
Und insbesondere der
- r1.~containsTeil scheint zu einer recht deutlichen Verlängerung der Instanzsuche zu sorgen (in einer leichten Variation desradioClockBeispiels, die den Effekt genau dieses Ausschlusses zu provozieren versuchte).