GaloisInc / salty

A DSL for generating GR(1) problems
BSD 3-Clause "New" or "Revised" License
11 stars 3 forks source link

Panic Error when using formula of the form (x == 0) -> (x' == 1) #11

Closed sahabi closed 7 years ago

sahabi commented 7 years ago

I get the below error whenever I try to synthesize a controller using a formula of the form (x == 0) -> (x' == 1), where x is an Int. The problem it seems to be coming from the use of x', if I have a formula of the form (x == 0) -> (y == 1) there will be no problem.

salty: PANIC(mkAssign): Invalid arguments to assign: (EApp (EPrim (PNext TInt)) (EVar TInt (Name {nText = "x", nUnique = 2, nOrigin = FromDecl (Range {rangeSource = Just "slugs_input.salt", rangeStart = Position {posRow = 9, posCol = 8}, rangeEnd = Position {posRow = 9, posCol = 9}}) (Name {nText = "Visgame", nUnique = 0, nOrigin = FromController (Range {rangeSource = Just "slugs_input.salt", rangeStart = Position {posRow = 1, posCol = 12}, rangeEnd = Position {posRow = 16, posCol = 9}}), nOutName = Nothing}), nOutName = Nothing})),ENum 0)