TAPAAL

Boundedness Checking Broken Again

Bug #816113 reported by Jiri Srba on 2011-07-25

This bug affects 1 person

	Status	Importance	Assigned to	Milestone
TAPAAL	Fix Released	Critical	Unassigned
2.0	Fix Released	Critical	Unassigned	TAPAAL 2.0.1
VerifyTAPN	Invalid	Critical	Unassigned	VerifyTAPN 1.2
1.0	Invalid	Critical	Unassigned	VerifyTAPN 1.0.1

Bug Description

Open the attached net, open the query, click on boundedness check. It returns as we need -4 extra tokens.

Related branches

lp:tapaal

Revision history for this message

Jiri Srba (srba) wrote on 2011-07-25:

error-in-boundedness-check.xml Edit (78.1 KiB, text/xml)

Changed in verifytapn:
importance:	Undecided → Critical
milestone:	none → 1.1

Revision history for this message

Jiri Srba (srba) wrote on 2011-07-25:

After little bit more investigation, the problem seems to be related to the fact that in the GUI some of the components
are disabled, after removing them it seems that it is working well, so the problem is probably related to the fact
that the disabled components have some tokens in the initial marking.

Revision history for this message

Morten Jacobsen (mortenja) wrote on 2011-08-01:

I fixed the bug in the GUI. However there seems to be an issue in the engine as well (though not affecting this particular bug), so I will post a separate bug for it.