<br />
<b>Deprecated</b>:  The each() function is deprecated. This message will be suppressed on further calls in <b>/home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php</b> on line <b>456</b><br />
process TaskMAIN graphinfo {
templateName (32, 16);
paramList (184, 0);
location S0 (128, 96);
locationName S0 (-10, -30);
trans S0 S0 1 (-48, -16), (-48, 16);
guard S0 S0 1 (-60, -30);
sync S0 S0 1 (-96, -8);
assign S0 S0 1 (-60, 15);
trans S0 S0 2 (48, -16), (48, 16);
guard S0 S0 2 (-60, -30);
sync S0 S0 2 (64, -24);
assign S0 S0 2 (64, 0);
}
process TaskPUSH graphinfo {
templateName (32, 16);
paramList (184, 0);
location wait (72, 104);
locationName wait (-32, 16);
invariant wait (-32, 32);
location passive (248, 96);
locationName passive (-8, 16);
trans wait passive 1 (-64, -32), (64, -32);
guard wait passive 1 (-104, -56);
sync wait passive 1 (-24, -56);
assign wait passive 1 (40, -56);
trans passive wait 1 (64, 32), (-64, 32);
guard passive wait 1 (-56, 40);
sync passive wait 1 (48, 40);
}
process Piston graphinfo {
templateName (32, 16);
paramList (160, 0);
location s1 (96, 64);
locationName s1 (8, 8);
location s2 (96, 208);
locationName s2 (8, 8);
invariant s2 (8, 24);
sync s1 s2 1 (8, -28);
assign s1 s2 1 (8, 32);
trans s2 s1 1 (64, 72), (64, -72);
guard s2 s1 1 (56, 80);
trans s2 s1 2 (-64, 72), (-64, -72);
sync s2 s1 2 (-80, 80);
}
process Dumb graphinfo {
templateName (32, 16);
paramList (144, 0);
location S0 (64, 64);
locationName S0 (-32, -8);
trans S0 S0 1 (48, -16), (48, 16);
sync S0 S0 1 (56, -8);
}
process BlackBox graphinfo {
templateName (32, 16);
paramList (168, 0);
location start (48, 208);
locationName start (8, 8);
invariant start (8, 24);
location on1 (48, 80);
locationName on1 (8, 8);
invariant on1 (8, 24);
location on2 (304, 80);
locationName on2 (8, 8);
invariant on2 (8, 24);
location piston (432, 80);
locationName piston (8, 8);
invariant piston (8, 24);
location end (560, 80);
locationName end (8, 8);
location sensor (176, 80);
locationName sensor (8, 8);
invariant sensor (8, 24);
location off (432, 208);
locationName off (8, 8);
guard sensor on2 1 (-24, -24);
guard on2 piston 1 (-24, -24);
sync piston off 1 (8, 0);
guard piston end 1 (-48, -24);
guard start on1 1 (8, 0);
sync start on1 1 (-24, -16);
assign start on1 1 (8, 24);
guard on1 sensor 1 (-16, -24);
trans sensor on2 2 (-64, 48), (64, 48);
sync sensor on2 2 (-8, 56);
}
process RedBox graphinfo {
templateName (32, 16);
paramList (152, 0);
location start (48, 240);
locationName start (8, 8);
invariant start (8, 24);
location on1 (48, 112);
locationName on1 (8, 8);
invariant on1 (8, 24);
location on2 (304, 112);
locationName on2 (8, 8);
invariant on2 (8, 24);
location piston (432, 112);
locationName piston (8, 8);
invariant piston (8, 24);
location end (560, 112);
locationName end (8, 8);
location sensor (176, 112);
locationName sensor (-16, 8);
invariant sensor (-24, 24);
location off (432, 240);
locationName off (8, 8);
guard sensor on2 1 (-40, -24);
guard on2 piston 1 (-24, -24);
sync piston off 1 (8, 0);
guard piston end 1 (-48, -24);
guard start on1 1 (8, 0);
sync start on1 1 (-24, -8);
assign start on1 1 (8, 24);
guard on1 sensor 1 (-16, -24);
trans sensor on2 2 (-64, -40), (64, -40);
guard sensor on2 2 (-60, -30);
sync sensor on2 2 (-8, -64);
assign sensor on2 2 (-60, 15);
}
process Guard graphinfo {
templateName (5, 5);
paramList (5, 20);
location S0 (128, 96);
locationName S0 (-10, -30);
trans S0 S0 1 (-32, 64), (32, 64);
guard S0 S0 1 (-48, 8);
sync S0 S0 1 (-8, 64);
assign S0 S0 1 (24, 8);
}