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
-- Pmen with full process MODULE main DEFINE nloc := 11; nc := 0; e1 := 1; e2 := 2; d0 := 3; h1 := 4; h2 := 5; h3 := 6; l1 := 7; l2 := 8; d1 := 9; cs := 10; ex := 11; Ch := c[h1] + c[h2] + c[cs]; Ct := c[d0] + c[d1] + c[h3]; Ca := c[ex]; Ce := c[e1] + c[e2]; Cl := c[l1] + c[l2]; Cha := Ch + Ca; Chtl := Ch + Ct + Cl; Chta := Ch + Ct + Ca; Cntc := c[h1] + c[h2] + c[h3] + Cl; Ccomp := Cntc + Ct; Ph := pi in {h1, h2, cs}; Pt := pi in {d0,d1}; Pa := pi in {ex}; Pe := pi in {e1,e2}; Pl := pi in {l1,l2}; Pha := Ph | Pa; Phtl := Ph | Pt | Pl; Phta := Ph | Pt | Pa; Pntc := pi in {h1, h2, h3} | Pl; --- Doorway Code --- Enc := c[nc] > 0; Ee1 := (c[e1] > 0) & ((Chtl = 0 & !Phtl) | Ca > 0 | Pa); Ee2 := c[e2] > 0; --- Compeition ----- Ed0_h1 := c[d0] > 0; Ed0_l1 := c[d0] > 0; Eh1_cs := (c[h1] > 0) & (Cha = 1 & !Pha); Eh1_h2 := (c[h1] > 0) & (Cha > 1 | Pha); Eh2 := c[h2] > 0; Eh3_d0 := (c[h3] > 0) & (Cha = 0) & !Pha & (PP0 > 0); Eh3_d1 := (c[h3] > 0) & (Cha = 0) & !Pha & (PP1 > 0); El1 := (c[l1] > 0) & (Chta = 0) & !Phta; El2_d0 := (c[l2] > 0) & (PP0 > 0); El2_d1 := (c[l2] > 0) & (PP1 > 0); Ed1_h1 := (c[d1] > 0) & (Planner.choose = 1); Ed1_l1 := (c[d1] > 0) & (Planner.choose = 2); --- Exit Code ---- Ecs_nc := (c[cs] > 0) & (Ccomp > 0 | Phtl); -- if someone in competition Ecs_ex := (c[cs] > 0) & (Ccomp = 0) & !Phtl; -- if none in competition Eex := (c[ex] > 0) & (Ce = 0) & !Pe; -- wait until none in enter VAR c : array 0..nloc of 0..2; from : -1..nloc; to : -1..nloc; sch : -1..nloc; PP0 : 0..1; PP1 : 0..1; pi : -1..nloc; Pchoose : boolean; Tnc : process Tr(nc, e1, Enc, c[nc], c[e1], from, to, PP0, PP1, Cntc); Te1 : process Tr(e1, e2, Ee1, c[e1], c[e2], from, to, PP0, PP1, Cntc); Te2 : process Tr(e2, d0, Ee2, c[e2], c[d0], from, to, PP0, PP1, Cntc); Td0_h1 : process Tr(d0, h1, Ed0_h1, c[d0], c[h1], from, to, PP0, PP1, Cntc); Td0_l1 : process Tr(d0, l1, Ed0_l1, c[d0], c[l1], from, to, PP0, PP1, Cntc); Th1_cs : process Tr(h1, cs, Eh1_cs, c[h1], c[cs], from, to, PP0, PP1, Cntc); Th1_h2 : process Tr(h1, h2, Eh1_h2, c[h1], c[h2], from, to, PP0, PP1, Cntc); Th2 : process Tr(h2, h3, Eh2, c[h2], c[h3], from, to, PP0, PP1, Cntc); Th3_d0 : process Tr(h3, d0, Eh3_d0, c[h3], c[d0], from, to, PP0, PP1, Cntc); Th3_d1 : process Tr(h3, d1, Eh3_d1, c[h3], c[d1], from, to, PP0, PP1, Cntc); Tl1 : process Tr(l1, l2, El1, c[l1], c[l2], from, to, PP0, PP1, Cntc); Tl2_d0 : process Tr(l2, d0, El2_d0, c[l2], c[d0], from, to, PP0, PP1, Cntc); Tl2_d1 : process Tr(l2, d1, El2_d1, c[l2], c[d1], from, to, PP0, PP1, Cntc); Td1_h1 : process Tr(d1, h1, Ed1_h1, c[d1], c[h1], from, to, PP0, PP1, Cntc); Td1_l1 : process Tr(d1, l1, Ed1_l1, c[d1], c[l1], from, to, PP0, PP1, Cntc); Tcs_nc : process Tr(cs, nc, Ecs_nc, c[cs], c[nc], from, to, PP0, PP1, Cntc); Tcs_ex : process Tr(cs, ex, Ecs_ex, c[cs], c[ex], from, to, PP0, PP1, Cntc); Tex : process Tr(ex, nc, Eex, c[ex], c[nc], from, to, PP0, PP1, Cntc); Pfull : process P(pi, Pchoose, Ca, Ce, Cha, Chtl, Chta, Cntc, Planner.choose); Idle : process Id(from,to,PP0,PP1,c[d0], c[d1], (Ccomp > 0 | Phtl), Pchoose); Planner: planner(Ch, Ph); ASSIGN init(c[nc]) := 1; init(c[e1]) := 0; init(c[e2]) := 0; init(c[d0]) := 0; init(c[h1]) := 0; init(c[h2]) := 0; init(c[h3]) := 0; init(c[l1]) := 0; init(c[l2]) := 0; init(c[d1]) := 0; init(c[cs]) := 0; init(c[ex]) := 0; init(from) := -1; init(to) := -1; init(PP0) := 0; init(PP1) := 0; init(pi) := 0; init(Pchoose) := 0; MODULE Id(from,to,pp0, pp1, cd0, cd1, n_e_comp, Pchoose) -- n_e_comp is non-empty-competition, that is, either Ccomp > 0 or Phtl VAR inc : boolean; ASSIGN next(from) := -1; next(to) := -1; next(inc) := {0,1}; next(pp0) := case next(inc) : 0; 1 : pp0; esac; next(pp1) := case next(inc) & (pp0> 0 | pp1 > 0) : 1; 1 : pp1; esac; next(cd0) := case next(inc) : 0; 1 : cd0; esac; next(cd1) := case next(inc) & (cd0 > 0 | cd1 > 0) : 1; 1 : cd1; esac; next(Pchoose) := case next(inc) : 1; 1 : Pchoose; esac; JUSTICE !(n_e_comp & inc=0), inc=0 MODULE Tr(fid, tid, En, cf, ct, from, to, pp0, pp1, Cntc) DEFINE nloc := 11; nc := 0; e1 := 1; e2 := 2; d0 := 3; h1 := 4; h2 := 5; h3 := 6; l1 := 7; l2 := 8; d1 := 9; cs := 10; ex := 11; ASSIGN next(cf) := case !En : cf; (fid = cs | fid = ex) : 0; (fid = h1) & (cf = 2) : {1,2}; fid = h1 : 0; cf = 1 : {0,1}; 1 : cf; esac; next(ct) := case !En : ct; (tid = h1) & (ct = 2): 2; tid = h1 : ct + 1; ct = 1 : 1; ct < 1 : ct + 1; 1 : ct; esac; next(from) := case !En : -1; 1 : fid; esac; next(to) := case !En : -1; 1 : tid; esac; next(pp0) := case !En : pp0; ((tid = d0 | tid = d1) & next(cf) = 0 & Cntc = 1) : 0; ((tid = d0 | tid = d1) & pp0 = 1) : {0,1}; (fid = d0 & pp0 = 0) : 1; 1 : pp0; esac; next(pp1) := case !En : pp1; ((tid = d0 | tid = d1) & next(cf) = 0 & Cntc = 1) : 0; ((tid = d0 | tid = d1) & pp1 = 1) : {0,1}; (fid = d1 & pp1 =0) : 1; 1 : pp1; esac; JUSTICE !En | (from = fid) COMPASSION (from = fid, to = fid), ((to = e1), (to = d0)), (pp0 > 0 & ((from = d0) | (from = d1)), pp0 = 0), (pp1 > 0 & ((from = d0) | (from = d1)), pp1 = 0) MODULE P(pi, Pchoose, Ca, Ce, Cha, Chtl, Chta, Cntc, choose) DEFINE nloc := 11; nc := 0; e1 := 1; e2 := 2; d := 3; h1 := 4; h2 := 5; h3 := 6; l1 := 7; l2 := 8; -- d1 := 9; cs := 10; ex := 11; --- Doorway Code --- enc := pi = nc; ee1 := (pi = e1) & (Chtl = 0 | Ca > 0 ); ee2 := pi = e2; --- Compeition ----- ed_h1 := (pi = d & Pchoose & choose = 1); ed_l1 := (pi = d & Pchoose & choose = 2); ed := pi = d; eh1_cs := (pi = h1) & (Cha = 0); eh1_h2 := (pi = h1) & (Cha > 1); eh2 := pi = h2; eh3 := (pi = h3) & (Cha = 0); el1 := (pi = l1) & (Chta = 0); el2 := (pi = l2); --- Exit Code ---- ecs_nc := (pi = cs) & Chtl > 0; ecs_ex := (pi = cs) & Chtl = 0; eex := (pi = ex) & (Ce = 0); ASSIGN next(pi) := case enc : {nc,e1}; ee1 : e2; ee2 : d; ed_h1 : h1; ed_l1 : l1; ed : {h1, l1}; eh1_cs : cs; eh1_h2 : h1; eh2 : h3; eh3 : d; el1 : l2; el2 : d; ecs_nc : nc; ecs_ex : ex; eex : nc; 1 : pi; esac; next(Pchoose) := case Pchoose & pi = d : 0; 1 : Pchoose; esac; JUSTICE !ee1, !(pi = e2), !(pi = d), !(pi = h1), !(pi = h2), !eh3, !el1, !(pi = l2), !(pi = cs), !eex MODULE planner(C12,Ph) DEFINE choose := case C12=0 & !Ph : 1; 1 : 2; esac;