search

juodaspaulius / clafer

Clafer is a lightweight modeling language
http://clafer.org
MIT License
0 stars 1 forks source link

testcase: (tmp_TrafficLight,cfr) #18

Open RaoMukkamala opened 9 years ago

RaoMukkamala commented 9 years ago

The following part of the traffic light example fails to generate an instance.

xor TrafficLight_4 1
   xor on
      normal
      flashing
   off
   [initially off]
   // a constraint that 'remembers' that we left from normal
   [G (on.normal && X !on) => X(!on W on.normal)]  // (*)
   // a constraint that 'remembers' that we left from flashing
   [G (on.flashing && X !on) => X(!on W on.flashing)]

It compiles correctly in alloy analyser, but fails to generate an instance.