This issue tracker is closed. Please visit UPPAAL issue tracker at Github instead.

Bug 527

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

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.