# Testing multiple "diagonal" clock resets
# When using edges of the type used in (CASE 1), the model does not compile
# which is okish as this prevents incorrect behaviour
# (CASE 2) shows inconsistent behaviour

system:testresets

clock:1:x
clock:1:y
clock:1:z
event:none

process:P0
location:P0:LI{initial:}
location:P0:L0
location:P0:L1{invariant: x<=1 && x>=1 && y<=1 && y>=1 && z<=2 && z>=2 : labels: goal}

edge:P0:LI:L0:none{do:x=0; y=1; z=2}

# (CASE 1)
#edge:P0:L0:L1:none{provided:x<=0 && x>=0 && y<=3 && y>=3 : do : y=x+1; z=y+1} # System compilation failure ok I guess

# (CASE 2)
# Once the guard applied, the zone is the singleton (x=1, y=2, z=3)
# Applying the resets should give (x'=x=1, y'=x=1, z'=y=2)
# but it gives
# (x'=x=1, y'=x'=1, z'=y'=x'=1)
# As the resets are applied sequentially
edge:P0:L0:L1:none{provided:x<=1 && x>=1 && y<=2 && y>=2 && z<=3 && z>=3 : do : y=x; z=y} # No error, but incorrect behaviour