--Russian Cards in MCMAS (v0.6) --three agents Anne,Bill,Cath, Seven cards 0-6. --Assume each agent only knows her own card. --step 1 Dealing 3 cards to Anne, 3 cards to Bill, 1 card to Cath. --step 2 Anne makes an announcement. --step 3 Bill makes an announcement. --Now We verify that the following is a solution for Russian Cards problem:--Suppose the actual deal is 012.345.6 and --Anne announces "my hand is in {012,034,056,135,246}". --Bill announces "Cath has card 6". --We verify this is a solution for Russian Cards problem. --variable for agent Anne: axxxnn --var1-3: axxx the cards that Anne holds. --var4: n, t, f for A announces nothing, true, false respectively --var5: n, t, f for B announces nothing, true, false respectively --Similar for Bill. For Cath, we use cxnn --We also introduce an enviroment agent Env which encodes the actual deals. Agent Anne Lstate = { annnnn, a012nn,a012nt,a012nf,a012tn,a012tt,a012tf,a012fn,a012ft, a012ff,a013nn,a013nt,a013nf,a013tn,a013tt,a013tf,a013fn, a013ft,a013ff,a014nn,a014nt,a014nf,a014tn,a014tt,a014tf, a014fn,a014ft,a014ff,a015nn,a015nt,a015nf,a015tn,a015tt, a015tf,a015fn,a015ft,a015ff,a016nn,a016nt,a016nf,a016tn, a016tt,a016tf,a016fn,a016ft,a016ff,a023nn,a023nt,a023nf, a023tn,a023tt,a023tf,a023fn,a023ft,a023ff,a024nn,a024nt, a024nf,a024tn,a024tt,a024tf,a024fn,a024ft,a024ff,a025nn, a025nt,a025nf,a025tn,a025tt,a025tf,a025fn,a025ft,a025ff, a026nn,a026nt,a026nf,a026tn,a026tt,a026tf,a026fn,a026ft, a026ff,a034nn,a034nt,a034nf,a034tn,a034tt,a034tf,a034fn, a034ft,a034ff,a035nn,a035nt,a035nf,a035tn,a035tt,a035tf, a035fn,a035ft,a035ff,a036nn,a036nt,a036nf,a036tn,a036tt, a036tf,a036fn,a036ft,a036ff,a045nn,a045nt,a045nf,a045tn, a045tt,a045tf,a045fn,a045ft,a045ff,a046nn,a046nt,a046nf, a046tn,a046tt,a046tf,a046fn,a046ft,a046ff,a056nn,a056nt, a056nf,a056tn,a056tt,a056tf,a056fn,a056ft,a056ff,a123nn, a123nt,a123nf,a123tn,a123tt,a123tf,a123fn,a123ft,a123ff, a124nn,a124nt,a124nf,a124tn,a124tt,a124tf,a124fn,a124ft, a124ff,a125nn,a125nt,a125nf,a125tn,a125tt,a125tf,a125fn, a125ft,a125ff,a126nn,a126nt,a126nf,a126tn,a126tt,a126tf, a126fn,a126ft,a126ff,a134nn,a134nt,a134nf,a134tn,a134tt, a134tf,a134fn,a134ft,a134ff,a135nn,a135nt,a135nf,a135tn, a135tt,a135tf,a135fn,a135ft,a135ff,a136nn,a136nt,a136nf, a136tn,a136tt,a136tf,a136fn,a136ft,a136ff,a145nn,a145nt, a145nf,a145tn,a145tt,a145tf,a145fn,a145ft,a145ff,a146nn, a146nt,a146nf,a146tn,a146tt,a146tf,a146fn,a146ft,a146ff, a156nn,a156nt,a156nf,a156tn,a156tt,a156tf,a156fn,a156ft, a156ff,a234nn,a234nt,a234nf,a234tn,a234tt,a234tf,a234fn, a234ft,a234ff,a235nn,a235nt,a235nf,a235tn,a235tt,a235tf, a235fn,a235ft,a235ff,a236nn,a236nt,a236nf,a236tn,a236tt, a236tf,a236fn,a236ft,a236ff,a245nn,a245nt,a245nf,a245tn, a245tt,a245tf,a245fn,a245ft,a245ff,a246nn,a246nt,a246nf, a246tn,a246tt,a246tf,a246fn,a246ft,a246ff,a256nn,a256nt, a256nf,a256tn,a256tt,a256tf,a256fn,a256ft,a256ff,a345nn, a345nt,a345nf,a345tn,a345tt,a345tf,a345fn,a345ft,a345ff, a346nn,a346nt,a346nf,a346tn,a346tt,a346tf,a346fn,a346ft, a346ff,a356nn,a356nt,a356nf,a356tn,a356tt,a356tf,a356fn, a356ft,a356ff,a456nn,a456nt,a456nf,a456tn,a456tt,a456tf, a456fn,a456ft,a456ff}; Lgreen = { annnnn, a012nn,a012nt,a012nf,a012tn,a012tt,a012tf,a012fn,a012ft, a012ff,a013nn,a013nt,a013nf,a013tn,a013tt,a013tf,a013fn, a013ft,a013ff,a014nn,a014nt,a014nf,a014tn,a014tt,a014tf, a014fn,a014ft,a014ff,a015nn,a015nt,a015nf,a015tn,a015tt, a015tf,a015fn,a015ft,a015ff,a016nn,a016nt,a016nf,a016tn, a016tt,a016tf,a016fn,a016ft,a016ff,a023nn,a023nt,a023nf, a023tn,a023tt,a023tf,a023fn,a023ft,a023ff,a024nn,a024nt, a024nf,a024tn,a024tt,a024tf,a024fn,a024ft,a024ff,a025nn, a025nt,a025nf,a025tn,a025tt,a025tf,a025fn,a025ft,a025ff, a026nn,a026nt,a026nf,a026tn,a026tt,a026tf,a026fn,a026ft, a026ff,a034nn,a034nt,a034nf,a034tn,a034tt,a034tf,a034fn, a034ft,a034ff,a035nn,a035nt,a035nf,a035tn,a035tt,a035tf, a035fn,a035ft,a035ff,a036nn,a036nt,a036nf,a036tn,a036tt, a036tf,a036fn,a036ft,a036ff,a045nn,a045nt,a045nf,a045tn, a045tt,a045tf,a045fn,a045ft,a045ff,a046nn,a046nt,a046nf, a046tn,a046tt,a046tf,a046fn,a046ft,a046ff,a056nn,a056nt, a056nf,a056tn,a056tt,a056tf,a056fn,a056ft,a056ff,a123nn, a123nt,a123nf,a123tn,a123tt,a123tf,a123fn,a123ft,a123ff, a124nn,a124nt,a124nf,a124tn,a124tt,a124tf,a124fn,a124ft, a124ff,a125nn,a125nt,a125nf,a125tn,a125tt,a125tf,a125fn, a125ft,a125ff,a126nn,a126nt,a126nf,a126tn,a126tt,a126tf, a126fn,a126ft,a126ff,a134nn,a134nt,a134nf,a134tn,a134tt, a134tf,a134fn,a134ft,a134ff,a135nn,a135nt,a135nf,a135tn, a135tt,a135tf,a135fn,a135ft,a135ff,a136nn,a136nt,a136nf, a136tn,a136tt,a136tf,a136fn,a136ft,a136ff,a145nn,a145nt, a145nf,a145tn,a145tt,a145tf,a145fn,a145ft,a145ff,a146nn, a146nt,a146nf,a146tn,a146tt,a146tf,a146fn,a146ft,a146ff, a156nn,a156nt,a156nf,a156tn,a156tt,a156tf,a156fn,a156ft, a156ff,a234nn,a234nt,a234nf,a234tn,a234tt,a234tf,a234fn, a234ft,a234ff,a235nn,a235nt,a235nf,a235tn,a235tt,a235tf, a235fn,a235ft,a235ff,a236nn,a236nt,a236nf,a236tn,a236tt, a236tf,a236fn,a236ft,a236ff,a245nn,a245nt,a245nf,a245tn, a245tt,a245tf,a245fn,a245ft,a245ff,a246nn,a246nt,a246nf, a246tn,a246tt,a246tf,a246fn,a246ft,a246ff,a256nn,a256nt, a256nf,a256tn,a256tt,a256tf,a256fn,a256ft,a256ff,a345nn, a345nt,a345nf,a345tn,a345tt,a345tf,a345fn,a345ft,a345ff, a346nn,a346nt,a346nf,a346tn,a346tt,a346tf,a346fn,a346ft, a346ff,a356nn,a356nt,a356nf,a356tn,a356tt,a356tf,a356fn, a356ft,a356ff,a456nn,a456nt,a456nf,a456tn,a456tt,a456tf, a456fn,a456ft,a456ff}; Action ={null, Announce}; Protocol: annnnn:{null}; a012nn:{null};a012nt:{null};a012nf:{null};a012tn:{null};a012tt:{null}; a012tf:{null};a012fn:{null};a012ft:{null};a012ff:{null};a013nn:{null}; a013nt:{null};a013nf:{null};a013tn:{null};a013tt:{null};a013tf:{null}; a013fn:{null};a013ft:{null};a013ff:{null};a014nn:{null};a014nt:{null}; a014nf:{null};a014tn:{null};a014tt:{null};a014tf:{null};a014fn:{null}; a014ft:{null};a014ff:{null};a015nn:{null};a015nt:{null};a015nf:{null}; a015tn:{null};a015tt:{null};a015tf:{null};a015fn:{null};a015ft:{null}; a015ff:{null};a016nn:{null};a016nt:{null};a016nf:{null};a016tn:{null}; a016tt:{null};a016tf:{null};a016fn:{null};a016ft:{null};a016ff:{null}; a023nn:{null};a023nt:{null};a023nf:{null};a023tn:{null};a023tt:{null}; a023tf:{null};a023fn:{null};a023ft:{null};a023ff:{null};a024nn:{null}; a024nt:{null};a024nf:{null};a024tn:{null};a024tt:{null};a024tf:{null}; a024fn:{null};a024ft:{null};a024ff:{null};a025nn:{null};a025nt:{null}; a025nf:{null};a025tn:{null};a025tt:{null};a025tf:{null};a025fn:{null}; a025ft:{null};a025ff:{null};a026nn:{null};a026nt:{null};a026nf:{null}; a026tn:{null};a026tt:{null};a026tf:{null};a026fn:{null};a026ft:{null}; a026ff:{null};a034nn:{null};a034nt:{null};a034nf:{null};a034tn:{null}; a034tt:{null};a034tf:{null};a034fn:{null};a034ft:{null};a034ff:{null}; a035nn:{null};a035nt:{null};a035nf:{null};a035tn:{null};a035tt:{null}; a035tf:{null};a035fn:{null};a035ft:{null};a035ff:{null};a036nn:{null}; a036nt:{null};a036nf:{null};a036tn:{null};a036tt:{null};a036tf:{null}; a036fn:{null};a036ft:{null};a036ff:{null};a045nn:{null};a045nt:{null}; a045nf:{null};a045tn:{null};a045tt:{null};a045tf:{null};a045fn:{null}; a045ft:{null};a045ff:{null};a046nn:{null};a046nt:{null};a046nf:{null}; a046tn:{null};a046tt:{null};a046tf:{null};a046fn:{null};a046ft:{null}; a046ff:{null};a056nn:{null};a056nt:{null};a056nf:{null};a056tn:{null}; a056tt:{null};a056tf:{null};a056fn:{null};a056ft:{null};a056ff:{null}; a123nn:{null};a123nt:{null};a123nf:{null};a123tn:{null};a123tt:{null}; a123tf:{null};a123fn:{null};a123ft:{null};a123ff:{null};a124nn:{null}; a124nt:{null};a124nf:{null};a124tn:{null};a124tt:{null};a124tf:{null}; a124fn:{null};a124ft:{null};a124ff:{null};a125nn:{null};a125nt:{null}; a125nf:{null};a125tn:{null};a125tt:{null};a125tf:{null};a125fn:{null}; a125ft:{null};a125ff:{null};a126nn:{null};a126nt:{null};a126nf:{null}; a126tn:{null};a126tt:{null};a126tf:{null};a126fn:{null};a126ft:{null}; a126ff:{null};a134nn:{null};a134nt:{null};a134nf:{null};a134tn:{null}; a134tt:{null};a134tf:{null};a134fn:{null};a134ft:{null};a134ff:{null}; a135nn:{null};a135nt:{null};a135nf:{null};a135tn:{null};a135tt:{null}; a135tf:{null};a135fn:{null};a135ft:{null};a135ff:{null};a136nn:{null}; a136nt:{null};a136nf:{null};a136tn:{null};a136tt:{null};a136tf:{null}; a136fn:{null};a136ft:{null};a136ff:{null};a145nn:{null};a145nt:{null}; a145nf:{null};a145tn:{null};a145tt:{null};a145tf:{null};a145fn:{null}; a145ft:{null};a145ff:{null};a146nn:{null};a146nt:{null};a146nf:{null}; a146tn:{null};a146tt:{null};a146tf:{null};a146fn:{null};a146ft:{null}; a146ff:{null};a156nn:{null};a156nt:{null};a156nf:{null};a156tn:{null}; a156tt:{null};a156tf:{null};a156fn:{null};a156ft:{null};a156ff:{null}; a234nn:{null};a234nt:{null};a234nf:{null};a234tn:{null};a234tt:{null}; a234tf:{null};a234fn:{null};a234ft:{null};a234ff:{null};a235nn:{null}; a235nt:{null};a235nf:{null};a235tn:{null};a235tt:{null};a235tf:{null}; a235fn:{null};a235ft:{null};a235ff:{null};a236nn:{null};a236nt:{null}; a236nf:{null};a236tn:{null};a236tt:{null};a236tf:{null};a236fn:{null}; a236ft:{null};a236ff:{null};a245nn:{null};a245nt:{null};a245nf:{null}; a245tn:{null};a245tt:{null};a245tf:{null};a245fn:{null};a245ft:{null}; a245ff:{null};a246nn:{null};a246nt:{null};a246nf:{null};a246tn:{null}; a246tt:{null};a246tf:{null};a246fn:{null};a246ft:{null};a246ff:{null}; a256nn:{null};a256nt:{null};a256nf:{null};a256tn:{null};a256tt:{null}; a256tf:{null};a256fn:{null};a256ft:{null};a256ff:{null};a345nn:{null}; a345nt:{null};a345nf:{null};a345tn:{null};a345tt:{null};a345tf:{null}; a345fn:{null};a345ft:{null};a345ff:{null};a346nn:{null};a346nt:{null}; a346nf:{null};a346tn:{null};a346tt:{null};a346tf:{null};a346fn:{null}; a346ft:{null};a346ff:{null};a356nn:{null};a356nt:{null};a356nf:{null}; a356tn:{null};a356tt:{null};a356tf:{null};a356fn:{null};a356ft:{null}; a356ff:{null};a456nn:{null};a456nt:{null};a456nf:{null};a456tn:{null}; a456tt:{null};a456tf:{null};a456fn:{null};a456ft:{null};a456ff:{null}; end Protocol Ev: -----1 Reveal cards to Anne:annnnn->axxxnn------ a012nn if (Lstate=annnnn and ( Env.Lstate=e0123456 or Env.Lstate=e0123465 or Env.Lstate=e0123564 or Env.Lstate=e0124563 )); a013nn if (Lstate=annnnn and ( Env.Lstate=e0132456 or Env.Lstate=e0132465 or Env.Lstate=e0132564 or Env.Lstate=e0134562 )); a014nn if (Lstate=annnnn and ( Env.Lstate=e0142356 or Env.Lstate=e0142365 or Env.Lstate=e0142563 or Env.Lstate=e0143562 )); a015nn if (Lstate=annnnn and ( Env.Lstate=e0152346 or Env.Lstate=e0152364 or Env.Lstate=e0152463 or Env.Lstate=e0153462 )); a016nn if (Lstate=annnnn and ( Env.Lstate=e0162345 or Env.Lstate=e0162354 or Env.Lstate=e0162453 or Env.Lstate=e0163452 )); a023nn if (Lstate=annnnn and ( Env.Lstate=e0231456 or Env.Lstate=e0231465 or Env.Lstate=e0231564 or Env.Lstate=e0234561 )); a024nn if (Lstate=annnnn and ( Env.Lstate=e0241356 or Env.Lstate=e0241365 or Env.Lstate=e0241563 or Env.Lstate=e0243561 )); a025nn if (Lstate=annnnn and ( Env.Lstate=e0251346 or Env.Lstate=e0251364 or Env.Lstate=e0251463 or Env.Lstate=e0253461 )); a026nn if (Lstate=annnnn and ( Env.Lstate=e0261345 or Env.Lstate=e0261354 or Env.Lstate=e0261453 or Env.Lstate=e0263451 )); a034nn if (Lstate=annnnn and ( Env.Lstate=e0341256 or Env.Lstate=e0341265 or Env.Lstate=e0341562 or Env.Lstate=e0342561 )); a035nn if (Lstate=annnnn and ( Env.Lstate=e0351246 or Env.Lstate=e0351264 or Env.Lstate=e0351462 or Env.Lstate=e0352461 )); a036nn if (Lstate=annnnn and ( Env.Lstate=e0361245 or Env.Lstate=e0361254 or Env.Lstate=e0361452 or Env.Lstate=e0362451 )); a045nn if (Lstate=annnnn and ( Env.Lstate=e0451236 or Env.Lstate=e0451263 or Env.Lstate=e0451362 or Env.Lstate=e0452361 )); a046nn if (Lstate=annnnn and ( Env.Lstate=e0461235 or Env.Lstate=e0461253 or Env.Lstate=e0461352 or Env.Lstate=e0462351 )); a056nn if (Lstate=annnnn and ( Env.Lstate=e0561234 or Env.Lstate=e0561243 or Env.Lstate=e0561342 or Env.Lstate=e0562341 )); a123nn if (Lstate=annnnn and ( Env.Lstate=e1230456 or Env.Lstate=e1230465 or Env.Lstate=e1230564 or Env.Lstate=e1234560 )); a124nn if (Lstate=annnnn and ( Env.Lstate=e1240356 or Env.Lstate=e1240365 or Env.Lstate=e1240563 or Env.Lstate=e1243560 )); a125nn if (Lstate=annnnn and ( Env.Lstate=e1250346 or Env.Lstate=e1250364 or Env.Lstate=e1250463 or Env.Lstate=e1253460 )); a126nn if (Lstate=annnnn and ( Env.Lstate=e1260345 or Env.Lstate=e1260354 or Env.Lstate=e1260453 or Env.Lstate=e1263450 )); a134nn if (Lstate=annnnn and ( Env.Lstate=e1340256 or Env.Lstate=e1340265 or Env.Lstate=e1340562 or Env.Lstate=e1342560 )); a135nn if (Lstate=annnnn and ( Env.Lstate=e1350246 or Env.Lstate=e1350264 or Env.Lstate=e1350462 or Env.Lstate=e1352460 )); a136nn if (Lstate=annnnn and ( Env.Lstate=e1360245 or Env.Lstate=e1360254 or Env.Lstate=e1360452 or Env.Lstate=e1362450 )); a145nn if (Lstate=annnnn and ( Env.Lstate=e1450236 or Env.Lstate=e1450263 or Env.Lstate=e1450362 or Env.Lstate=e1452360 )); a146nn if (Lstate=annnnn and ( Env.Lstate=e1460235 or Env.Lstate=e1460253 or Env.Lstate=e1460352 or Env.Lstate=e1462350 )); a156nn if (Lstate=annnnn and ( Env.Lstate=e1560234 or Env.Lstate=e1560243 or Env.Lstate=e1560342 or Env.Lstate=e1562340 )); a234nn if (Lstate=annnnn and ( Env.Lstate=e2340156 or Env.Lstate=e2340165 or Env.Lstate=e2340561 or Env.Lstate=e2341560 )); a235nn if (Lstate=annnnn and ( Env.Lstate=e2350146 or Env.Lstate=e2350164 or Env.Lstate=e2350461 or Env.Lstate=e2351460 )); a236nn if (Lstate=annnnn and ( Env.Lstate=e2360145 or Env.Lstate=e2360154 or Env.Lstate=e2360451 or Env.Lstate=e2361450 )); a245nn if (Lstate=annnnn and ( Env.Lstate=e2450136 or Env.Lstate=e2450163 or Env.Lstate=e2450361 or Env.Lstate=e2451360 )); a246nn if (Lstate=annnnn and ( Env.Lstate=e2460135 or Env.Lstate=e2460153 or Env.Lstate=e2460351 or Env.Lstate=e2461350 )); a256nn if (Lstate=annnnn and ( Env.Lstate=e2560134 or Env.Lstate=e2560143 or Env.Lstate=e2560341 or Env.Lstate=e2561340 )); a345nn if (Lstate=annnnn and ( Env.Lstate=e3450126 or Env.Lstate=e3450162 or Env.Lstate=e3450261 or Env.Lstate=e3451260 )); a346nn if (Lstate=annnnn and ( Env.Lstate=e3460125 or Env.Lstate=e3460152 or Env.Lstate=e3460251 or Env.Lstate=e3461250 )); a356nn if (Lstate=annnnn and ( Env.Lstate=e3560124 or Env.Lstate=e3560142 or Env.Lstate=e3560241 or Env.Lstate=e3561240 )); a456nn if (Lstate=annnnn and ( Env.Lstate=e4560123 or Env.Lstate=e4560132 or Env.Lstate=e4560231 or Env.Lstate=e4561230 )); -----2 Anne's Announcement:axxxnn->axxxxn------ a012tn if (Lstate=a012nn); a013fn if (Lstate=a013nn); a014fn if (Lstate=a014nn); a015fn if (Lstate=a015nn); a016fn if (Lstate=a016nn); a023fn if (Lstate=a023nn); a024fn if (Lstate=a024nn); a025fn if (Lstate=a025nn); a026fn if (Lstate=a026nn); a034tn if (Lstate=a034nn); a035fn if (Lstate=a035nn); a036fn if (Lstate=a036nn); a045fn if (Lstate=a045nn); a046fn if (Lstate=a046nn); a056tn if (Lstate=a056nn); a123fn if (Lstate=a123nn); a124fn if (Lstate=a124nn); a125fn if (Lstate=a125nn); a126fn if (Lstate=a126nn); a134fn if (Lstate=a134nn); a135tn if (Lstate=a135nn); a136fn if (Lstate=a136nn); a145fn if (Lstate=a145nn); a146fn if (Lstate=a146nn); a156fn if (Lstate=a156nn); a234fn if (Lstate=a234nn); a235fn if (Lstate=a235nn); a236fn if (Lstate=a236nn); a245fn if (Lstate=a245nn); a246tn if (Lstate=a246nn); a256fn if (Lstate=a256nn); a345fn if (Lstate=a345nn); a346fn if (Lstate=a346nn); a356fn if (Lstate=a356nn); a456fn if (Lstate=a456nn); -----2 Bill's Announcement:axxxxn->axxxxx------ a012tt if (Lstate=a012tn and Env.Lstate=e0123456); a012tf if (Lstate=a012tn and ( Env.Lstate=e0123465 or Env.Lstate=e0123564 or Env.Lstate=e0124563)); a034tt if (Lstate=a034tn and Env.Lstate=e0341256); a034tf if (Lstate=a034tn and ( Env.Lstate=e0341265 or Env.Lstate=e0341562 or Env.Lstate=e0342561)); a056tf if (Lstate=a056tn and ( Env.Lstate=e0561234 or Env.Lstate=e0561243 or Env.Lstate=e0561342 or Env.Lstate=e0562341)); a135tt if (Lstate=a135tn and Env.Lstate=e1350246); a135tf if (Lstate=a135tn and ( Env.Lstate=e1350264 or Env.Lstate=e1350462 or Env.Lstate=e1352460)); a246tf if (Lstate=a246tn and ( Env.Lstate=e2460135 or Env.Lstate=e2460153 or Env.Lstate=e2460351 or Env.Lstate=e2461350)); end Ev end Agent Agent Bill Lstate = { bnnnnn, b012nn,b012nt,b012nf,b012tn,b012tt,b012tf,b012fn,b012ft, b012ff,b013nn,b013nt,b013nf,b013tn,b013tt,b013tf,b013fn, b013ft,b013ff,b014nn,b014nt,b014nf,b014tn,b014tt,b014tf, b014fn,b014ft,b014ff,b015nn,b015nt,b015nf,b015tn,b015tt, b015tf,b015fn,b015ft,b015ff,b016nn,b016nt,b016nf,b016tn, b016tt,b016tf,b016fn,b016ft,b016ff,b023nn,b023nt,b023nf, b023tn,b023tt,b023tf,b023fn,b023ft,b023ff,b024nn,b024nt, b024nf,b024tn,b024tt,b024tf,b024fn,b024ft,b024ff,b025nn, b025nt,b025nf,b025tn,b025tt,b025tf,b025fn,b025ft,b025ff, b026nn,b026nt,b026nf,b026tn,b026tt,b026tf,b026fn,b026ft, b026ff,b034nn,b034nt,b034nf,b034tn,b034tt,b034tf,b034fn, b034ft,b034ff,b035nn,b035nt,b035nf,b035tn,b035tt,b035tf, b035fn,b035ft,b035ff,b036nn,b036nt,b036nf,b036tn,b036tt, b036tf,b036fn,b036ft,b036ff,b045nn,b045nt,b045nf,b045tn, b045tt,b045tf,b045fn,b045ft,b045ff,b046nn,b046nt,b046nf, b046tn,b046tt,b046tf,b046fn,b046ft,b046ff,b056nn,b056nt, b056nf,b056tn,b056tt,b056tf,b056fn,b056ft,b056ff,b123nn, b123nt,b123nf,b123tn,b123tt,b123tf,b123fn,b123ft,b123ff, b124nn,b124nt,b124nf,b124tn,b124tt,b124tf,b124fn,b124ft, b124ff,b125nn,b125nt,b125nf,b125tn,b125tt,b125tf,b125fn, b125ft,b125ff,b126nn,b126nt,b126nf,b126tn,b126tt,b126tf, b126fn,b126ft,b126ff,b134nn,b134nt,b134nf,b134tn,b134tt, b134tf,b134fn,b134ft,b134ff,b135nn,b135nt,b135nf,b135tn, b135tt,b135tf,b135fn,b135ft,b135ff,b136nn,b136nt,b136nf, b136tn,b136tt,b136tf,b136fn,b136ft,b136ff,b145nn,b145nt, b145nf,b145tn,b145tt,b145tf,b145fn,b145ft,b145ff,b146nn, b146nt,b146nf,b146tn,b146tt,b146tf,b146fn,b146ft,b146ff, b156nn,b156nt,b156nf,b156tn,b156tt,b156tf,b156fn,b156ft, b156ff,b234nn,b234nt,b234nf,b234tn,b234tt,b234tf,b234fn, b234ft,b234ff,b235nn,b235nt,b235nf,b235tn,b235tt,b235tf, b235fn,b235ft,b235ff,b236nn,b236nt,b236nf,b236tn,b236tt, b236tf,b236fn,b236ft,b236ff,b245nn,b245nt,b245nf,b245tn, b245tt,b245tf,b245fn,b245ft,b245ff,b246nn,b246nt,b246nf, b246tn,b246tt,b246tf,b246fn,b246ft,b246ff,b256nn,b256nt, b256nf,b256tn,b256tt,b256tf,b256fn,b256ft,b256ff,b345nn, b345nt,b345nf,b345tn,b345tt,b345tf,b345fn,b345ft,b345ff, b346nn,b346nt,b346nf,b346tn,b346tt,b346tf,b346fn,b346ft, b346ff,b356nn,b356nt,b356nf,b356tn,b356tt,b356tf,b356fn, b356ft,b356ff,b456nn,b456nt,b456nf,b456tn,b456tt,b456tf, b456fn,b456ft,b456ff}; Lgreen = { bnnnnn, b012nn,b012nt,b012nf,b012tn,b012tt,b012tf,b012fn,b012ft, b012ff,b013nn,b013nt,b013nf,b013tn,b013tt,b013tf,b013fn, b013ft,b013ff,b014nn,b014nt,b014nf,b014tn,b014tt,b014tf, b014fn,b014ft,b014ff,b015nn,b015nt,b015nf,b015tn,b015tt, b015tf,b015fn,b015ft,b015ff,b016nn,b016nt,b016nf,b016tn, b016tt,b016tf,b016fn,b016ft,b016ff,b023nn,b023nt,b023nf, b023tn,b023tt,b023tf,b023fn,b023ft,b023ff,b024nn,b024nt, b024nf,b024tn,b024tt,b024tf,b024fn,b024ft,b024ff,b025nn, b025nt,b025nf,b025tn,b025tt,b025tf,b025fn,b025ft,b025ff, b026nn,b026nt,b026nf,b026tn,b026tt,b026tf,b026fn,b026ft, b026ff,b034nn,b034nt,b034nf,b034tn,b034tt,b034tf,b034fn, b034ft,b034ff,b035nn,b035nt,b035nf,b035tn,b035tt,b035tf, b035fn,b035ft,b035ff,b036nn,b036nt,b036nf,b036tn,b036tt, b036tf,b036fn,b036ft,b036ff,b045nn,b045nt,b045nf,b045tn, b045tt,b045tf,b045fn,b045ft,b045ff,b046nn,b046nt,b046nf, b046tn,b046tt,b046tf,b046fn,b046ft,b046ff,b056nn,b056nt, b056nf,b056tn,b056tt,b056tf,b056fn,b056ft,b056ff,b123nn, b123nt,b123nf,b123tn,b123tt,b123tf,b123fn,b123ft,b123ff, b124nn,b124nt,b124nf,b124tn,b124tt,b124tf,b124fn,b124ft, b124ff,b125nn,b125nt,b125nf,b125tn,b125tt,b125tf,b125fn, b125ft,b125ff,b126nn,b126nt,b126nf,b126tn,b126tt,b126tf, b126fn,b126ft,b126ff,b134nn,b134nt,b134nf,b134tn,b134tt, b134tf,b134fn,b134ft,b134ff,b135nn,b135nt,b135nf,b135tn, b135tt,b135tf,b135fn,b135ft,b135ff,b136nn,b136nt,b136nf, b136tn,b136tt,b136tf,b136fn,b136ft,b136ff,b145nn,b145nt, b145nf,b145tn,b145tt,b145tf,b145fn,b145ft,b145ff,b146nn, b146nt,b146nf,b146tn,b146tt,b146tf,b146fn,b146ft,b146ff, b156nn,b156nt,b156nf,b156tn,b156tt,b156tf,b156fn,b156ft, b156ff,b234nn,b234nt,b234nf,b234tn,b234tt,b234tf,b234fn, b234ft,b234ff,b235nn,b235nt,b235nf,b235tn,b235tt,b235tf, b235fn,b235ft,b235ff,b236nn,b236nt,b236nf,b236tn,b236tt, b236tf,b236fn,b236ft,b236ff,b245nn,b245nt,b245nf,b245tn, b245tt,b245tf,b245fn,b245ft,b245ff,b246nn,b246nt,b246nf, b246tn,b246tt,b246tf,b246fn,b246ft,b246ff,b256nn,b256nt, b256nf,b256tn,b256tt,b256tf,b256fn,b256ft,b256ff,b345nn, b345nt,b345nf,b345tn,b345tt,b345tf,b345fn,b345ft,b345ff, b346nn,b346nt,b346nf,b346tn,b346tt,b346tf,b346fn,b346ft, b346ff,b356nn,b356nt,b356nf,b356tn,b356tt,b356tf,b356fn, b356ft,b356ff,b456nn,b456nt,b456nf,b456tn,b456tt,b456tf, b456fn,b456ft,b456ff}; Action ={null, Announce}; Protocol: bnnnnn:{null}; b012nn:{null};b012nt:{null};b012nf:{null};b012tn:{null};b012tt:{null}; b012tf:{null};b012fn:{null};b012ft:{null};b012ff:{null};b013nn:{null}; b013nt:{null};b013nf:{null};b013tn:{null};b013tt:{null};b013tf:{null}; b013fn:{null};b013ft:{null};b013ff:{null};b014nn:{null};b014nt:{null}; b014nf:{null};b014tn:{null};b014tt:{null};b014tf:{null};b014fn:{null}; b014ft:{null};b014ff:{null};b015nn:{null};b015nt:{null};b015nf:{null}; b015tn:{null};b015tt:{null};b015tf:{null};b015fn:{null};b015ft:{null}; b015ff:{null};b016nn:{null};b016nt:{null};b016nf:{null};b016tn:{null}; b016tt:{null};b016tf:{null};b016fn:{null};b016ft:{null};b016ff:{null}; b023nn:{null};b023nt:{null};b023nf:{null};b023tn:{null};b023tt:{null}; b023tf:{null};b023fn:{null};b023ft:{null};b023ff:{null};b024nn:{null}; b024nt:{null};b024nf:{null};b024tn:{null};b024tt:{null};b024tf:{null}; b024fn:{null};b024ft:{null};b024ff:{null};b025nn:{null};b025nt:{null}; b025nf:{null};b025tn:{null};b025tt:{null};b025tf:{null};b025fn:{null}; b025ft:{null};b025ff:{null};b026nn:{null};b026nt:{null};b026nf:{null}; b026tn:{null};b026tt:{null};b026tf:{null};b026fn:{null};b026ft:{null}; b026ff:{null};b034nn:{null};b034nt:{null};b034nf:{null};b034tn:{null}; b034tt:{null};b034tf:{null};b034fn:{null};b034ft:{null};b034ff:{null}; b035nn:{null};b035nt:{null};b035nf:{null};b035tn:{null};b035tt:{null}; b035tf:{null};b035fn:{null};b035ft:{null};b035ff:{null};b036nn:{null}; b036nt:{null};b036nf:{null};b036tn:{null};b036tt:{null};b036tf:{null}; b036fn:{null};b036ft:{null};b036ff:{null};b045nn:{null};b045nt:{null}; b045nf:{null};b045tn:{null};b045tt:{null};b045tf:{null};b045fn:{null}; b045ft:{null};b045ff:{null};b046nn:{null};b046nt:{null};b046nf:{null}; b046tn:{null};b046tt:{null};b046tf:{null};b046fn:{null};b046ft:{null}; b046ff:{null};b056nn:{null};b056nt:{null};b056nf:{null};b056tn:{null}; b056tt:{null};b056tf:{null};b056fn:{null};b056ft:{null};b056ff:{null}; b123nn:{null};b123nt:{null};b123nf:{null};b123tn:{null};b123tt:{null}; b123tf:{null};b123fn:{null};b123ft:{null};b123ff:{null};b124nn:{null}; b124nt:{null};b124nf:{null};b124tn:{null};b124tt:{null};b124tf:{null}; b124fn:{null};b124ft:{null};b124ff:{null};b125nn:{null};b125nt:{null}; b125nf:{null};b125tn:{null};b125tt:{null};b125tf:{null};b125fn:{null}; b125ft:{null};b125ff:{null};b126nn:{null};b126nt:{null};b126nf:{null}; b126tn:{null};b126tt:{null};b126tf:{null};b126fn:{null};b126ft:{null}; b126ff:{null};b134nn:{null};b134nt:{null};b134nf:{null};b134tn:{null}; b134tt:{null};b134tf:{null};b134fn:{null};b134ft:{null};b134ff:{null}; b135nn:{null};b135nt:{null};b135nf:{null};b135tn:{null};b135tt:{null}; b135tf:{null};b135fn:{null};b135ft:{null};b135ff:{null};b136nn:{null}; b136nt:{null};b136nf:{null};b136tn:{null};b136tt:{null};b136tf:{null}; b136fn:{null};b136ft:{null};b136ff:{null};b145nn:{null};b145nt:{null}; b145nf:{null};b145tn:{null};b145tt:{null};b145tf:{null};b145fn:{null}; b145ft:{null};b145ff:{null};b146nn:{null};b146nt:{null};b146nf:{null}; b146tn:{null};b146tt:{null};b146tf:{null};b146fn:{null};b146ft:{null}; b146ff:{null};b156nn:{null};b156nt:{null};b156nf:{null};b156tn:{null}; b156tt:{null};b156tf:{null};b156fn:{null};b156ft:{null};b156ff:{null}; b234nn:{null};b234nt:{null};b234nf:{null};b234tn:{null};b234tt:{null}; b234tf:{null};b234fn:{null};b234ft:{null};b234ff:{null};b235nn:{null}; b235nt:{null};b235nf:{null};b235tn:{null};b235tt:{null};b235tf:{null}; b235fn:{null};b235ft:{null};b235ff:{null};b236nn:{null};b236nt:{null}; b236nf:{null};b236tn:{null};b236tt:{null};b236tf:{null};b236fn:{null}; b236ft:{null};b236ff:{null};b245nn:{null};b245nt:{null};b245nf:{null}; b245tn:{null};b245tt:{null};b245tf:{null};b245fn:{null};b245ft:{null}; b245ff:{null};b246nn:{null};b246nt:{null};b246nf:{null};b246tn:{null}; b246tt:{null};b246tf:{null};b246fn:{null};b246ft:{null};b246ff:{null}; b256nn:{null};b256nt:{null};b256nf:{null};b256tn:{null};b256tt:{null}; b256tf:{null};b256fn:{null};b256ft:{null};b256ff:{null};b345nn:{null}; b345nt:{null};b345nf:{null};b345tn:{null};b345tt:{null};b345tf:{null}; b345fn:{null};b345ft:{null};b345ff:{null};b346nn:{null};b346nt:{null}; b346nf:{null};b346tn:{null};b346tt:{null};b346tf:{null};b346fn:{null}; b346ft:{null};b346ff:{null};b356nn:{null};b356nt:{null};b356nf:{null}; b356tn:{null};b356tt:{null};b356tf:{null};b356fn:{null};b356ft:{null}; b356ff:{null};b456nn:{null};b456nt:{null};b456nf:{null};b456tn:{null}; b456tt:{null};b456tf:{null};b456fn:{null};b456ft:{null};b456ff:{null}; end Protocol Ev: -----1 Reveal cards to Bill:bnnnnn->bxxxnn------ b012nn if (Lstate=bnnnnn and ( Env.Lstate=e3450126 or Env.Lstate=e3460125 or Env.Lstate=e3560124 or Env.Lstate=e4560123 )); b013nn if (Lstate=bnnnnn and ( Env.Lstate=e2450136 or Env.Lstate=e2460135 or Env.Lstate=e2560134 or Env.Lstate=e4560132 )); b014nn if (Lstate=bnnnnn and ( Env.Lstate=e2350146 or Env.Lstate=e2360145 or Env.Lstate=e2560143 or Env.Lstate=e3560142 )); b015nn if (Lstate=bnnnnn and ( Env.Lstate=e2340156 or Env.Lstate=e2360154 or Env.Lstate=e2460153 or Env.Lstate=e3460152 )); b016nn if (Lstate=bnnnnn and ( Env.Lstate=e2340165 or Env.Lstate=e2350164 or Env.Lstate=e2450163 or Env.Lstate=e3450162 )); b023nn if (Lstate=bnnnnn and ( Env.Lstate=e1450236 or Env.Lstate=e1460235 or Env.Lstate=e1560234 or Env.Lstate=e4560231 )); b024nn if (Lstate=bnnnnn and ( Env.Lstate=e1350246 or Env.Lstate=e1360245 or Env.Lstate=e1560243 or Env.Lstate=e3560241 )); b025nn if (Lstate=bnnnnn and ( Env.Lstate=e1340256 or Env.Lstate=e1360254 or Env.Lstate=e1460253 or Env.Lstate=e3460251 )); b026nn if (Lstate=bnnnnn and ( Env.Lstate=e1340265 or Env.Lstate=e1350264 or Env.Lstate=e1450263 or Env.Lstate=e3450261 )); b034nn if (Lstate=bnnnnn and ( Env.Lstate=e1250346 or Env.Lstate=e1260345 or Env.Lstate=e1560342 or Env.Lstate=e2560341 )); b035nn if (Lstate=bnnnnn and ( Env.Lstate=e1240356 or Env.Lstate=e1260354 or Env.Lstate=e1460352 or Env.Lstate=e2460351 )); b036nn if (Lstate=bnnnnn and ( Env.Lstate=e1240365 or Env.Lstate=e1250364 or Env.Lstate=e1450362 or Env.Lstate=e2450361 )); b045nn if (Lstate=bnnnnn and ( Env.Lstate=e1230456 or Env.Lstate=e1260453 or Env.Lstate=e1360452 or Env.Lstate=e2360451 )); b046nn if (Lstate=bnnnnn and ( Env.Lstate=e1230465 or Env.Lstate=e1250463 or Env.Lstate=e1350462 or Env.Lstate=e2350461 )); b056nn if (Lstate=bnnnnn and ( Env.Lstate=e1230564 or Env.Lstate=e1240563 or Env.Lstate=e1340562 or Env.Lstate=e2340561 )); b123nn if (Lstate=bnnnnn and ( Env.Lstate=e0451236 or Env.Lstate=e0461235 or Env.Lstate=e0561234 or Env.Lstate=e4561230 )); b124nn if (Lstate=bnnnnn and ( Env.Lstate=e0351246 or Env.Lstate=e0361245 or Env.Lstate=e0561243 or Env.Lstate=e3561240 )); b125nn if (Lstate=bnnnnn and ( Env.Lstate=e0341256 or Env.Lstate=e0361254 or Env.Lstate=e0461253 or Env.Lstate=e3461250 )); b126nn if (Lstate=bnnnnn and ( Env.Lstate=e0341265 or Env.Lstate=e0351264 or Env.Lstate=e0451263 or Env.Lstate=e3451260 )); b134nn if (Lstate=bnnnnn and ( Env.Lstate=e0251346 or Env.Lstate=e0261345 or Env.Lstate=e0561342 or Env.Lstate=e2561340 )); b135nn if (Lstate=bnnnnn and ( Env.Lstate=e0241356 or Env.Lstate=e0261354 or Env.Lstate=e0461352 or Env.Lstate=e2461350 )); b136nn if (Lstate=bnnnnn and ( Env.Lstate=e0241365 or Env.Lstate=e0251364 or Env.Lstate=e0451362 or Env.Lstate=e2451360 )); b145nn if (Lstate=bnnnnn and ( Env.Lstate=e0231456 or Env.Lstate=e0261453 or Env.Lstate=e0361452 or Env.Lstate=e2361450 )); b146nn if (Lstate=bnnnnn and ( Env.Lstate=e0231465 or Env.Lstate=e0251463 or Env.Lstate=e0351462 or Env.Lstate=e2351460 )); b156nn if (Lstate=bnnnnn and ( Env.Lstate=e0231564 or Env.Lstate=e0241563 or Env.Lstate=e0341562 or Env.Lstate=e2341560 )); b234nn if (Lstate=bnnnnn and ( Env.Lstate=e0152346 or Env.Lstate=e0162345 or Env.Lstate=e0562341 or Env.Lstate=e1562340 )); b235nn if (Lstate=bnnnnn and ( Env.Lstate=e0142356 or Env.Lstate=e0162354 or Env.Lstate=e0462351 or Env.Lstate=e1462350 )); b236nn if (Lstate=bnnnnn and ( Env.Lstate=e0142365 or Env.Lstate=e0152364 or Env.Lstate=e0452361 or Env.Lstate=e1452360 )); b245nn if (Lstate=bnnnnn and ( Env.Lstate=e0132456 or Env.Lstate=e0162453 or Env.Lstate=e0362451 or Env.Lstate=e1362450 )); b246nn if (Lstate=bnnnnn and ( Env.Lstate=e0132465 or Env.Lstate=e0152463 or Env.Lstate=e0352461 or Env.Lstate=e1352460 )); b256nn if (Lstate=bnnnnn and ( Env.Lstate=e0132564 or Env.Lstate=e0142563 or Env.Lstate=e0342561 or Env.Lstate=e1342560 )); b345nn if (Lstate=bnnnnn and ( Env.Lstate=e0123456 or Env.Lstate=e0163452 or Env.Lstate=e0263451 or Env.Lstate=e1263450 )); b346nn if (Lstate=bnnnnn and ( Env.Lstate=e0123465 or Env.Lstate=e0153462 or Env.Lstate=e0253461 or Env.Lstate=e1253460 )); b356nn if (Lstate=bnnnnn and ( Env.Lstate=e0123564 or Env.Lstate=e0143562 or Env.Lstate=e0243561 or Env.Lstate=e1243560 )); b456nn if (Lstate=bnnnnn and ( Env.Lstate=e0124563 or Env.Lstate=e0134562 or Env.Lstate=e0234561 or Env.Lstate=e1234560 )); -----2 Anne's Announcement:bxxxnn->bxxxxn------ b012fn if (Lstate=b012nn and ( Env.Lstate=e3450126 or Env.Lstate=e3460125 or Env.Lstate=e3560124 or Env.Lstate=e4560123)); b013tn if (Lstate=b013nn and ( Env.Lstate=e2460135)); b013fn if (Lstate=b013nn and ( Env.Lstate=e2450136 or Env.Lstate=e2560134 or Env.Lstate=e4560132)); b014fn if (Lstate=b014nn and ( Env.Lstate=e2350146 or Env.Lstate=e2360145 or Env.Lstate=e2560143 or Env.Lstate=e3560142)); b015tn if (Lstate=b015nn and ( Env.Lstate=e2460153)); b015fn if (Lstate=b015nn and ( Env.Lstate=e2340156 or Env.Lstate=e2360154 or Env.Lstate=e3460152)); b016fn if (Lstate=b016nn and ( Env.Lstate=e2340165 or Env.Lstate=e2350164 or Env.Lstate=e2450163 or Env.Lstate=e3450162)); b023fn if (Lstate=b023nn and ( Env.Lstate=e1450236 or Env.Lstate=e1460235 or Env.Lstate=e1560234 or Env.Lstate=e4560231)); b024tn if (Lstate=b024nn and ( Env.Lstate=e1350246)); b024fn if (Lstate=b024nn and ( Env.Lstate=e1360245 or Env.Lstate=e1560243 or Env.Lstate=e3560241)); b025fn if (Lstate=b025nn and ( Env.Lstate=e1340256 or Env.Lstate=e1360254 or Env.Lstate=e1460253 or Env.Lstate=e3460251)); b026tn if (Lstate=b026nn and ( Env.Lstate=e1350264)); b026fn if (Lstate=b026nn and ( Env.Lstate=e1340265 or Env.Lstate=e1450263 or Env.Lstate=e3450261)); b034fn if (Lstate=b034nn and ( Env.Lstate=e1250346 or Env.Lstate=e1260345 or Env.Lstate=e1560342 or Env.Lstate=e2560341)); b035tn if (Lstate=b035nn and ( Env.Lstate=e2460351)); b035fn if (Lstate=b035nn and ( Env.Lstate=e1240356 or Env.Lstate=e1260354 or Env.Lstate=e1460352)); b036fn if (Lstate=b036nn and ( Env.Lstate=e1240365 or Env.Lstate=e1250364 or Env.Lstate=e1450362 or Env.Lstate=e2450361)); b045fn if (Lstate=b045nn and ( Env.Lstate=e1230456 or Env.Lstate=e1260453 or Env.Lstate=e1360452 or Env.Lstate=e2360451)); b046tn if (Lstate=b046nn and ( Env.Lstate=e1350462)); b046fn if (Lstate=b046nn and ( Env.Lstate=e1230465 or Env.Lstate=e1250463 or Env.Lstate=e2350461)); b056fn if (Lstate=b056nn and ( Env.Lstate=e1230564 or Env.Lstate=e1240563 or Env.Lstate=e1340562 or Env.Lstate=e2340561)); b123tn if (Lstate=b123nn and ( Env.Lstate=e0561234)); b123fn if (Lstate=b123nn and ( Env.Lstate=e0451236 or Env.Lstate=e0461235 or Env.Lstate=e4561230)); b124tn if (Lstate=b124nn and ( Env.Lstate=e0561243)); b124fn if (Lstate=b124nn and ( Env.Lstate=e0351246 or Env.Lstate=e0361245 or Env.Lstate=e3561240)); b125tn if (Lstate=b125nn and ( Env.Lstate=e0341256)); b125fn if (Lstate=b125nn and ( Env.Lstate=e0361254 or Env.Lstate=e0461253 or Env.Lstate=e3461250)); b126tn if (Lstate=b126nn and ( Env.Lstate=e0341265)); b126fn if (Lstate=b126nn and ( Env.Lstate=e0351264 or Env.Lstate=e0451263 or Env.Lstate=e3451260)); b134tn if (Lstate=b134nn and ( Env.Lstate=e0561342)); b134fn if (Lstate=b134nn and ( Env.Lstate=e0251346 or Env.Lstate=e0261345 or Env.Lstate=e2561340)); b135tn if (Lstate=b135nn and ( Env.Lstate=e2461350)); b135fn if (Lstate=b135nn and ( Env.Lstate=e0241356 or Env.Lstate=e0261354 or Env.Lstate=e0461352)); b136fn if (Lstate=b136nn and ( Env.Lstate=e0241365 or Env.Lstate=e0251364 or Env.Lstate=e0451362 or Env.Lstate=e2451360)); b145fn if (Lstate=b145nn and ( Env.Lstate=e0231456 or Env.Lstate=e0261453 or Env.Lstate=e0361452 or Env.Lstate=e2361450)); b146fn if (Lstate=b146nn and ( Env.Lstate=e0231465 or Env.Lstate=e0251463 or Env.Lstate=e0351462 or Env.Lstate=e2351460)); b156tn if (Lstate=b156nn and ( Env.Lstate=e0341562)); b156fn if (Lstate=b156nn and ( Env.Lstate=e0231564 or Env.Lstate=e0241563 or Env.Lstate=e2341560)); b234tn if (Lstate=b234nn and ( Env.Lstate=e0562341)); b234fn if (Lstate=b234nn and ( Env.Lstate=e0152346 or Env.Lstate=e0162345 or Env.Lstate=e1562340)); b235fn if (Lstate=b235nn and ( Env.Lstate=e0142356 or Env.Lstate=e0162354 or Env.Lstate=e0462351 or Env.Lstate=e1462350)); b236fn if (Lstate=b236nn and ( Env.Lstate=e0142365 or Env.Lstate=e0152364 or Env.Lstate=e0452361 or Env.Lstate=e1452360)); b245fn if (Lstate=b245nn and ( Env.Lstate=e0132456 or Env.Lstate=e0162453 or Env.Lstate=e0362451 or Env.Lstate=e1362450)); b246tn if (Lstate=b246nn and ( Env.Lstate=e1352460)); b246fn if (Lstate=b246nn and ( Env.Lstate=e0132465 or Env.Lstate=e0152463 or Env.Lstate=e0352461)); b256tn if (Lstate=b256nn and ( Env.Lstate=e0342561)); b256fn if (Lstate=b256nn and ( Env.Lstate=e0132564 or Env.Lstate=e0142563 or Env.Lstate=e1342560)); b345tn if (Lstate=b345nn and ( Env.Lstate=e0123456)); b345fn if (Lstate=b345nn and ( Env.Lstate=e0163452 or Env.Lstate=e0263451 or Env.Lstate=e1263450)); b346tn if (Lstate=b346nn and ( Env.Lstate=e0123465)); b346fn if (Lstate=b346nn and ( Env.Lstate=e0153462 or Env.Lstate=e0253461 or Env.Lstate=e1253460)); b356tn if (Lstate=b356nn and ( Env.Lstate=e0123564)); b356fn if (Lstate=b356nn and ( Env.Lstate=e0143562 or Env.Lstate=e0243561 or Env.Lstate=e1243560)); b456tn if (Lstate=b456nn and ( Env.Lstate=e0124563)); b456fn if (Lstate=b456nn and ( Env.Lstate=e0134562 or Env.Lstate=e0234561 or Env.Lstate=e1234560)); -----2 Bill's Announcement:bxxxxn->bxxxxx------ b345tt if (Lstate=b345tn and Env.Lstate=e0123456); b346tf if (Lstate=b346tn and Env.Lstate=e0123465); b356tf if (Lstate=b356tn and Env.Lstate=e0123564); b456tf if (Lstate=b456tn and Env.Lstate=e0124563); b125tt if (Lstate=b125tn and Env.Lstate=e0341256); b126tf if (Lstate=b126tn and Env.Lstate=e0341265); b156tf if (Lstate=b156tn and Env.Lstate=e0341562); b256tf if (Lstate=b256tn and Env.Lstate=e0342561); b123tf if (Lstate=b123tn and Env.Lstate=e0561234); b124tf if (Lstate=b124tn and Env.Lstate=e0561243); b134tf if (Lstate=b134tn and Env.Lstate=e0561342); b234tf if (Lstate=b234tn and Env.Lstate=e0562341); b024tt if (Lstate=b024tn and Env.Lstate=e1350246); b026tf if (Lstate=b026tn and Env.Lstate=e1350264); b046tf if (Lstate=b046tn and Env.Lstate=e1350462); b246tf if (Lstate=b246tn and Env.Lstate=e1352460); b013tf if (Lstate=b013tn and Env.Lstate=e2460135); b015tf if (Lstate=b015tn and Env.Lstate=e2460153); b035tf if (Lstate=b035tn and Env.Lstate=e2460351); b135tf if (Lstate=b135tn and Env.Lstate=e2461350); end Ev end Agent Agent Cath Lstate = { cnnn, c0nn,c0nt,c0nf,c0tn,c0tt,c0tf,c0fn,c0ft, c0ff,c1nn,c1nt,c1nf,c1tn,c1tt,c1tf,c1fn, c1ft,c1ff,c2nn,c2nt,c2nf,c2tn,c2tt,c2tf, c2fn,c2ft,c2ff,c3nn,c3nt,c3nf,c3tn,c3tt, c3tf,c3fn,c3ft,c3ff,c4nn,c4nt,c4nf,c4tn, c4tt,c4tf,c4fn,c4ft,c4ff,c5nn,c5nt,c5nf, c5tn,c5tt,c5tf,c5fn,c5ft,c5ff,c6nn,c6nt, c6nf,c6tn,c6tt,c6tf,c6fn,c6ft,c6ff}; Lgreen = { cnnn, c0nn,c0nt,c0nf,c0tn,c0tt,c0tf,c0fn,c0ft, c0ff,c1nn,c1nt,c1nf,c1tn,c1tt,c1tf,c1fn, c1ft,c1ff,c2nn,c2nt,c2nf,c2tn,c2tt,c2tf, c2fn,c2ft,c2ff,c3nn,c3nt,c3nf,c3tn,c3tt, c3tf,c3fn,c3ft,c3ff,c4nn,c4nt,c4nf,c4tn, c4tt,c4tf,c4fn,c4ft,c4ff,c5nn,c5nt,c5nf, c5tn,c5tt,c5tf,c5fn,c5ft,c5ff,c6nn,c6nt, c6nf,c6tn,c6tt,c6tf,c6fn,c6ft,c6ff}; Action ={null}; Protocol: cnnn:{null}; c0nn:{null};c0nt:{null};c0nf:{null};c0tn:{null};c0tt:{null}; c0tf:{null};c0fn:{null};c0ft:{null};c0ff:{null};c1nn:{null}; c1nt:{null};c1nf:{null};c1tn:{null};c1tt:{null};c1tf:{null}; c1fn:{null};c1ft:{null};c1ff:{null};c2nn:{null};c2nt:{null}; c2nf:{null};c2tn:{null};c2tt:{null};c2tf:{null};c2fn:{null}; c2ft:{null};c2ff:{null};c3nn:{null};c3nt:{null};c3nf:{null}; c3tn:{null};c3tt:{null};c3tf:{null};c3fn:{null};c3ft:{null}; c3ff:{null};c4nn:{null};c4nt:{null};c4nf:{null};c4tn:{null}; c4tt:{null};c4tf:{null};c4fn:{null};c4ft:{null};c4ff:{null}; c5nn:{null};c5nt:{null};c5nf:{null};c5tn:{null};c5tt:{null}; c5tf:{null};c5fn:{null};c5ft:{null};c5ff:{null};c6nn:{null}; c6nt:{null};c6nf:{null};c6tn:{null};c6tt:{null};c6tf:{null}; c6fn:{null};c6ft:{null};c6ff:{null}; end Protocol Ev: -----1 Reveal cards to Cath:cnnn->cxnn------ c0nn if (Lstate=cnnn and ( Env.Lstate=e1234560 or Env.Lstate=e1243560 or Env.Lstate=e1253460 or Env.Lstate=e1263450 or Env.Lstate=e1342560 or Env.Lstate=e1352460 or Env.Lstate=e1362450 or Env.Lstate=e1452360 or Env.Lstate=e1462350 or Env.Lstate=e1562340 or Env.Lstate=e2341560 or Env.Lstate=e2351460 or Env.Lstate=e2361450 or Env.Lstate=e2451360 or Env.Lstate=e2461350 or Env.Lstate=e2561340 or Env.Lstate=e3451260 or Env.Lstate=e3461250 or Env.Lstate=e3561240 or Env.Lstate=e4561230 )); c1nn if (Lstate=cnnn and ( Env.Lstate=e0234561 or Env.Lstate=e0243561 or Env.Lstate=e0253461 or Env.Lstate=e0263451 or Env.Lstate=e0342561 or Env.Lstate=e0352461 or Env.Lstate=e0362451 or Env.Lstate=e0452361 or Env.Lstate=e0462351 or Env.Lstate=e0562341 or Env.Lstate=e2340561 or Env.Lstate=e2350461 or Env.Lstate=e2360451 or Env.Lstate=e2450361 or Env.Lstate=e2460351 or Env.Lstate=e2560341 or Env.Lstate=e3450261 or Env.Lstate=e3460251 or Env.Lstate=e3560241 or Env.Lstate=e4560231 )); c2nn if (Lstate=cnnn and ( Env.Lstate=e0134562 or Env.Lstate=e0143562 or Env.Lstate=e0153462 or Env.Lstate=e0163452 or Env.Lstate=e0341562 or Env.Lstate=e0351462 or Env.Lstate=e0361452 or Env.Lstate=e0451362 or Env.Lstate=e0461352 or Env.Lstate=e0561342 or Env.Lstate=e1340562 or Env.Lstate=e1350462 or Env.Lstate=e1360452 or Env.Lstate=e1450362 or Env.Lstate=e1460352 or Env.Lstate=e1560342 or Env.Lstate=e3450162 or Env.Lstate=e3460152 or Env.Lstate=e3560142 or Env.Lstate=e4560132 )); c3nn if (Lstate=cnnn and ( Env.Lstate=e0124563 or Env.Lstate=e0142563 or Env.Lstate=e0152463 or Env.Lstate=e0162453 or Env.Lstate=e0241563 or Env.Lstate=e0251463 or Env.Lstate=e0261453 or Env.Lstate=e0451263 or Env.Lstate=e0461253 or Env.Lstate=e0561243 or Env.Lstate=e1240563 or Env.Lstate=e1250463 or Env.Lstate=e1260453 or Env.Lstate=e1450263 or Env.Lstate=e1460253 or Env.Lstate=e1560243 or Env.Lstate=e2450163 or Env.Lstate=e2460153 or Env.Lstate=e2560143 or Env.Lstate=e4560123 )); c4nn if (Lstate=cnnn and ( Env.Lstate=e0123564 or Env.Lstate=e0132564 or Env.Lstate=e0152364 or Env.Lstate=e0162354 or Env.Lstate=e0231564 or Env.Lstate=e0251364 or Env.Lstate=e0261354 or Env.Lstate=e0351264 or Env.Lstate=e0361254 or Env.Lstate=e0561234 or Env.Lstate=e1230564 or Env.Lstate=e1250364 or Env.Lstate=e1260354 or Env.Lstate=e1350264 or Env.Lstate=e1360254 or Env.Lstate=e1560234 or Env.Lstate=e2350164 or Env.Lstate=e2360154 or Env.Lstate=e2560134 or Env.Lstate=e3560124 )); c5nn if (Lstate=cnnn and ( Env.Lstate=e0123465 or Env.Lstate=e0132465 or Env.Lstate=e0142365 or Env.Lstate=e0162345 or Env.Lstate=e0231465 or Env.Lstate=e0241365 or Env.Lstate=e0261345 or Env.Lstate=e0341265 or Env.Lstate=e0361245 or Env.Lstate=e0461235 or Env.Lstate=e1230465 or Env.Lstate=e1240365 or Env.Lstate=e1260345 or Env.Lstate=e1340265 or Env.Lstate=e1360245 or Env.Lstate=e1460235 or Env.Lstate=e2340165 or Env.Lstate=e2360145 or Env.Lstate=e2460135 or Env.Lstate=e3460125 )); c6nn if (Lstate=cnnn and ( Env.Lstate=e0123456 or Env.Lstate=e0132456 or Env.Lstate=e0142356 or Env.Lstate=e0152346 or Env.Lstate=e0231456 or Env.Lstate=e0241356 or Env.Lstate=e0251346 or Env.Lstate=e0341256 or Env.Lstate=e0351246 or Env.Lstate=e0451236 or Env.Lstate=e1230456 or Env.Lstate=e1240356 or Env.Lstate=e1250346 or Env.Lstate=e1340256 or Env.Lstate=e1350246 or Env.Lstate=e1450236 or Env.Lstate=e2340156 or Env.Lstate=e2350146 or Env.Lstate=e2450136 or Env.Lstate=e3450126 )); -----2 Anne's Announcement:cxnn->cxxn------ c0tn if (Lstate=c0nn and ( Env.Lstate=e1352460 or Env.Lstate=e2461350)); c0fn if (Lstate=c0nn and ( Env.Lstate=e1234560 or Env.Lstate=e1243560 or Env.Lstate=e1253460 or Env.Lstate=e1263450 or Env.Lstate=e1342560 or Env.Lstate=e1362450 or Env.Lstate=e1452360 or Env.Lstate=e1462350 or Env.Lstate=e1562340 or Env.Lstate=e2341560 or Env.Lstate=e2351460 or Env.Lstate=e2361450 or Env.Lstate=e2451360 or Env.Lstate=e2561340 or Env.Lstate=e3451260 or Env.Lstate=e3461250 or Env.Lstate=e3561240 or Env.Lstate=e4561230)); c1tn if (Lstate=c1nn and ( Env.Lstate=e0342561 or Env.Lstate=e0562341 or Env.Lstate=e2460351)); c1fn if (Lstate=c1nn and ( Env.Lstate=e0234561 or Env.Lstate=e0243561 or Env.Lstate=e0253461 or Env.Lstate=e0263451 or Env.Lstate=e0352461 or Env.Lstate=e0362451 or Env.Lstate=e0452361 or Env.Lstate=e0462351 or Env.Lstate=e2340561 or Env.Lstate=e2350461 or Env.Lstate=e2360451 or Env.Lstate=e2450361 or Env.Lstate=e2560341 or Env.Lstate=e3450261 or Env.Lstate=e3460251 or Env.Lstate=e3560241 or Env.Lstate=e4560231)); c2tn if (Lstate=c2nn and ( Env.Lstate=e0341562 or Env.Lstate=e0561342 or Env.Lstate=e1350462)); c2fn if (Lstate=c2nn and ( Env.Lstate=e0134562 or Env.Lstate=e0143562 or Env.Lstate=e0153462 or Env.Lstate=e0163452 or Env.Lstate=e0351462 or Env.Lstate=e0361452 or Env.Lstate=e0451362 or Env.Lstate=e0461352 or Env.Lstate=e1340562 or Env.Lstate=e1360452 or Env.Lstate=e1450362 or Env.Lstate=e1460352 or Env.Lstate=e1560342 or Env.Lstate=e3450162 or Env.Lstate=e3460152 or Env.Lstate=e3560142 or Env.Lstate=e4560132)); c3tn if (Lstate=c3nn and ( Env.Lstate=e0124563 or Env.Lstate=e0561243 or Env.Lstate=e2460153)); c3fn if (Lstate=c3nn and ( Env.Lstate=e0142563 or Env.Lstate=e0152463 or Env.Lstate=e0162453 or Env.Lstate=e0241563 or Env.Lstate=e0251463 or Env.Lstate=e0261453 or Env.Lstate=e0451263 or Env.Lstate=e0461253 or Env.Lstate=e1240563 or Env.Lstate=e1250463 or Env.Lstate=e1260453 or Env.Lstate=e1450263 or Env.Lstate=e1460253 or Env.Lstate=e1560243 or Env.Lstate=e2450163 or Env.Lstate=e2560143 or Env.Lstate=e4560123)); c4tn if (Lstate=c4nn and ( Env.Lstate=e0123564 or Env.Lstate=e0561234 or Env.Lstate=e1350264)); c4fn if (Lstate=c4nn and ( Env.Lstate=e0132564 or Env.Lstate=e0152364 or Env.Lstate=e0162354 or Env.Lstate=e0231564 or Env.Lstate=e0251364 or Env.Lstate=e0261354 or Env.Lstate=e0351264 or Env.Lstate=e0361254 or Env.Lstate=e1230564 or Env.Lstate=e1250364 or Env.Lstate=e1260354 or Env.Lstate=e1360254 or Env.Lstate=e1560234 or Env.Lstate=e2350164 or Env.Lstate=e2360154 or Env.Lstate=e2560134 or Env.Lstate=e3560124)); c5tn if (Lstate=c5nn and ( Env.Lstate=e0123465 or Env.Lstate=e0341265 or Env.Lstate=e2460135)); c5fn if (Lstate=c5nn and ( Env.Lstate=e0132465 or Env.Lstate=e0142365 or Env.Lstate=e0162345 or Env.Lstate=e0231465 or Env.Lstate=e0241365 or Env.Lstate=e0261345 or Env.Lstate=e0361245 or Env.Lstate=e0461235 or Env.Lstate=e1230465 or Env.Lstate=e1240365 or Env.Lstate=e1260345 or Env.Lstate=e1340265 or Env.Lstate=e1360245 or Env.Lstate=e1460235 or Env.Lstate=e2340165 or Env.Lstate=e2360145 or Env.Lstate=e3460125)); c6tn if (Lstate=c6nn and ( Env.Lstate=e0123456 or Env.Lstate=e0341256 or Env.Lstate=e1350246)); c6fn if (Lstate=c6nn and ( Env.Lstate=e0132456 or Env.Lstate=e0142356 or Env.Lstate=e0152346 or Env.Lstate=e0231456 or Env.Lstate=e0241356 or Env.Lstate=e0251346 or Env.Lstate=e0351246 or Env.Lstate=e0451236 or Env.Lstate=e1230456 or Env.Lstate=e1240356 or Env.Lstate=e1250346 or Env.Lstate=e1340256 or Env.Lstate=e1450236 or Env.Lstate=e2340156 or Env.Lstate=e2350146 or Env.Lstate=e2450136 or Env.Lstate=e3450126)); -----2 Bill's Announcement:cxxn->cxxx------ c0tf if (Lstate=c0tn); c1tf if (Lstate=c1tn); c2tf if (Lstate=c2tn); c3tf if (Lstate=c3tn); c4tf if (Lstate=c4tn); c5tf if (Lstate=c5tn); c6tt if (Lstate=c6tn); end Ev end Agent Agent Env Lstate={ --Introduce 7 variables for the card deal e0123456,e0123465,e0123564,e0124563,e0132456,e0132465, e0132564,e0134562,e0142356,e0142365,e0142563,e0143562, e0152346,e0152364,e0152463,e0153462,e0162345,e0162354, e0162453,e0163452,e0231456,e0231465,e0231564,e0234561, e0241356,e0241365,e0241563,e0243561,e0251346,e0251364, e0251463,e0253461,e0261345,e0261354,e0261453,e0263451, e0341256,e0341265,e0341562,e0342561,e0351246,e0351264, e0351462,e0352461,e0361245,e0361254,e0361452,e0362451, e0451236,e0451263,e0451362,e0452361,e0461235,e0461253, e0461352,e0462351,e0561234,e0561243,e0561342,e0562341, e1230456,e1230465,e1230564,e1234560,e1240356,e1240365, e1240563,e1243560,e1250346,e1250364,e1250463,e1253460, e1260345,e1260354,e1260453,e1263450,e1340256,e1340265, e1340562,e1342560,e1350246,e1350264,e1350462,e1352460, e1360245,e1360254,e1360452,e1362450,e1450236,e1450263, e1450362,e1452360,e1460235,e1460253,e1460352,e1462350, e1560234,e1560243,e1560342,e1562340,e2340156,e2340165, e2340561,e2341560,e2350146,e2350164,e2350461,e2351460, e2360145,e2360154,e2360451,e2361450,e2450136,e2450163, e2450361,e2451360,e2460135,e2460153,e2460351,e2461350, e2560134,e2560143,e2560341,e2561340,e3450126,e3450162, e3450261,e3451260,e3460125,e3460152,e3460251,e3461250, e3560124,e3560142,e3560241,e3561240,e4560123,e4560132, e4560231,e4561230}; Lgreen={ e0123456,e0123465,e0123564,e0124563,e0132456,e0132465, e0132564,e0134562,e0142356,e0142365,e0142563,e0143562, e0152346,e0152364,e0152463,e0153462,e0162345,e0162354, e0162453,e0163452,e0231456,e0231465,e0231564,e0234561, e0241356,e0241365,e0241563,e0243561,e0251346,e0251364, e0251463,e0253461,e0261345,e0261354,e0261453,e0263451, e0341256,e0341265,e0341562,e0342561,e0351246,e0351264, e0351462,e0352461,e0361245,e0361254,e0361452,e0362451, e0451236,e0451263,e0451362,e0452361,e0461235,e0461253, e0461352,e0462351,e0561234,e0561243,e0561342,e0562341, e1230456,e1230465,e1230564,e1234560,e1240356,e1240365, e1240563,e1243560,e1250346,e1250364,e1250463,e1253460, e1260345,e1260354,e1260453,e1263450,e1340256,e1340265, e1340562,e1342560,e1350246,e1350264,e1350462,e1352460, e1360245,e1360254,e1360452,e1362450,e1450236,e1450263, e1450362,e1452360,e1460235,e1460253,e1460352,e1462350, e1560234,e1560243,e1560342,e1562340,e2340156,e2340165, e2340561,e2341560,e2350146,e2350164,e2350461,e2351460, e2360145,e2360154,e2360451,e2361450,e2450136,e2450163, e2450361,e2451360,e2460135,e2460153,e2460351,e2461350, e2560134,e2560143,e2560341,e2561340,e3450126,e3450162, e3450261,e3451260,e3460125,e3460152,e3460251,e3461250, e3560124,e3560142,e3560241,e3561240,e4560123,e4560132, e4560231,e4561230}; Action={null}; Protocol: e0123456:{null};e0123465:{null};e0123564:{null};e0124563:{null}; e0132456:{null};e0132465:{null};e0132564:{null};e0134562:{null}; e0142356:{null};e0142365:{null};e0142563:{null};e0143562:{null}; e0152346:{null};e0152364:{null};e0152463:{null};e0153462:{null}; e0162345:{null};e0162354:{null};e0162453:{null};e0163452:{null}; e0231456:{null};e0231465:{null};e0231564:{null};e0234561:{null}; e0241356:{null};e0241365:{null};e0241563:{null};e0243561:{null}; e0251346:{null};e0251364:{null};e0251463:{null};e0253461:{null}; e0261345:{null};e0261354:{null};e0261453:{null};e0263451:{null}; e0341256:{null};e0341265:{null};e0341562:{null};e0342561:{null}; e0351246:{null};e0351264:{null};e0351462:{null};e0352461:{null}; e0361245:{null};e0361254:{null};e0361452:{null};e0362451:{null}; e0451236:{null};e0451263:{null};e0451362:{null};e0452361:{null}; e0461235:{null};e0461253:{null};e0461352:{null};e0462351:{null}; e0561234:{null};e0561243:{null};e0561342:{null};e0562341:{null}; e1230456:{null};e1230465:{null};e1230564:{null};e1234560:{null}; e1240356:{null};e1240365:{null};e1240563:{null};e1243560:{null}; e1250346:{null};e1250364:{null};e1250463:{null};e1253460:{null}; e1260345:{null};e1260354:{null};e1260453:{null};e1263450:{null}; e1340256:{null};e1340265:{null};e1340562:{null};e1342560:{null}; e1350246:{null};e1350264:{null};e1350462:{null};e1352460:{null}; e1360245:{null};e1360254:{null};e1360452:{null};e1362450:{null}; e1450236:{null};e1450263:{null};e1450362:{null};e1452360:{null}; e1460235:{null};e1460253:{null};e1460352:{null};e1462350:{null}; e1560234:{null};e1560243:{null};e1560342:{null};e1562340:{null}; e2340156:{null};e2340165:{null};e2340561:{null};e2341560:{null}; e2350146:{null};e2350164:{null};e2350461:{null};e2351460:{null}; e2360145:{null};e2360154:{null};e2360451:{null};e2361450:{null}; e2450136:{null};e2450163:{null};e2450361:{null};e2451360:{null}; e2460135:{null};e2460153:{null};e2460351:{null};e2461350:{null}; e2560134:{null};e2560143:{null};e2560341:{null};e2561340:{null}; e3450126:{null};e3450162:{null};e3450261:{null};e3451260:{null}; e3460125:{null};e3460152:{null};e3460251:{null};e3461250:{null}; e3560124:{null};e3560142:{null};e3560241:{null};e3561240:{null}; e4560123:{null};e4560132:{null};e4560231:{null};e4561230:{null}; end Protocol Ev: e0123456 if (Lstate=e0123456); e0123465 if (Lstate=e0123465); e0123564 if (Lstate=e0123564); e0124563 if (Lstate=e0124563); e0132456 if (Lstate=e0132456); e0132465 if (Lstate=e0132465); e0132564 if (Lstate=e0132564); e0134562 if (Lstate=e0134562); e0142356 if (Lstate=e0142356); e0142365 if (Lstate=e0142365); e0142563 if (Lstate=e0142563); e0143562 if (Lstate=e0143562); e0152346 if (Lstate=e0152346); e0152364 if (Lstate=e0152364); e0152463 if (Lstate=e0152463); e0153462 if (Lstate=e0153462); e0162345 if (Lstate=e0162345); e0162354 if (Lstate=e0162354); e0162453 if (Lstate=e0162453); e0163452 if (Lstate=e0163452); e0231456 if (Lstate=e0231456); e0231465 if (Lstate=e0231465); e0231564 if (Lstate=e0231564); e0234561 if (Lstate=e0234561); e0241356 if (Lstate=e0241356); e0241365 if (Lstate=e0241365); e0241563 if (Lstate=e0241563); e0243561 if (Lstate=e0243561); e0251346 if (Lstate=e0251346); e0251364 if (Lstate=e0251364); e0251463 if (Lstate=e0251463); e0253461 if (Lstate=e0253461); e0261345 if (Lstate=e0261345); e0261354 if (Lstate=e0261354); e0261453 if (Lstate=e0261453); e0263451 if (Lstate=e0263451); e0341256 if (Lstate=e0341256); e0341265 if (Lstate=e0341265); e0341562 if (Lstate=e0341562); e0342561 if (Lstate=e0342561); e0351246 if (Lstate=e0351246); e0351264 if (Lstate=e0351264); e0351462 if (Lstate=e0351462); e0352461 if (Lstate=e0352461); e0361245 if (Lstate=e0361245); e0361254 if (Lstate=e0361254); e0361452 if (Lstate=e0361452); e0362451 if (Lstate=e0362451); e0451236 if (Lstate=e0451236); e0451263 if (Lstate=e0451263); e0451362 if (Lstate=e0451362); e0452361 if (Lstate=e0452361); e0461235 if (Lstate=e0461235); e0461253 if (Lstate=e0461253); e0461352 if (Lstate=e0461352); e0462351 if (Lstate=e0462351); e0561234 if (Lstate=e0561234); e0561243 if (Lstate=e0561243); e0561342 if (Lstate=e0561342); e0562341 if (Lstate=e0562341); e1230456 if (Lstate=e1230456); e1230465 if (Lstate=e1230465); e1230564 if (Lstate=e1230564); e1234560 if (Lstate=e1234560); e1240356 if (Lstate=e1240356); e1240365 if (Lstate=e1240365); e1240563 if (Lstate=e1240563); e1243560 if (Lstate=e1243560); e1250346 if (Lstate=e1250346); e1250364 if (Lstate=e1250364); e1250463 if (Lstate=e1250463); e1253460 if (Lstate=e1253460); e1260345 if (Lstate=e1260345); e1260354 if (Lstate=e1260354); e1260453 if (Lstate=e1260453); e1263450 if (Lstate=e1263450); c6fn if (Lstate=c6nn and ( Env.Lstate=e0132456 or Env.Lstate=e0142356 or Env.Lstate=e0152346 or Env.Lstate=e0231456 or Env.Lstate=e0241356 or Env.Lstate=e0251346 or Env.Lstate=e0351246 or Env.Lstate=e0451236 or Env.Lstate=e1230456 or Env.Lstate=e1240356 or Env.Lstate=e1250346 or Env.Lstate=e1340256 or Env.Lstate=e1450236 or Env.Lstate=e2340156 or Env.Lstate=e2350146 or Env.Lstate=e2450136 or Env.Lstate=e3450126)); e1340256 if (Lstate=e1340256); e1340265 if (Lstate=e1340265); e1340562 if (Lstate=e1340562); e1342560 if (Lstate=e1342560); e1350246 if (Lstate=e1350246); e1350264 if (Lstate=e1350264); e1350462 if (Lstate=e1350462); e1352460 if (Lstate=e1352460); e1360245 if (Lstate=e1360245); e1360254 if (Lstate=e1360254); e1360452 if (Lstate=e1360452); e1362450 if (Lstate=e1362450); e1450236 if (Lstate=e1450236); e1450263 if (Lstate=e1450263); e1450362 if (Lstate=e1450362); e1452360 if (Lstate=e1452360); e1460235 if (Lstate=e1460235); e1460253 if (Lstate=e1460253); e1460352 if (Lstate=e1460352); e1462350 if (Lstate=e1462350); e1560234 if (Lstate=e1560234); e1560243 if (Lstate=e1560243); e1560342 if (Lstate=e1560342); e1562340 if (Lstate=e1562340); e2340156 if (Lstate=e2340156); e2340165 if (Lstate=e2340165); e2340561 if (Lstate=e2340561); e2341560 if (Lstate=e2341560); e2350146 if (Lstate=e2350146); e2350164 if (Lstate=e2350164); e2350461 if (Lstate=e2350461); e2351460 if (Lstate=e2351460); e2360145 if (Lstate=e2360145); e2360154 if (Lstate=e2360154); e2360451 if (Lstate=e2360451); c6fn if (Lstate=c6nn and ( Env.Lstate=e0132456 or Env.Lstate=e0142356 or Env.Lstate=e0152346 or Env.Lstate=e0231456 or Env.Lstate=e0241356 or Env.Lstate=e0251346 or Env.Lstate=e0351246 or Env.Lstate=e0451236 or Env.Lstate=e1230456 or Env.Lstate=e1240356 or Env.Lstate=e1250346 or Env.Lstate=e1340256 or Env.Lstate=e1450236 or Env.Lstate=e2340156 or Env.Lstate=e2350146 or Env.Lstate=e2450136 or Env.Lstate=e3450126)); e2361450 if (Lstate=e2361450); e2450136 if (Lstate=e2450136); e2450163 if (Lstate=e2450163); e2450361 if (Lstate=e2450361); e2451360 if (Lstate=e2451360); e2460135 if (Lstate=e2460135); e2460153 if (Lstate=e2460153); e2460351 if (Lstate=e2460351); e2461350 if (Lstate=e2461350); e2560134 if (Lstate=e2560134); e2560143 if (Lstate=e2560143); e2560341 if (Lstate=e2560341); e2561340 if (Lstate=e2561340); e3450126 if (Lstate=e3450126); e3450162 if (Lstate=e3450162); e3450261 if (Lstate=e3450261); e3451260 if (Lstate=e3451260); e3460125 if (Lstate=e3460125); e3460152 if (Lstate=e3460152); e3460251 if (Lstate=e3460251); e3461250 if (Lstate=e3461250); e3560124 if (Lstate=e3560124); e3560142 if (Lstate=e3560142); e3560241 if (Lstate=e3560241); e3561240 if (Lstate=e3561240); e4560123 if (Lstate=e4560123); e4560132 if (Lstate=e4560132); e4560231 if (Lstate=e4560231); e4561230 if (Lstate=e4561230); end Ev end Agent Evaluation a0 if ( Env.Lstate = e0123456 or Env.Lstate = e0123465 or Env.Lstate = e0123564 or Env.Lstate = e0124563 or Env.Lstate = e0132456 or Env.Lstate = e0132465 or Env.Lstate = e0132564 or Env.Lstate = e0134562 or Env.Lstate = e0142356 or Env.Lstate = e0142365 or Env.Lstate = e0142563 or Env.Lstate = e0143562 or Env.Lstate = e0152346 or Env.Lstate = e0152364 or Env.Lstate = e0152463 or Env.Lstate = e0153462 or Env.Lstate = e0162345 or Env.Lstate = e0162354 or Env.Lstate = e0162453 or Env.Lstate = e0163452 or Env.Lstate = e0231456 or Env.Lstate = e0231465 or Env.Lstate = e0231564 or Env.Lstate = e0234561 or Env.Lstate = e0241356 or Env.Lstate = e0241365 or Env.Lstate = e0241563 or Env.Lstate = e0243561 or Env.Lstate = e0251346 or Env.Lstate = e0251364 or Env.Lstate = e0251463 or Env.Lstate = e0253461 or Env.Lstate = e0261345 or Env.Lstate = e0261354 or Env.Lstate = e0261453 or Env.Lstate = e0263451 or Env.Lstate = e0341256 or Env.Lstate = e0341265 or Env.Lstate = e0341562 or Env.Lstate = e0342561 or Env.Lstate = e0351246 or Env.Lstate = e0351264 or Env.Lstate = e0351462 or Env.Lstate = e0352461 or Env.Lstate = e0361245 or Env.Lstate = e0361254 or Env.Lstate = e0361452 or Env.Lstate = e0362451 or Env.Lstate = e0451236 or Env.Lstate = e0451263 or Env.Lstate = e0451362 or Env.Lstate = e0452361 or Env.Lstate = e0461235 or Env.Lstate = e0461253 or Env.Lstate = e0461352 or Env.Lstate = e0462351 or Env.Lstate = e0561234 or Env.Lstate = e0561243 or Env.Lstate = e0561342 or Env.Lstate = e0562341); a1 if ( Env.Lstate = e0123456 or Env.Lstate = e0123465 or Env.Lstate = e0123564 or Env.Lstate = e0124563 or Env.Lstate = e0132456 or Env.Lstate = e0132465 or Env.Lstate = e0132564 or Env.Lstate = e0134562 or Env.Lstate = e0142356 or Env.Lstate = e0142365 or Env.Lstate = e0142563 or Env.Lstate = e0143562 or Env.Lstate = e0152346 or Env.Lstate = e0152364 or Env.Lstate = e0152463 or Env.Lstate = e0153462 or Env.Lstate = e0162345 or Env.Lstate = e0162354 or Env.Lstate = e0162453 or Env.Lstate = e0163452 or Env.Lstate = e1230456 or Env.Lstate = e1230465 or Env.Lstate = e1230564 or Env.Lstate = e1234560 or Env.Lstate = e1240356 or Env.Lstate = e1240365 or Env.Lstate = e1240563 or Env.Lstate = e1243560 or Env.Lstate = e1250346 or Env.Lstate = e1250364 or Env.Lstate = e1250463 or Env.Lstate = e1253460 or Env.Lstate = e1260345 or Env.Lstate = e1260354 or Env.Lstate = e1260453 or Env.Lstate = e1263450 or Env.Lstate = e1340256 or Env.Lstate = e1340265 or Env.Lstate = e1340562 or Env.Lstate = e1342560 or Env.Lstate = e1350246 or Env.Lstate = e1350264 or Env.Lstate = e1350462 or Env.Lstate = e1352460 or Env.Lstate = e1360245 or Env.Lstate = e1360254 or Env.Lstate = e1360452 or Env.Lstate = e1362450 or Env.Lstate = e1450236 or Env.Lstate = e1450263 or Env.Lstate = e1450362 or Env.Lstate = e1452360 or Env.Lstate = e1460235 or Env.Lstate = e1460253 or Env.Lstate = e1460352 or Env.Lstate = e1462350 or Env.Lstate = e1560234 or Env.Lstate = e1560243 or Env.Lstate = e1560342 or Env.Lstate = e1562340); a2 if ( Env.Lstate = e0123456 or Env.Lstate = e0123465 or Env.Lstate = e0123564 or Env.Lstate = e0124563 or Env.Lstate = e0231456 or Env.Lstate = e0231465 or Env.Lstate = e0231564 or Env.Lstate = e0234561 or Env.Lstate = e0241356 or Env.Lstate = e0241365 or Env.Lstate = e0241563 or Env.Lstate = e0243561 or Env.Lstate = e0251346 or Env.Lstate = e0251364 or Env.Lstate = e0251463 or Env.Lstate = e0253461 or Env.Lstate = e0261345 or Env.Lstate = e0261354 or Env.Lstate = e0261453 or Env.Lstate = e0263451 or Env.Lstate = e1230456 or Env.Lstate = e1230465 or Env.Lstate = e1230564 or Env.Lstate = e1234560 or Env.Lstate = e1240356 or Env.Lstate = e1240365 or Env.Lstate = e1240563 or Env.Lstate = e1243560 or Env.Lstate = e1250346 or Env.Lstate = e1250364 or Env.Lstate = e1250463 or Env.Lstate = e1253460 or Env.Lstate = e1260345 or Env.Lstate = e1260354 or Env.Lstate = e1260453 or Env.Lstate = e1263450 or Env.Lstate = e2340156 or Env.Lstate = e2340165 or Env.Lstate = e2340561 or Env.Lstate = e2341560 or Env.Lstate = e2350146 or Env.Lstate = e2350164 or Env.Lstate = e2350461 or Env.Lstate = e2351460 or Env.Lstate = e2360145 or Env.Lstate = e2360154 or Env.Lstate = e2360451 or Env.Lstate = e2361450 or Env.Lstate = e2450136 or Env.Lstate = e2450163 or Env.Lstate = e2450361 or Env.Lstate = e2451360 or Env.Lstate = e2460135 or Env.Lstate = e2460153 or Env.Lstate = e2460351 or Env.Lstate = e2461350 or Env.Lstate = e2560134 or Env.Lstate = e2560143 or Env.Lstate = e2560341 or Env.Lstate = e2561340); a3 if ( Env.Lstate = e0132456 or Env.Lstate = e0132465 or Env.Lstate = e0132564 or Env.Lstate = e0134562 or Env.Lstate = e0231456 or Env.Lstate = e0231465 or Env.Lstate = e0231564 or Env.Lstate = e0234561 or Env.Lstate = e0341256 or Env.Lstate = e0341265 or Env.Lstate = e0341562 or Env.Lstate = e0342561 or Env.Lstate = e0351246 or Env.Lstate = e0351264 or Env.Lstate = e0351462 or Env.Lstate = e0352461 or Env.Lstate = e0361245 or Env.Lstate = e0361254 or Env.Lstate = e0361452 or Env.Lstate = e0362451 or Env.Lstate = e1230456 or Env.Lstate = e1230465 or Env.Lstate = e1230564 or Env.Lstate = e1234560 or Env.Lstate = e1340256 or Env.Lstate = e1340265 or Env.Lstate = e1340562 or Env.Lstate = e1342560 or Env.Lstate = e1350246 or Env.Lstate = e1350264 or Env.Lstate = e1350462 or Env.Lstate = e1352460 or Env.Lstate = e1360245 or Env.Lstate = e1360254 or Env.Lstate = e1360452 or Env.Lstate = e1362450 or Env.Lstate = e2340156 or Env.Lstate = e2340165 or Env.Lstate = e2340561 or Env.Lstate = e2341560 or Env.Lstate = e2350146 or Env.Lstate = e2350164 or Env.Lstate = e2350461 or Env.Lstate = e2351460 or Env.Lstate = e2360145 or Env.Lstate = e2360154 or Env.Lstate = e2360451 or Env.Lstate = e2361450 or Env.Lstate = e3450126 or Env.Lstate = e3450162 or Env.Lstate = e3450261 or Env.Lstate = e3451260 or Env.Lstate = e3460125 or Env.Lstate = e3460152 or Env.Lstate = e3460251 or Env.Lstate = e3461250 or Env.Lstate = e3560124 or Env.Lstate = e3560142 or Env.Lstate = e3560241 or Env.Lstate = e3561240); a4 if ( Env.Lstate = e0142356 or Env.Lstate = e0142365 or Env.Lstate = e0142563 or Env.Lstate = e0143562 or Env.Lstate = e0241356 or Env.Lstate = e0241365 or Env.Lstate = e0241563 or Env.Lstate = e0243561 or Env.Lstate = e0341256 or Env.Lstate = e0341265 or Env.Lstate = e0341562 or Env.Lstate = e0342561 or Env.Lstate = e0451236 or Env.Lstate = e0451263 or Env.Lstate = e0451362 or Env.Lstate = e0452361 or Env.Lstate = e0461235 or Env.Lstate = e0461253 or Env.Lstate = e0461352 or Env.Lstate = e0462351 or Env.Lstate = e1240356 or Env.Lstate = e1240365 or Env.Lstate = e1240563 or Env.Lstate = e1243560 or Env.Lstate = e1340256 or Env.Lstate = e1340265 or Env.Lstate = e1340562 or Env.Lstate = e1342560 or Env.Lstate = e1450236 or Env.Lstate = e1450263 or Env.Lstate = e1450362 or Env.Lstate = e1452360 or Env.Lstate = e1460235 or Env.Lstate = e1460253 or Env.Lstate = e1460352 or Env.Lstate = e1462350 or Env.Lstate = e2340156 or Env.Lstate = e2340165 or Env.Lstate = e2340561 or Env.Lstate = e2341560 or Env.Lstate = e2450136 or Env.Lstate = e2450163 or Env.Lstate = e2450361 or Env.Lstate = e2451360 or Env.Lstate = e2460135 or Env.Lstate = e2460153 or Env.Lstate = e2460351 or Env.Lstate = e2461350 or Env.Lstate = e3450126 or Env.Lstate = e3450162 or Env.Lstate = e3450261 or Env.Lstate = e3451260 or Env.Lstate = e3460125 or Env.Lstate = e3460152 or Env.Lstate = e3460251 or Env.Lstate = e3461250 or Env.Lstate = e4560123 or Env.Lstate = e4560132 or Env.Lstate = e4560231 or Env.Lstate = e4561230); a5 if ( Env.Lstate = e0152346 or Env.Lstate = e0152364 or Env.Lstate = e0152463 or Env.Lstate = e0153462 or Env.Lstate = e0251346 or Env.Lstate = e0251364 or Env.Lstate = e0251463 or Env.Lstate = e0253461 or Env.Lstate = e0351246 or Env.Lstate = e0351264 or Env.Lstate = e0351462 or Env.Lstate = e0352461 or Env.Lstate = e0451236 or Env.Lstate = e0451263 or Env.Lstate = e0451362 or Env.Lstate = e0452361 or Env.Lstate = e0561234 or Env.Lstate = e0561243 or Env.Lstate = e0561342 or Env.Lstate = e0562341 or Env.Lstate = e1250346 or Env.Lstate = e1250364 or Env.Lstate = e1250463 or Env.Lstate = e1253460 or Env.Lstate = e1350246 or Env.Lstate = e1350264 or Env.Lstate = e1350462 or Env.Lstate = e1352460 or Env.Lstate = e1450236 or Env.Lstate = e1450263 or Env.Lstate = e1450362 or Env.Lstate = e1452360 or Env.Lstate = e1560234 or Env.Lstate = e1560243 or Env.Lstate = e1560342 or Env.Lstate = e1562340 or Env.Lstate = e2350146 or Env.Lstate = e2350164 or Env.Lstate = e2350461 or Env.Lstate = e2351460 or Env.Lstate = e2450136 or Env.Lstate = e2450163 or Env.Lstate = e2450361 or Env.Lstate = e2451360 or Env.Lstate = e2560134 or Env.Lstate = e2560143 or Env.Lstate = e2560341 or Env.Lstate = e2561340 or Env.Lstate = e3450126 or Env.Lstate = e3450162 or Env.Lstate = e3450261 or Env.Lstate = e3451260 or Env.Lstate = e3560124 or Env.Lstate = e3560142 or Env.Lstate = e3560241 or Env.Lstate = e3561240 or Env.Lstate = e4560123 or Env.Lstate = e4560132 or Env.Lstate = e4560231 or Env.Lstate = e4561230); a6 if ( Env.Lstate = e0162345 or Env.Lstate = e0162354 or Env.Lstate = e0162453 or Env.Lstate = e0163452 or Env.Lstate = e0261345 or Env.Lstate = e0261354 or Env.Lstate = e0261453 or Env.Lstate = e0263451 or Env.Lstate = e0361245 or Env.Lstate = e0361254 or Env.Lstate = e0361452 or Env.Lstate = e0362451 or Env.Lstate = e0461235 or Env.Lstate = e0461253 or Env.Lstate = e0461352 or Env.Lstate = e0462351 or Env.Lstate = e0561234 or Env.Lstate = e0561243 or Env.Lstate = e0561342 or Env.Lstate = e0562341 or Env.Lstate = e1260345 or Env.Lstate = e1260354 or Env.Lstate = e1260453 or Env.Lstate = e1263450 or Env.Lstate = e1360245 or Env.Lstate = e1360254 or Env.Lstate = e1360452 or Env.Lstate = e1362450 or Env.Lstate = e1460235 or Env.Lstate = e1460253 or Env.Lstate = e1460352 or Env.Lstate = e1462350 or Env.Lstate = e1560234 or Env.Lstate = e1560243 or Env.Lstate = e1560342 or Env.Lstate = e1562340 or Env.Lstate = e2360145 or Env.Lstate = e2360154 or Env.Lstate = e2360451 or Env.Lstate = e2361450 or Env.Lstate = e2460135 or Env.Lstate = e2460153 or Env.Lstate = e2460351 or Env.Lstate = e2461350 or Env.Lstate = e2560134 or Env.Lstate = e2560143 or Env.Lstate = e2560341 or Env.Lstate = e2561340 or Env.Lstate = e3460125 or Env.Lstate = e3460152 or Env.Lstate = e3460251 or Env.Lstate = e3461250 or Env.Lstate = e3560124 or Env.Lstate = e3560142 or Env.Lstate = e3560241 or Env.Lstate = e3561240 or Env.Lstate = e4560123 or Env.Lstate = e4560132 or Env.Lstate = e4560231 or Env.Lstate = e4561230); b0 if ( Env.Lstate = e1230456 or Env.Lstate = e1230465 or Env.Lstate = e1230564 or Env.Lstate = e1240356 or Env.Lstate = e1240365 or Env.Lstate = e1240563 or Env.Lstate = e1250346 or Env.Lstate = e1250364 or Env.Lstate = e1250463 or Env.Lstate = e1260345 or Env.Lstate = e1260354 or Env.Lstate = e1260453 or Env.Lstate = e1340256 or Env.Lstate = e1340265 or Env.Lstate = e1340562 or Env.Lstate = e1350246 or Env.Lstate = e1350264 or Env.Lstate = e1350462 or Env.Lstate = e1360245 or Env.Lstate = e1360254 or Env.Lstate = e1360452 or Env.Lstate = e1450236 or Env.Lstate = e1450263 or Env.Lstate = e1450362 or Env.Lstate = e1460235 or Env.Lstate = e1460253 or Env.Lstate = e1460352 or Env.Lstate = e1560234 or Env.Lstate = e1560243 or Env.Lstate = e1560342 or Env.Lstate = e2340156 or Env.Lstate = e2340165 or Env.Lstate = e2340561 or Env.Lstate = e2350146 or Env.Lstate = e2350164 or Env.Lstate = e2350461 or Env.Lstate = e2360145 or Env.Lstate = e2360154 or Env.Lstate = e2360451 or Env.Lstate = e2450136 or Env.Lstate = e2450163 or Env.Lstate = e2450361 or Env.Lstate = e2460135 or Env.Lstate = e2460153 or Env.Lstate = e2460351 or Env.Lstate = e2560134 or Env.Lstate = e2560143 or Env.Lstate = e2560341 or Env.Lstate = e3450126 or Env.Lstate = e3450162 or Env.Lstate = e3450261 or Env.Lstate = e3460125 or Env.Lstate = e3460152 or Env.Lstate = e3460251 or Env.Lstate = e3560124 or Env.Lstate = e3560142 or Env.Lstate = e3560241 or Env.Lstate = e4560123 or Env.Lstate = e4560132 or Env.Lstate = e4560231); b1 if ( Env.Lstate = e0231456 or Env.Lstate = e0231465 or Env.Lstate = e0231564 or Env.Lstate = e0241356 or Env.Lstate = e0241365 or Env.Lstate = e0241563 or Env.Lstate = e0251346 or Env.Lstate = e0251364 or Env.Lstate = e0251463 or Env.Lstate = e0261345 or Env.Lstate = e0261354 or Env.Lstate = e0261453 or Env.Lstate = e0341256 or Env.Lstate = e0341265 or Env.Lstate = e0341562 or Env.Lstate = e0351246 or Env.Lstate = e0351264 or Env.Lstate = e0351462 or Env.Lstate = e0361245 or Env.Lstate = e0361254 or Env.Lstate = e0361452 or Env.Lstate = e0451236 or Env.Lstate = e0451263 or Env.Lstate = e0451362 or Env.Lstate = e0461235 or Env.Lstate = e0461253 or Env.Lstate = e0461352 or Env.Lstate = e0561234 or Env.Lstate = e0561243 or Env.Lstate = e0561342 or Env.Lstate = e2340156 or Env.Lstate = e2340165 or Env.Lstate = e2341560 or Env.Lstate = e2350146 or Env.Lstate = e2350164 or Env.Lstate = e2351460 or Env.Lstate = e2360145 or Env.Lstate = e2360154 or Env.Lstate = e2361450 or Env.Lstate = e2450136 or Env.Lstate = e2450163 or Env.Lstate = e2451360 or Env.Lstate = e2460135 or Env.Lstate = e2460153 or Env.Lstate = e2461350 or Env.Lstate = e2560134 or Env.Lstate = e2560143 or Env.Lstate = e2561340 or Env.Lstate = e3450126 or Env.Lstate = e3450162 or Env.Lstate = e3451260 or Env.Lstate = e3460125 or Env.Lstate = e3460152 or Env.Lstate = e3461250 or Env.Lstate = e3560124 or Env.Lstate = e3560142 or Env.Lstate = e3561240 or Env.Lstate = e4560123 or Env.Lstate = e4560132 or Env.Lstate = e4561230); b2 if ( Env.Lstate = e0132456 or Env.Lstate = e0132465 or Env.Lstate = e0132564 or Env.Lstate = e0142356 or Env.Lstate = e0142365 or Env.Lstate = e0142563 or Env.Lstate = e0152346 or Env.Lstate = e0152364 or Env.Lstate = e0152463 or Env.Lstate = e0162345 or Env.Lstate = e0162354 or Env.Lstate = e0162453 or Env.Lstate = e0341256 or Env.Lstate = e0341265 or Env.Lstate = e0342561 or Env.Lstate = e0351246 or Env.Lstate = e0351264 or Env.Lstate = e0352461 or Env.Lstate = e0361245 or Env.Lstate = e0361254 or Env.Lstate = e0362451 or Env.Lstate = e0451236 or Env.Lstate = e0451263 or Env.Lstate = e0452361 or Env.Lstate = e0461235 or Env.Lstate = e0461253 or Env.Lstate = e0462351 or Env.Lstate = e0561234 or Env.Lstate = e0561243 or Env.Lstate = e0562341 or Env.Lstate = e1340256 or Env.Lstate = e1340265 or Env.Lstate = e1342560 or Env.Lstate = e1350246 or Env.Lstate = e1350264 or Env.Lstate = e1352460 or Env.Lstate = e1360245 or Env.Lstate = e1360254 or Env.Lstate = e1362450 or Env.Lstate = e1450236 or Env.Lstate = e1450263 or Env.Lstate = e1452360 or Env.Lstate = e1460235 or Env.Lstate = e1460253 or Env.Lstate = e1462350 or Env.Lstate = e1560234 or Env.Lstate = e1560243 or Env.Lstate = e1562340 or Env.Lstate = e3450126 or Env.Lstate = e3450261 or Env.Lstate = e3451260 or Env.Lstate = e3460125 or Env.Lstate = e3460251 or Env.Lstate = e3461250 or Env.Lstate = e3560124 or Env.Lstate = e3560241 or Env.Lstate = e3561240 or Env.Lstate = e4560123 or Env.Lstate = e4560231 or Env.Lstate = e4561230); b3 if ( Env.Lstate = e0123456 or Env.Lstate = e0123465 or Env.Lstate = e0123564 or Env.Lstate = e0142356 or Env.Lstate = e0142365 or Env.Lstate = e0143562 or Env.Lstate = e0152346 or Env.Lstate = e0152364 or Env.Lstate = e0153462 or Env.Lstate = e0162345 or Env.Lstate = e0162354 or Env.Lstate = e0163452 or Env.Lstate = e0241356 or Env.Lstate = e0241365 or Env.Lstate = e0243561 or Env.Lstate = e0251346 or Env.Lstate = e0251364 or Env.Lstate = e0253461 or Env.Lstate = e0261345 or Env.Lstate = e0261354 or Env.Lstate = e0263451 or Env.Lstate = e0451236 or Env.Lstate = e0451362 or Env.Lstate = e0452361 or Env.Lstate = e0461235 or Env.Lstate = e0461352 or Env.Lstate = e0462351 or Env.Lstate = e0561234 or Env.Lstate = e0561342 or Env.Lstate = e0562341 or Env.Lstate = e1240356 or Env.Lstate = e1240365 or Env.Lstate = e1243560 or Env.Lstate = e1250346 or Env.Lstate = e1250364 or Env.Lstate = e1253460 or Env.Lstate = e1260345 or Env.Lstate = e1260354 or Env.Lstate = e1263450 or Env.Lstate = e1450236 or Env.Lstate = e1450362 or Env.Lstate = e1452360 or Env.Lstate = e1460235 or Env.Lstate = e1460352 or Env.Lstate = e1462350 or Env.Lstate = e1560234 or Env.Lstate = e1560342 or Env.Lstate = e1562340 or Env.Lstate = e2450136 or Env.Lstate = e2450361 or Env.Lstate = e2451360 or Env.Lstate = e2460135 or Env.Lstate = e2460351 or Env.Lstate = e2461350 or Env.Lstate = e2560134 or Env.Lstate = e2560341 or Env.Lstate = e2561340 or Env.Lstate = e4560132 or Env.Lstate = e4560231 or Env.Lstate = e4561230); b4 if ( Env.Lstate = e0123456 or Env.Lstate = e0123465 or Env.Lstate = e0124563 or Env.Lstate = e0132456 or Env.Lstate = e0132465 or Env.Lstate = e0134562 or Env.Lstate = e0152346 or Env.Lstate = e0152463 or Env.Lstate = e0153462 or Env.Lstate = e0162345 or Env.Lstate = e0162453 or Env.Lstate = e0163452 or Env.Lstate = e0231456 or Env.Lstate = e0231465 or Env.Lstate = e0234561 or Env.Lstate = e0251346 or Env.Lstate = e0251463 or Env.Lstate = e0253461 or Env.Lstate = e0261345 or Env.Lstate = e0261453 or Env.Lstate = e0263451 or Env.Lstate = e0351246 or Env.Lstate = e0351462 or Env.Lstate = e0352461 or Env.Lstate = e0361245 or Env.Lstate = e0361452 or Env.Lstate = e0362451 or Env.Lstate = e0561243 or Env.Lstate = e0561342 or Env.Lstate = e0562341 or Env.Lstate = e1230456 or Env.Lstate = e1230465 or Env.Lstate = e1234560 or Env.Lstate = e1250346 or Env.Lstate = e1250463 or Env.Lstate = e1253460 or Env.Lstate = e1260345 or Env.Lstate = e1260453 or Env.Lstate = e1263450 or Env.Lstate = e1350246 or Env.Lstate = e1350462 or Env.Lstate = e1352460 or Env.Lstate = e1360245 or Env.Lstate = e1360452 or Env.Lstate = e1362450 or Env.Lstate = e1560243 or Env.Lstate = e1560342 or Env.Lstate = e1562340 or Env.Lstate = e2350146 or Env.Lstate = e2350461 or Env.Lstate = e2351460 or Env.Lstate = e2360145 or Env.Lstate = e2360451 or Env.Lstate = e2361450 or Env.Lstate = e2560143 or Env.Lstate = e2560341 or Env.Lstate = e2561340 or Env.Lstate = e3560142 or Env.Lstate = e3560241 or Env.Lstate = e3561240); b5 if ( Env.Lstate = e0123456 or Env.Lstate = e0123564 or Env.Lstate = e0124563 or Env.Lstate = e0132456 or Env.Lstate = e0132564 or Env.Lstate = e0134562 or Env.Lstate = e0142356 or Env.Lstate = e0142563 or Env.Lstate = e0143562 or Env.Lstate = e0162354 or Env.Lstate = e0162453 or Env.Lstate = e0163452 or Env.Lstate = e0231456 or Env.Lstate = e0231564 or Env.Lstate = e0234561 or Env.Lstate = e0241356 or Env.Lstate = e0241563 or Env.Lstate = e0243561 or Env.Lstate = e0261354 or Env.Lstate = e0261453 or Env.Lstate = e0263451 or Env.Lstate = e0341256 or Env.Lstate = e0341562 or Env.Lstate = e0342561 or Env.Lstate = e0361254 or Env.Lstate = e0361452 or Env.Lstate = e0362451 or Env.Lstate = e0461253 or Env.Lstate = e0461352 or Env.Lstate = e0462351 or Env.Lstate = e1230456 or Env.Lstate = e1230564 or Env.Lstate = e1234560 or Env.Lstate = e1240356 or Env.Lstate = e1240563 or Env.Lstate = e1243560 or Env.Lstate = e1260354 or Env.Lstate = e1260453 or Env.Lstate = e1263450 or Env.Lstate = e1340256 or Env.Lstate = e1340562 or Env.Lstate = e1342560 or Env.Lstate = e1360254 or Env.Lstate = e1360452 or Env.Lstate = e1362450 or Env.Lstate = e1460253 or Env.Lstate = e1460352 or Env.Lstate = e1462350 or Env.Lstate = e2340156 or Env.Lstate = e2340561 or Env.Lstate = e2341560 or Env.Lstate = e2360154 or Env.Lstate = e2360451 or Env.Lstate = e2361450 or Env.Lstate = e2460153 or Env.Lstate = e2460351 or Env.Lstate = e2461350 or Env.Lstate = e3460152 or Env.Lstate = e3460251 or Env.Lstate = e3461250); b6 if ( Env.Lstate = e0123465 or Env.Lstate = e0123564 or Env.Lstate = e0124563 or Env.Lstate = e0132465 or Env.Lstate = e0132564 or Env.Lstate = e0134562 or Env.Lstate = e0142365 or Env.Lstate = e0142563 or Env.Lstate = e0143562 or Env.Lstate = e0152364 or Env.Lstate = e0152463 or Env.Lstate = e0153462 or Env.Lstate = e0231465 or Env.Lstate = e0231564 or Env.Lstate = e0234561 or Env.Lstate = e0241365 or Env.Lstate = e0241563 or Env.Lstate = e0243561 or Env.Lstate = e0251364 or Env.Lstate = e0251463 or Env.Lstate = e0253461 or Env.Lstate = e0341265 or Env.Lstate = e0341562 or Env.Lstate = e0342561 or Env.Lstate = e0351264 or Env.Lstate = e0351462 or Env.Lstate = e0352461 or Env.Lstate = e0451263 or Env.Lstate = e0451362 or Env.Lstate = e0452361 or Env.Lstate = e1230465 or Env.Lstate = e1230564 or Env.Lstate = e1234560 or Env.Lstate = e1240365 or Env.Lstate = e1240563 or Env.Lstate = e1243560 or Env.Lstate = e1250364 or Env.Lstate = e1250463 or Env.Lstate = e1253460 or Env.Lstate = e1340265 or Env.Lstate = e1340562 or Env.Lstate = e1342560 or Env.Lstate = e1350264 or Env.Lstate = e1350462 or Env.Lstate = e1352460 or Env.Lstate = e1450263 or Env.Lstate = e1450362 or Env.Lstate = e1452360 or Env.Lstate = e2340165 or Env.Lstate = e2340561 or Env.Lstate = e2341560 or Env.Lstate = e2350164 or Env.Lstate = e2350461 or Env.Lstate = e2351460 or Env.Lstate = e2450163 or Env.Lstate = e2450361 or Env.Lstate = e2451360 or Env.Lstate = e3450162 or Env.Lstate = e3450261 or Env.Lstate = e3451260); c0 if ( Env.Lstate = e1234560 or Env.Lstate = e1243560 or Env.Lstate = e1253460 or Env.Lstate = e1263450 or Env.Lstate = e1342560 or Env.Lstate = e1352460 or Env.Lstate = e1362450 or Env.Lstate = e1452360 or Env.Lstate = e1462350 or Env.Lstate = e1562340 or Env.Lstate = e2341560 or Env.Lstate = e2351460 or Env.Lstate = e2361450 or Env.Lstate = e2451360 or Env.Lstate = e2461350 or Env.Lstate = e2561340 or Env.Lstate = e3451260 or Env.Lstate = e3461250 or Env.Lstate = e3561240 or Env.Lstate = e4561230); c1 if ( Env.Lstate = e0234561 or Env.Lstate = e0243561 or Env.Lstate = e0253461 or Env.Lstate = e0263451 or Env.Lstate = e0342561 or Env.Lstate = e0352461 or Env.Lstate = e0362451 or Env.Lstate = e0452361 or Env.Lstate = e0462351 or Env.Lstate = e0562341 or Env.Lstate = e2340561 or Env.Lstate = e2350461 or Env.Lstate = e2360451 or Env.Lstate = e2450361 or Env.Lstate = e2460351 or Env.Lstate = e2560341 or Env.Lstate = e3450261 or Env.Lstate = e3460251 or Env.Lstate = e3560241 or Env.Lstate = e4560231); c2 if ( Env.Lstate = e0134562 or Env.Lstate = e0143562 or Env.Lstate = e0153462 or Env.Lstate = e0163452 or Env.Lstate = e0341562 or Env.Lstate = e0351462 or Env.Lstate = e0361452 or Env.Lstate = e0451362 or Env.Lstate = e0461352 or Env.Lstate = e0561342 or Env.Lstate = e1340562 or Env.Lstate = e1350462 or Env.Lstate = e1360452 or Env.Lstate = e1450362 or Env.Lstate = e1460352 or Env.Lstate = e1560342 or Env.Lstate = e3450162 or Env.Lstate = e3460152 or Env.Lstate = e3560142 or Env.Lstate = e4560132); c3 if ( Env.Lstate = e0124563 or Env.Lstate = e0142563 or Env.Lstate = e0152463 or Env.Lstate = e0162453 or Env.Lstate = e0241563 or Env.Lstate = e0251463 or Env.Lstate = e0261453 or Env.Lstate = e0451263 or Env.Lstate = e0461253 or Env.Lstate = e0561243 or Env.Lstate = e1240563 or Env.Lstate = e1250463 or Env.Lstate = e1260453 or Env.Lstate = e1450263 or Env.Lstate = e1460253 or Env.Lstate = e1560243 or Env.Lstate = e2450163 or Env.Lstate = e2460153 or Env.Lstate = e2560143 or Env.Lstate = e4560123); c4 if ( Env.Lstate = e0123564 or Env.Lstate = e0132564 or Env.Lstate = e0152364 or Env.Lstate = e0162354 or Env.Lstate = e0231564 or Env.Lstate = e0251364 or Env.Lstate = e0261354 or Env.Lstate = e0351264 or Env.Lstate = e0361254 or Env.Lstate = e0561234 or Env.Lstate = e1230564 or Env.Lstate = e1250364 or Env.Lstate = e1260354 or Env.Lstate = e1350264 or Env.Lstate = e1360254 or Env.Lstate = e1560234 or Env.Lstate = e2350164 or Env.Lstate = e2360154 or Env.Lstate = e2560134 or Env.Lstate = e3560124); c5 if ( Env.Lstate = e0123465 or Env.Lstate = e0132465 or Env.Lstate = e0142365 or Env.Lstate = e0162345 or Env.Lstate = e0231465 or Env.Lstate = e0241365 or Env.Lstate = e0261345 or Env.Lstate = e0341265 or Env.Lstate = e0361245 or Env.Lstate = e0461235 or Env.Lstate = e1230465 or Env.Lstate = e1240365 or Env.Lstate = e1260345 or Env.Lstate = e1340265 or Env.Lstate = e1360245 or Env.Lstate = e1460235 or Env.Lstate = e2340165 or Env.Lstate = e2360145 or Env.Lstate = e2460135 or Env.Lstate = e3460125); c6 if ( Env.Lstate = e0123456 or Env.Lstate = e0132456 or Env.Lstate = e0142356 or Env.Lstate = e0152346 or Env.Lstate = e0231456 or Env.Lstate = e0241356 or Env.Lstate = e0251346 or Env.Lstate = e0341256 or Env.Lstate = e0351246 or Env.Lstate = e0451236 or Env.Lstate = e1230456 or Env.Lstate = e1240356 or Env.Lstate = e1250346 or Env.Lstate = e1340256 or Env.Lstate = e1350246 or Env.Lstate = e1450236 or Env.Lstate = e2340156 or Env.Lstate = e2350146 or Env.Lstate = e2450136 or Env.Lstate = e3450126); init if ( (Anne.Lstate=annnnn and Bill.Lstate=bnnnnn and Cath.Lstate=cnnn) and (Env.Lstate=e0123456 or Env.Lstate=e0123465 or Env.Lstate=e0123564 or Env.Lstate=e0124563 or Env.Lstate=e0132456 or Env.Lstate=e0132465 or Env.Lstate=e0132564 or Env.Lstate=e0134562 or Env.Lstate=e0142356 or Env.Lstate=e0142365 or Env.Lstate=e0142563 or Env.Lstate=e0143562 or Env.Lstate=e0152346 or Env.Lstate=e0152364 or Env.Lstate=e0152463 or Env.Lstate=e0153462 or Env.Lstate=e0162345 or Env.Lstate=e0162354 or Env.Lstate=e0162453 or Env.Lstate=e0163452 or Env.Lstate=e0231456 or Env.Lstate=e0231465 or Env.Lstate=e0231564 or Env.Lstate=e0234561 or Env.Lstate=e0241356 or Env.Lstate=e0241365 or Env.Lstate=e0241563 or Env.Lstate=e0243561 or Env.Lstate=e0251346 or Env.Lstate=e0251364 or Env.Lstate=e0251463 or Env.Lstate=e0253461 or Env.Lstate=e0261345 or Env.Lstate=e0261354 or Env.Lstate=e0261453 or Env.Lstate=e0263451 or Env.Lstate=e0341256 or Env.Lstate=e0341265 or Env.Lstate=e0341562 or Env.Lstate=e0342561 or Env.Lstate=e0351246 or Env.Lstate=e0351264 or Env.Lstate=e0351462 or Env.Lstate=e0352461 or Env.Lstate=e0361245 or Env.Lstate=e0361254 or Env.Lstate=e0361452 or Env.Lstate=e0362451 or Env.Lstate=e0451236 or Env.Lstate=e0451263 or Env.Lstate=e0451362 or Env.Lstate=e0452361 or Env.Lstate=e0461235 or Env.Lstate=e0461253 or Env.Lstate=e0461352 or Env.Lstate=e0462351 or Env.Lstate=e0561234 or Env.Lstate=e0561243 or Env.Lstate=e0561342 or Env.Lstate=e0562341 or Env.Lstate=e1230456 or Env.Lstate=e1230465 or Env.Lstate=e1230564 or Env.Lstate=e1234560 or Env.Lstate=e1240356 or Env.Lstate=e1240365 or Env.Lstate=e1240563 or Env.Lstate=e1243560 or Env.Lstate=e1250346 or Env.Lstate=e1250364 or Env.Lstate=e1250463 or Env.Lstate=e1253460 or Env.Lstate=e1260345 or Env.Lstate=e1260354 or Env.Lstate=e1260453 or Env.Lstate=e1263450 or Env.Lstate=e1340256 or Env.Lstate=e1340265 or Env.Lstate=e1340562 or Env.Lstate=e1342560 or Env.Lstate=e1350246 or Env.Lstate=e1350264 or Env.Lstate=e1350462 or Env.Lstate=e1352460 or Env.Lstate=e1360245 or Env.Lstate=e1360254 or Env.Lstate=e1360452 or Env.Lstate=e1362450 or Env.Lstate=e1450236 or Env.Lstate=e1450263 or Env.Lstate=e1450362 or Env.Lstate=e1452360 or Env.Lstate=e1460235 or Env.Lstate=e1460253 or Env.Lstate=e1460352 or Env.Lstate=e1462350 or Env.Lstate=e1560234 or Env.Lstate=e1560243 or Env.Lstate=e1560342 or Env.Lstate=e1562340 or Env.Lstate=e2340156 or Env.Lstate=e2340165 or Env.Lstate=e2340561 or Env.Lstate=e2341560 or Env.Lstate=e2350146 or Env.Lstate=e2350164 or Env.Lstate=e2350461 or Env.Lstate=e2351460 or Env.Lstate=e2360145 or Env.Lstate=e2360154 or Env.Lstate=e2360451 or Env.Lstate=e2361450 or Env.Lstate=e2450136 or Env.Lstate=e2450163 or Env.Lstate=e2450361 or Env.Lstate=e2451360 or Env.Lstate=e2460135 or Env.Lstate=e2460153 or Env.Lstate=e2460351 or Env.Lstate=e2461350 or Env.Lstate=e2560134 or Env.Lstate=e2560143 or Env.Lstate=e2560341 or Env.Lstate=e2561340 or Env.Lstate=e3450126 or Env.Lstate=e3450162 or Env.Lstate=e3450261 or Env.Lstate=e3451260 or Env.Lstate=e3460125 or Env.Lstate=e3460152 or Env.Lstate=e3460251 or Env.Lstate=e3461250 or Env.Lstate=e3560124 or Env.Lstate=e3560142 or Env.Lstate=e3560241 or Env.Lstate=e3561240 or Env.Lstate=e4560123 or Env.Lstate=e4560132 or Env.Lstate=e4560231 or Env.Lstate=e4561230)); ab_d0123456 if (Anne.Lstate=a012tt and Bill.Lstate=b345tt and Cath.Lstate=c6tt and Env.Lstate=e0123456); a_d0123456 if (Anne.Lstate=a012tn and Bill.Lstate=b345tn and Cath.Lstate=c6tn and Env.Lstate=e0123456); n_d0123456 if (Anne.Lstate=a012nn and Bill.Lstate=b345nn and Cath.Lstate=c6nn and Env.Lstate=e0123456); init0123456 if (Anne.Lstate=annnnn and Bill.Lstate=bnnnnn and Cath.Lstate=cnnn and Env.Lstate=e0123456); end Evaluation InitStates (Anne.Lstate=annnnn and Bill.Lstate=bnnnnn and Cath.Lstate=cnnn) and (Env.Lstate=e0123456 or Env.Lstate=e0123465 or Env.Lstate=e0123564 or Env.Lstate=e0124563 or Env.Lstate=e0132456 or Env.Lstate=e0132465 or Env.Lstate=e0132564 or Env.Lstate=e0134562 or Env.Lstate=e0142356 or Env.Lstate=e0142365 or Env.Lstate=e0142563 or Env.Lstate=e0143562 or Env.Lstate=e0152346 or Env.Lstate=e0152364 or Env.Lstate=e0152463 or Env.Lstate=e0153462 or Env.Lstate=e0162345 or Env.Lstate=e0162354 or Env.Lstate=e0162453 or Env.Lstate=e0163452 or Env.Lstate=e0231456 or Env.Lstate=e0231465 or Env.Lstate=e0231564 or Env.Lstate=e0234561 or Env.Lstate=e0241356 or Env.Lstate=e0241365 or Env.Lstate=e0241563 or Env.Lstate=e0243561 or Env.Lstate=e0251346 or Env.Lstate=e0251364 or Env.Lstate=e0251463 or Env.Lstate=e0253461 or Env.Lstate=e0261345 or Env.Lstate=e0261354 or Env.Lstate=e0261453 or Env.Lstate=e0263451 or Env.Lstate=e0341256 or Env.Lstate=e0341265 or Env.Lstate=e0341562 or Env.Lstate=e0342561 or Env.Lstate=e0351246 or Env.Lstate=e0351264 or Env.Lstate=e0351462 or Env.Lstate=e0352461 or Env.Lstate=e0361245 or Env.Lstate=e0361254 or Env.Lstate=e0361452 or Env.Lstate=e0362451 or Env.Lstate=e0451236 or Env.Lstate=e0451263 or Env.Lstate=e0451362 or Env.Lstate=e0452361 or Env.Lstate=e0461235 or Env.Lstate=e0461253 or Env.Lstate=e0461352 or Env.Lstate=e0462351 or Env.Lstate=e0561234 or Env.Lstate=e0561243 or Env.Lstate=e0561342 or Env.Lstate=e0562341 or Env.Lstate=e1230456 or Env.Lstate=e1230465 or Env.Lstate=e1230564 or Env.Lstate=e1234560 or Env.Lstate=e1240356 or Env.Lstate=e1240365 or Env.Lstate=e1240563 or Env.Lstate=e1243560 or Env.Lstate=e1250346 or Env.Lstate=e1250364 or Env.Lstate=e1250463 or Env.Lstate=e1253460 or Env.Lstate=e1260345 or Env.Lstate=e1260354 or Env.Lstate=e1260453 or Env.Lstate=e1263450 or Env.Lstate=e1340256 or Env.Lstate=e1340265 or Env.Lstate=e1340562 or Env.Lstate=e1342560 or Env.Lstate=e1350246 or Env.Lstate=e1350264 or Env.Lstate=e1350462 or Env.Lstate=e1352460 or Env.Lstate=e1360245 or Env.Lstate=e1360254 or Env.Lstate=e1360452 or Env.Lstate=e1362450 or Env.Lstate=e1450236 or Env.Lstate=e1450263 or Env.Lstate=e1450362 or Env.Lstate=e1452360 or Env.Lstate=e1460235 or Env.Lstate=e1460253 or Env.Lstate=e1460352 or Env.Lstate=e1462350 or Env.Lstate=e1560234 or Env.Lstate=e1560243 or Env.Lstate=e1560342 or Env.Lstate=e1562340 or Env.Lstate=e2340156 or Env.Lstate=e2340165 or Env.Lstate=e2340561 or Env.Lstate=e2341560 or Env.Lstate=e2350146 or Env.Lstate=e2350164 or Env.Lstate=e2350461 or Env.Lstate=e2351460 or Env.Lstate=e2360145 or Env.Lstate=e2360154 or Env.Lstate=e2360451 or Env.Lstate=e2361450 or Env.Lstate=e2450136 or Env.Lstate=e2450163 or Env.Lstate=e2450361 or Env.Lstate=e2451360 or Env.Lstate=e2460135 or Env.Lstate=e2460153 or Env.Lstate=e2460351 or Env.Lstate=e2461350 or Env.Lstate=e2560134 or Env.Lstate=e2560143 or Env.Lstate=e2560341 or Env.Lstate=e2561340 or Env.Lstate=e3450126 or Env.Lstate=e3450162 or Env.Lstate=e3450261 or Env.Lstate=e3451260 or Env.Lstate=e3460125 or Env.Lstate=e3460152 or Env.Lstate=e3460251 or Env.Lstate=e3461250 or Env.Lstate=e3560124 or Env.Lstate=e3560142 or Env.Lstate=e3560241 or Env.Lstate=e3561240 or Env.Lstate=e4560123 or Env.Lstate=e4560132 or Env.Lstate=e4560231 or Env.Lstate=e4561230); end InitStates Groups AB={Anne,Bill}; AC={Anne,Cath}; BC={Bill, Cath}; ABC={Anne, Bill, Cath}; end Groups Formulae --We take 012.345.6 as the actual deal. --Then checking some postconditions of (A)nne and (B)ill's announcements. --prefix a_ denotes After Anne's announcement --prefix ab_ denotes After Anne and Bill's announcements --After A's announcement, Bill know Cath holds 6. a_d0123456 -> K(Bill, c6); --After A's announcement, it is not the case that a_knows_bs. a_d0123456 -> !( ( K(Anne,b0) or K(Anne,!b0) ) and ( K(Anne,b1) or K(Anne,!b1) ) and ( K(Anne,b2) or K(Anne,!b2) ) and ( K(Anne,b3) or K(Anne,!b3) ) and ( K(Anne,b4) or K(Anne,!b4) ) and ( K(Anne,b5) or K(Anne,!b5) ) and ( K(Anne,b6) or K(Anne,!b6) ) ); --After A and B's announcement, --it is common knowledge among Anne and Bill that a_knows_bs. ab_d0123456 -> GCK(AB, ( ( K(Anne,b0) or K(Anne,!b0) ) and ( K(Anne,b1) or K(Anne,!b1) ) and ( K(Anne,b2) or K(Anne,!b2) ) and ( K(Anne,b3) or K(Anne,!b3) ) and ( K(Anne,b4) or K(Anne,!b4) ) and ( K(Anne,b5) or K(Anne,!b5) ) and ( K(Anne,b6) or K(Anne,!b6) ) )); --After A's announcement, it is common knowledge that cignorant: a_d0123456 -> GCK(ABC,( !c0-> ( !K(Cath,a0) and !K(Cath,b0) ) and !c1-> ( !K(Cath,a1) and !K(Cath,b1) ) and !c2-> ( !K(Cath,a2) and !K(Cath,b2) ) and !c3-> ( !K(Cath,a3) and !K(Cath,b3) ) and !c4-> ( !K(Cath,a4) and !K(Cath,b4) ) and !c5-> ( !K(Cath,a5) and !K(Cath,b5) ) and !c6-> ( !K(Cath,a6) and !K(Cath,b6) ) )); --After B's announcement, it is common knowledge that cignorant. ab_d0123456 -> GCK(ABC,( !c0-> ( !K(Cath,a0) and !K(Cath,b0) ) and !c1-> ( !K(Cath,a1) and !K(Cath,b1) ) and !c2-> ( !K(Cath,a2) and !K(Cath,b2) ) and !c3-> ( !K(Cath,a3) and !K(Cath,b3) ) and !c4-> ( !K(Cath,a4) and !K(Cath,b4) ) and !c5-> ( !K(Cath,a5) and !K(Cath,b5) ) and !c6-> ( !K(Cath,a6) and !K(Cath,b6) ) )); end Formulae