@startuml
hide footbox

box "Checker Process" #LightBlue
	participant Checker
end box

box "Application Process" #LightBlue
	participant Maestro
	participant Actor1
	participant Actor2 
end box

activate Checker
[-> Checker
Checker -> Maestro : Start Scheduling Round
deactivate Checker
activate Maestro

Maestro -> Actor1 : . schedule
deactivate Maestro

activate Actor1
Actor1 -> Maestro : simcall
deactivate Actor1

activate Maestro
Maestro -> Actor2 : . schedule
deactivate Maestro

activate Actor2
Actor2 -> Maestro : simcall
deactivate Actor2

activate Maestro
Maestro -> Checker : Scheduling round is over
deactivate Maestro
activate Checker

Checker o<[#red]-o Maestro : Take a system-level checkpoint

Checker -> Maestro : tell me about the existing transitions/simcalls
Maestro -> Checker : enabled or not, visible or not, dependency informations

note right of Checker : Checker algo decides which transition to fire first

Checker -> Maestro : . Execute that transition; start next scheduling round
deactivate Checker
activate Maestro
Maestro -> Actor1 : schedule
deactivate Maestro


...Repeat until the Application terminates (until the current execution path reaches its end)...

Maestro -> Checker : Application is over
activate Checker
note right of Checker : Checker algo decides which transition to fire next
Checker o-[#red]>o Maestro : Restore system image from previous checkpoint
Checker -> Maestro : . Execute that transition; start next scheduling round
deactivate Checker

...Repeat until all execution paths have been explored...

@enduml