eventually pattern (tmp_eventually04.cfr)

juodaspaulius / clafer

Clafer is a lightweight modeling language

http://clafer.org

MIT License

0 stars 1 forks source link

eventually pattern (tmp_eventually04.cfr) #17

Open RaoMukkamala opened 9 years ago

RaoMukkamala commented 9 years ago

The following models compiles, desugars correctly, but failed to generate a valid instance.

xor a
   b 
   c 
   [b => eventually c]
assert[always (a.b => eventually a.c)]

I tried many times, but I get the following message and no valid instance can be generated.

Executing "Check assertOnLine_8 for 10"
Solver=minisat(jni) Bitwidth=0 MaxSeq=0 SkolemDepth=1 Symmetry=20
51855 vars. 2230 primary vars. 62664 clauses. 130ms.
No counterexample found. Assertion may be valid. 7ms.

wasowski commented 9 years ago

Now "make test" hangs for me on this input; have no idea why; it also starts up Alloy GUI unlike other test-cases. I am still too lost in the code to see why it is doing that.