Verification (translation) to UPPAAL fails

[Jiri Srba]

Open the attached Net with a query and run the verification. It fails to give any output and std output says:

There was an error verifying the model.

[Kenneth Yrke Jørgensen (yrke)]

This is a problem with the usage of * in the names. * is not allowed as an identifier in uppaal

[Kenneth Yrke Jørgensen (yrke)]

This problem has also been traced back to an logical error in the reduction code.
All problems is now corrected

[Jiri Srba (srba)]

Just run Fisher on the new code and advanced+sym gives:

The new way 2Transition Exit3
The new way 2Transition Exit1
The new way 1!! Transition Enter
Hmmm wtf? error point 25659852
The new way 2Transition Choose2A

and the error point is in red.

Jiri

> This problem has also been traced back to an logical error in the reduction code.
> All problems is now corrected
>
> ** Changed in: tapn
> Assignee: Joakim Byg (joakim-byg) => Kenneth Yrke Joergensen (yrke)
> Status: New => Fix Committed
>
> --
> Verification (translation) to UPPAAL fails
> https://bugs.launchpad.net/bugs/342766
> You received this bug notification because you are a member of TAPAAL
> Developers, which is the registrant for TAPAAL.
>
> Status in TAPAAL: Fix Committed
>
> Bug description:
> Open the attached Net with a query and run the verification. It fails to give any output and std output says:
>
> There was an error verifying the model.
>

---
Jiri Srba, <email address hidden>
Associate Professor at Aalborg University, Denmark
Dep. of Computer Science, Selma Lagerlofs Vej 300, 9220 Aalborg
http://www.brics.dk/~srba/
office phone: [phone]
mobile: [phone] or [phone]
fax: [phone]
---