Understanding Urgent Channels in Uppaal
I have three automata (see below), the single global declaration urgent chan u; and the system declaration system UrgentChannel, P1, P2;. My understanding is that by making u an urgent channel, the transition from start to goal has to be taken.
I would like to understand why the property P1.start --> P1.goal is not satisfied. The counter example from the simulator does not seem to help here.
The model for download is here. Thanks for reading!
- P1:
- P2:
- UrgentChannel:
The counter example (the diagnostic trace) in simulator has a tail marked in red, which means that it is repeated infinitely (P2 can perform zeno loop). Basically, Uppaal is trying to tell that there exist an infinit loop which may prevent the urgent transition from reaching the goal state.
If you remove the process P2, then the property holds.
If you are concerned with liveness properties, then such zeno loops are not desirable hence Uppaal rightly reports them as a counter example.
- How to cast a double value to a integer value in UPPAAL?
- UPPAAL - force transition with synchro doesn't work
- What is the difference between Symbolic and Concrete model checking when the search is bounded in time?
- Uppaal - How to force a transition when a condition becomes true?
- UPPAAL: ModelDemo for Java API (Error while getting memory info: 34, javax.xml.stream.XMLStreamException: ParseError at [row,col]:[1,3])
- Uppaal : Is there a way to know the size of the state space?
- Trace format from verifyta not compatible with tracer utility of libutap library
- Declaration of multiple processes from the same Template in Uppaal
- how to convert double values to integer with int fint (double) without getting 'Server connection lost' in Uppaal
- How to save variables from Uppaal created during the modeling process
- Can't find what could cause the "caused by an out-of-range assignment or out-of-range array lookup." error
- UPPAAL SMC motivating example
- Array Initialization In Uppaal
- Understanding Urgent Channels in Uppaal
- What if Uppaal removes relative time?
- UPPAAL SMC avoid State Space Explosion
- can you decalare a json array in uppaal?
- Uppaal Verification not working as intended
- Simple basic verification problem in uppal
- How to return an array in UPPAAL?
- Is there a terminating state in UPPAAL?
- UPPAAL deadlock unclear
- UPPAAL: Do clocks given as function parameters have methods or attributes?
- UPPAAL: Checking member of array
- Channel Declaration in UPPAAL
- System contains deadlock - how to find it? (UPPAAL)
- UPPAAL: What cause clock to stop running
- How to select array of integers in UPPAAL?
- promela/spin vs uppaal pros and cons for embedded modelling