Ist there some way to query markings without a successor?

Asked by Falk Benke on 2013-03-06

I would like to find out, if there are cases, where no more transitions can be fired. Is that possible somehow?
Even an indirect approach via UPPAAL is fine.

Question information

Language:
English Edit question
Status:
Answered
For:
TAPAAL Edit question
Assignee:
No assignee Edit question
Last query:
2013-03-06
Last reply:
2013-09-10
Jiri Srba (srba) said : #1

Thanks for the question. I guess that what you want is to find out is if there are deadlocks in your net, meaning
that you reach a marking from which (after some delay) there are no more enabled transitions. At the moment,
we do not support deadlock-check in TAPAAL but it is pretty high on todo list. In the meantime, you can use
in the query dialog "Export to UPPAAL XML", open the exported xml file in UPPAAL GUI and ask the question:

E<> deadlock

It is very important you choose one of the Broadcast translations to UPPAAL. The other two translations
introduce new deadlocks into the model that were not there before.

I hope we will be able to support deadlocks directly in some of the future releases.

Jiri Srba (srba) said : #2

We are happy to announce a new release 2.4.0 that now supports the deadlock propostion.
Please, take a look at www.tapaal.net and let us know if something is unclear.

Can you help with this problem?

Provide an answer of your own, or ask Falk Benke for more information if necessary.

To post a message you must log in.