search

juodaspaulius / clafer

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

Power Window Total (tmp_powerwindow_total.cfr) #13

Open RaoMukkamala opened 9 years ago

RaoMukkamala commented 9 years ago

Failed to compile Power Window Total transitions model: Please take a look at the model which is committed to repository under positive folder or you can also find at: Power Window Total. The following are the error messages, when it tried to compile using clafer LTL compiler.

  1. Error 1: The following let constraint failed to compile:

[no (req, endOfTravel, objectDetected) => (let oldState = State | next (State = oldState))]

Error message: Parse failed at line 77 column 69... syntax error at line 77 before | next ( State [Finished in 0.0s with exit code 1] [cmd: ['/home/clafertools/.config/sublime-text-3/Packages/Clafer Tools/clafer', '/home/clafertools/behavioral-0.4.0/clafer/test/positive/tmp_powerwindow_total.cfr', '-m=alloyltl', '-m=clafer', '-m=html', '--add-comments', '--self-contained']] [dir: /home/clafertools/behavioral-0.4.0/clafer/test/positive] [path: .:/opt/ghc/7.8.3/bin:/opt/cabal/1.20/bin:/home/clafertools/.cabal/bin:/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin:/usr/games:/usr/local/games]

  1. Error 2: The following constraint fails to compile

[ (req=down || no req) => always (movingDown until endOfTravel) ]

Error message: Parse failed at line 112 column 39... syntax error at line 112 before always ( movingDown until [Finished in 0.0s with exit code 1] [cmd: ['/home/clafertools/.config/sublime-text-3/Packages/Clafer Tools/clafer', '/home/clafertools/behavioral-0.4.0/clafer/test/positive/tmp_powerwindow_total.cfr', '-m=alloyltl', '-m=clafer', '-m=html', '--add-comments', '--self-contained']] [dir: /home/clafertools/behavioral-0.4.0/clafer/test/positive] [path: .:/opt/ghc/7.8.3/bin:/opt/cabal/1.20/bin:/home/clafertools/.cabal/bin:/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin:/usr/games:/usr/local/games]

However, the same constraint compiles if we change always to G like the following.

[ (req=down || no req) => G (movingDown until endOfTravel) ]

  1. Error 3: Finally if we comment the above two error constraints lines, we get the following error:

clafer: AlloyLtl.genPExp': No pattern match for IClaferId {_modName = "", _sident = "ref", _isTop = True, _binding = Nothing} [Finished in 0.4s with exit code 1] [cmd: ['/home/clafertools/.config/sublime-text-3/Packages/Clafer Tools/clafer', '/home/clafertools/behavioral-0.4.0/clafer/test/positive/tmp_powerwindow_total.cfr', '-m=alloyltl', '-m=clafer', '-m=html', '--add-comments', '--self-contained']] [dir: /home/clafertools/behavioral-0.4.0/clafer/test/positive] [path: .:/opt/ghc/7.8.3/bin:/opt/cabal/1.20/bin:/home/clafertools/.cabal/bin:/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin:/usr/games:/usr/local/games]

mantkiew commented 7 years ago

As of Jan 10, 2017, Error 3 no longer appears; however, Errors 1 & 2 still occur.