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 black 1;
const red 2;
const true 1;
const false 0;
int[0,1] active;
clock x, time;
chan eject;
urgent chan blck, rd, remove, go;
process TaskMain{
state S0;
init S0;
trans S0 -> S0 {sync rd?; },
S0 -> S0 {sync blck?; assign x:=0,
active:=true; };
}
process TaskPiston{
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 ColorBox(const color, 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; assign pos:=0; },
on1 -> sensor {guard pos==9; },
sensor -> on2 {guard color==black; sync blck!; },
sensor -> on2 {guard color==red; sync rd!; };
}
BlackBox := ColorBox( black, 10, 10 );
RedBox:= ColorBox( red, 40, 40 );
AnotherBlackBox := ColorBox( black, 140, 240);
system
TaskMain, TaskPiston,
Piston,
BlackBox, RedBox,
Dumb;