Two Process Race
There are two processes, main and int.
The process main increments a counter count
as long as a Boolean flag flag is false.
The process int's only task is to set flag to true.
When flag is true the process main decrements count
until it reaches 0 and then jumps to its final state.
The process main performs its actions once
every [l1, l2] time units.
The process int has an upper bound of l for its task.
Problem 1
Model this system using timed automata / Uppaal.
Problem 2
Derive an upper bound on the time it takes before main reaches its
final state, validate your result for some instances using Uppaal.