-- RESET PETRI NET
-- MP 22/11/2007


var  x,y: discrete;  	
     p : parameter;

automaton p
synclabs : ;

initially ss & True;
           

loc ss : while x >= 0 & y >=0 wait {} 

-- t1
     when 
           x >= 1  
         do { x'=0, y'=y+2 } goto ss;

-- t2
     when 
       y >= 1  
     do { x'=x+2, y'=y-1 } goto ss;

end


var 
   init_reg, final_reg, reached: region;

init_reg   := x=1 & y=0 ;
final_reg  := x=3 & y=0 ;

reached:= reach backward from final_reg endreach;

 if empty(reached & init_reg)
  then prints "Target not reached (safety holds!)";
       print reached;
  else prints "Target reached (safety does not hold!)";

endif;