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 :-
Declarations :-