Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
//Insert declarations of global clocks, variables, constants and channels. urgent chan coin, pub, cof; clock y, x, z; process Person{ //Insert local declarations of clocks, variables and constants. state start, Wait1{y<=3}, Ready, Wait2{y<=2}, Go; init start; trans start -> Wait1 {sync coin!; assign y:=0; }, Wait1 -> Ready {guard y==3; }, Ready -> Wait2 {sync cof?; assign y:=0; }, Wait2 -> Go {guard y==2; }, Go -> start {sync pub!; }; } process Machine{ //Insert local declarations of clocks, variables and constants. state S0, S1{x<=5}, S2{x<=5}; init S0; trans S0 -> S1 {sync coin?; assign x:=0; }, S1 -> S2 {guard x>=3; assign x:=0; }, S2 -> S0 {guard x==5; }, S2 -> S0 {sync cof!; }; } process Observer{ //Insert local declarations of clocks, variables and constants. state S0, sad, S2{z<=5}; init S0; trans S0 -> S2 {sync pub?; assign z:=0; }, S2 -> sad {guard z==5; }, S2 -> S2 {sync pub?; assign z:=0; }; } //Insert process assignments. //Edit system definition. system Person, Machine, Observer;