# MODEL: Minimal one-agent timedCGS for TCTL and TOL smoke tests

# PURPOSE: Two states, one clock, self-loop and edge to s1.

# LOGIC: TCTL, TOL

Transition
* 0
0 *
Name_State
s0 s1
Initial_State
s0
Atomic_propositions
p
Labelling
1
0
Number_of_agents
1
Clocks
x
Clock_constraints
x<=1
x<=1
Invariants
x<=2
x<=2
