Modeling 2 threads using UPPAAL

92 Views Asked by At

Pseudo code that I am trying to model (has 2 threads) :-

sleep_time = 10;
deadline_time = 2;

main thread :-

while(true){
write(); // function is defined.
sleep(sleep_time);
}

thread-2 :-

while(true){
if(write function is called every 2 (deadline_time) secs){
} 
else {
callback_function();
}
}

Below are the automaton that I have built (and it's satisfying both the cases where when sleep_time > deadline_time I move to unsafe_state otherwise I never move to unsafe_state), but the issue I am facing I am not faithful to the actual code.

I am making use of the channel synchronization which kind of feels like I established some kind dependency between the 2 threads but in the actual code there is no such thing. I want to model it without creating this dependency (not using channel synchronization between them).

Edit :-

Automata for main-thread :- enter image description here

Automata for thread-2 :- enter image description here

Declarations :-

enter image description here

0

There are 0 best solutions below