// Place global declarations here.ClockGuardTemplate// Place local declarations here.
clock a;L2L1L0UrgentIntialTemplate// Place local declarations here.
clock a;L2L1L0// Place template instantiations here.
UrgentIntial = UrgentIntialTemplate();
ClockGuard = ClockGuardTemplate();
// List one or more processes to be composed into a system.
system UrgentIntial, ClockGuard;
E<> ClockGuard.L2
It is possible to get to the L2 location, even though there is an edge restricting L0 to reach L1 if time is greater than 1, and L1 have an invariant only allowing time to be larger than 2.
E<> UrgentIntial.L2
It is possible to get to the L2 location, even though no time should be allowed to pass in L0, and L1 requires time to have been passed.