search

AlloyTools / org.alloytools.alloy

Alloy is a language for describing structures and a tool for exploring them. It has been used in a wide range of applications from finding holes in security mechanisms to designing telephone switching networks. This repository contains the code for the tool.
Other
696 stars 124 forks source link

Inconsistent results between Alloy 5 and Alloy 5.1 (related to int-usage assumptions) #123

Closed gregistecco closed 2 years ago

gregistecco commented 3 years ago

There is a problem with some commands wrongly reporting an unsatisfiable result. The results are inconsistent with previous versions of Alloy 5. For instance, the model attached should find pred test1 to be satisfiable, but the command:

run test1 expect 1

gives an unsatisfiable outcome. It reports “0 vars. 0 primary vars. 0 clauses”.

I think the problem has to do with the use of integers. A potential fix is changing line:

boolean shouldUseInts = true; // TODO CompUtil.areIntsUsed(sigs, cmd);(https://github.com/AlloyTools/org.alloytools.alloy/blob/ee124f9d782e04493a4171b7e06842e2a4c5070e/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/translator/ScopeComputer.java#L351)

by boolean shouldUseInts = CompUtil.areIntsUsed(sigs,cmd);

(Notice that CompUtil should also be imported) import edu.mit.csail.sdg.parser.CompUtil;

module unknown sig Node { adj: (set Node) } pred noLoops[] { (adj = (iden - (Node->Node))) }

pred test1 { some disj Node1, Node2 : Node | {
Node = (Node1 + Node2) no adj noLoops[] } } run test1 expect 1

pkriens commented 2 years ago

Could you try this out in the latest 6.0 release and re-open this big if it still fails?