Bug 527

Summary: Same model but different result
Product: UPPAAL Reporter: truongkhanhit
Component: EngineAssignee: Marius Mikučionis <marius>
Severity: normal CC: marius
Priority: P2    
Version: 4.1.4   
Hardware: PC   
OS: Windows XP   

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.