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
//This file was generated from UPPAAL2k. /* *** By Paul Pettersson (paupet@docs.uu.se) 2001-3-6. */ //NO_QUERY /* A solution can be found. */ E<>( ( G0.s[0]==1 and G0.s[1]==1 and G0.s[2]==1 and G0.s[3]==1 ) and \\ ( G1.s[0]==1 and G1.s[1]==1 and G1.s[2]==1 and G1.s[3]==1 ) and \\ ( G2.s[0]==1 and G2.s[1]==1 and G2.s[2]==1 and G2.s[3]==1 ) and \\ ( G3.s[0]==1 and G3.s[1]==1 and G3.s[2]==1 and G3.s[3]==1 ) ) /* A solution can be found using four calls. */ E<>( ( G0.s[0]==1 and G0.s[1]==1 and G0.s[2]==1 and G0.s[3]==1 ) and \\ ( G1.s[0]==1 and G1.s[1]==1 and G1.s[2]==1 and G1.s[3]==1 ) and \\ ( G2.s[0]==1 and G2.s[1]==1 and G2.s[2]==1 and G2.s[3]==1 ) and \\ ( G3.s[0]==1 and G3.s[1]==1 and G3.s[2]==1 and G3.s[3]==1 ) and ( nr==4 )) /* At least four phone calls must be made to find a solution. */ A[]( ( G0.s[0]==1 and G0.s[1]==1 and G0.s[2]==1 and G0.s[3]==1 ) and \\ ( G1.s[0]==1 and G1.s[1]==1 and G1.s[2]==1 and G1.s[3]==1 ) and \\ ( G2.s[0]==1 and G2.s[1]==1 and G2.s[2]==1 and G2.s[3]==1 ) and \\ ( G3.s[0]==1 and G3.s[1]==1 and G3.s[2]==1 and G3.s[3]==1 ) imply ( nr>=4 )) /* A solution can be found using four calls. */ E<>( ( G0.s[0]==1 and G0.s[1]==1 and G0.s[2]==1 and G0.s[3]==1 ) and \\ ( G1.s[0]==1 and G1.s[1]==1 and G1.s[2]==1 and G1.s[3]==1 ) and \\ ( G2.s[0]==1 and G2.s[1]==1 and G2.s[2]==1 and G2.s[3]==1 ) and \\ ( G3.s[0]==1 and G3.s[1]==1 and G3.s[2]==1 and G3.s[3]==1 ) and ( nr==6 ) ) /* No more than 6 phone meaningful phone calls (where secrets are exchanged) can be made. */ A[]( nr<=6 )