search

VerifiableRobotics / slugs

SmalL bUt Complete GROne Synthesizer
Other
37 stars 25 forks source link

Counterstrategy synthesis doesn't work properly for "transition" liveness conditions #10

Closed vraman closed 9 years ago

vraman commented 9 years ago

See the following example:

[INPUT] ball cat

[OUTPUT] bit0

[ENV_TRANS] | ! cat' ! ball'

[ENV_LIVENESS] 1

[ENV_INIT] 1

[SYS_TRANS] | ! ball' ! bit0' | ! cat' ! ! bit0'

[SYS_LIVENESS] bit0' ! bit0'

[SYS_INIT] ! bit0

The counterstrategy synthesized does not prevent the goals. However, changing the goals to "current" time step fixes the problem and the counterstrategy is correct.