Bug 527 - Same model but different result
Summary: Same model but different result
Alias: None
Product: UPPAAL
Classification: Unclassified
Component: Engine (show other bugs)
Version: 4.1.4
Hardware: PC Windows XP
: P2 normal
Assignee: Marius Mikučionis
Depends on:
Reported: 2011-09-30 13:43 CEST by truongkhanhit
Modified: 2019-11-25 12:01 CET (History)
1 user (show)

See Also:


Note You need to log in before you can comment on or make changes to this bug.
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.