TAPAAL

Broken trace visualization after verification

Bug #354781 reported by Jiri Srba on 2009-04-03

Affects		Status	Importance	Assigned to	Milestone
	TAPAAL	Fix Released	High	Kenneth Yrke Jørgensen	TAPAAL 1.1

Bug Description

Open the attached file and click "Verify" on the query "Three in Garbage". It should return a trace that will place three tokens into Garbage place, but the trace it too short and moreoever it cannot be simulated (step forward) in the simulator.

Revision history for this message

Jiri Srba (srba) wrote on 2009-04-03:

producer-consumer.xml Edit (9.5 KiB, text/xml)

Changed in tapn:
importance:	Undecided → High
milestone:	none → version1.5

Revision history for this message

Kenneth Yrke Jørgensen (yrke) wrote on 2009-04-04:

I just had a quick look on this problem, and it seems like that by some reason verifyta returns an abstract trace instead of an concrete. This issue will need further investigation.

Changed in tapn:
assignee:	nobody → yrke
status:	New → Confirmed

Revision history for this message

Kenneth Yrke Jørgensen (yrke) wrote on 2009-04-04:

It seems that the problem with concrete trace in verifyta is dependent on the E[] property.

Kenneth Yrke Jørgensen (yrke) on 2009-04-08

Changed in tapn:
status:	Confirmed → In Progress

Revision history for this message

Kenneth Yrke Jørgensen (yrke) wrote on 2009-04-13:

I just had a quick word with the Uppaal team, and verifyta does not offer a concrete trace when verifyring E[] propertis, (known bug) This might be implemented in future version of verifyta, but for now then uppaal team does not have time to fix the issue.

Kenneth Yrke Jørgensen (yrke) on 2009-04-17