|Summary:||Same model but different result|
|Component:||Engine||Assignee:||Marius Mikučionis <marius>|
Description truongkhanhit 2011-09-30 13:43:10 CEST
I have a model and I do the liveness checking then the result is Satisfied. Then I just remove the guard of a transition which is, to me, always True. Then the result is unsatisfied.
Comment 1 Marius Mikučionis 2019-11-15 10:33:09 CET
I need more information on how to replicate the issue. From the description I could just speculate that maybe it is an expected behavior, i.e. maybe the guarded edge leads to a location where infinite delay is possible, and thus is a counteraxmple that the target predicate is no longer satisfiable. Please upload a model or a minimal example. Alternatively, could you try it with newer release? Perhaps the issue has been fixed already.
Comment 2 Marius Mikučionis 2019-11-25 12:01:50 CET
I am marking this as invalid, feel free to reopen with new information.