UPPAAL - force transition with synchro doesn't work
Totally stuck on it.
Basically, I have heater, temp sensor and process that simulates rise of temperature.
I want heater to transite to "disabled" state when temp is above some value. It can be synchronised with transition to abnormal temp state.
But in simulation I can only get possibility to make transition when condition is true.
heater:
temp riser:
sensor:
I tried to add synchro for it like that:
sensor:
heater:
But since it can't change state in automatic mode, the synchro also doesn't work...
How can I make it?
A quick fix specific to this case:
Declare the disable_heater as urgent and will not allow delay option.
In general this solution is not a good design. The issue is that your model uses asynchronous communication through variables, which introduces many more states and makes it hard to verify. A better option is to use synchronous communication. You are already on your way by using the disable_heater, but you also need to synchronize with temp riser through channel, eg temp_update!. You will need to synchronize multiple processes so you either link them through urgent or committed location, or use broadcast channel (one sender multiple receivers).
Please see Uppaal Tutorial section on value communication.
- Do I need to synchronize writes to memory mapped file from different threads before flushing and unmapping it?
- How to wait (vkCmdWaitEvents) 2 different events most efficiently in one cmd buffer?
- Best practice for synchronizing a changing List of the model to a ObservableList of the ViewModel?
- UWP: how to optimize synchronization between WCF WebServices and SQLite through async calls
- When does windows signal a process handle?
- Best way to synchronize my code between multiple workstations?
- requestAnimationFrame() animation of multiple objects sync problem
- Why use a ReentrantLock if one can use synchronized(this)?
- Is multi-thread output from System.out.println interleaved
- How can I synchronize asyncio with other OS threads?
- Drawing from multiple threads in Qt
- Why we have to add an 'async' declaration word to the javascript function which call a sync javascript function?
- CUDA: how to use barrier.sync
- What is the synchronization cost of calling a synchronized method from a synchronized method?
- How to sync a local folder with a folder in a Google Cloud Platform bucket?
- linux/ubuntu batch scripts with FreeFileSync
- How do I update or sync a forked repository on GitHub?
- How to wait until a predicate condition becomes true in JavaScript?
- Why isn't calling wait(), notify() or notifyAll() without a synchronized block not a compiler error?
- Why can't I use the 'await' operator within the body of a lock statement?
- Interval synced to Time
- Android Studio how to run gradle sync manually?
- What are atomic operations for newbies?
- Alternative to Lock.tryLock() in Java 1.4
- How Do I Queue My Python Locks?
- In Swift Structured Concurrency, how are Actors synchronized?
- Two independent Blazor tasks, pause one until the other completes
- How to keep two folders automatically synchronized?
- Mutex example / tutorial?
- What problems might arise from ignoring this race condition?