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
const ctime 75;
const true 1;
const false 0;
int[0,1] active;
clock x, time;
chan eject, ok;
urgent chan blck, red, remove, go;
process TaskMAIN{
state S0;
init S0;
trans S0 -> S0 {sync red?; },
S0 -> S0 {sync blck?; assign x:=0,
active:=true; };
}
process TaskPUSH{
state wait{x<=ctime}, passive;
init passive;
trans wait -> passive {guard x==ctime; sync eject!; assign active:=false; },
passive -> wait {guard active==true; sync go?; };
}
process Piston{
clock y;
state s1, s2{y<=1};
init s1;
trans s1 -> s2 {sync eject?; assign y:=0; },
s2 -> s1 {guard y==1; },
s2 -> s1 {sync remove!; };
}
process Dumb{
state S0;
init S0;
trans S0 -> S0 {sync go!; };
}
process BlackBox(const low, up){
clock pos;
state start{pos<=up}, on1{pos<=9}, on2{pos<=81}, piston{pos<=90}, end, sensor{pos<=18}, off;
init start;
trans sensor -> on2 {guard pos==18; },
on2 -> piston {guard pos==81; },
piston -> off {sync remove?; },
piston -> end {guard pos==90; },
start -> on1 {guard pos>=low; sync ok?; assign pos:=0; },
on1 -> sensor {guard pos==9; },
sensor -> on2 {sync blck!; };
}
process RedBox(const low, up){
clock pos;
state start{pos<=up}, on1{pos<=9}, on2{pos<=81}, piston{pos<=90}, end, sensor{pos<=18}, off;
init start;
trans sensor -> on2 {guard pos==18; },
on2 -> piston {guard pos==81; },
piston -> off {sync remove?; },
piston -> end {guard pos==90; },
start -> on1 {guard pos>=low; sync ok?; assign pos:=0; },
on1 -> sensor {guard pos==9; },
sensor -> on2 {sync red!; };
}
process Guard{
clock z;
state S0;
init S0;
trans S0 -> S0 {guard z>=10; sync ok!; assign z:=0; };
}
B1:=BlackBox(0,200);
B2:=BlackBox(0,200);
R1:=RedBox(0,200);
R2:=RedBox(0,200);
system
TaskMAIN, TaskPUSH,
Piston,
B1, B2, Dumb,
R1, R2, Guard;