%------------------------------------------------------------------------------ % File : SWV011+0 : TPTP v7.2.0. Released v4.0.0. % Domain : Software Verification % Axioms : Axioms for verification of Stoller's leader election algorithm % Version : [Sve07] axioms : Especial. % English : % Refs : [Sto97] Stoller (1997), Leader Election in Distributed Systems % : [Sve07] Svensson (2007), Email to Koen Claessen % : [Sve08] Svensson (2008), A Semi-Automatic Correctness Proof Pr % Source : [Sve07] % Names : stoller2 [Sve07] % : con_sys [Sve07] % : cons_snoc [Sve07] % : arith [Sve07] % : sets [Sve07] % Status : Satisfiable % Syntax : Number of formulae : 66 ( 40 unit) % Number of atoms : 111 ( 62 equality) % Maximal formula depth : 10 ( 4 average) % Number of connectives : 89 ( 44 ~; 7 |; 14 &) % ( 13 <=>; 11 =>; 0 <=) % ( 0 <~>; 0 ~|; 0 ~&) % Number of predicates : 6 ( 0 propositional; 1-2 arity) % Number of functors : 27 ( 11 constant; 0-2 arity) % Number of variables : 119 ( 0 sgn; 118 !; 1 ?) % Maximal term depth : 3 ( 2 average) % SPC : % Comments : %------------------------------------------------------------------------------ %----Stoller axioms messages and such things %----NewPid fof(axiom,axiom,( ! [Pid,Pid2] : ( elem(m_Ack(Pid,Pid2),queue(host(Pid))) => ( setIn(Pid,pids) & setIn(Pid2,pids) ) ) )). fof(axiom_01,axiom,( ! [P,Q] : ( s(host(P)) = host(Q) => host(P) != host(Q) ) )). fof(axiom_02,axiom,( ! [P] : leq(s(zero),host(P)) )). fof(axiom_03,axiom,( leq(s(zero),nbr_proc) )). fof(axiom_04,axiom,( ! [P] : leq(host(P),nbr_proc) )). fof(axiom_05,axiom,( elec_1 != elec_2 )). fof(axiom_06,axiom,( elec_1 != wait )). fof(axiom_07,axiom,( elec_1 != norm )). fof(axiom_08,axiom,( elec_2 != wait )). fof(axiom_09,axiom,( elec_2 != norm )). fof(axiom_10,axiom,( norm != wait )). fof(axiom_11,axiom,( ! [X,Y,Z] : m_Ack(X,Y) != m_Halt(Z) )). fof(axiom_12,axiom,( ! [X,Y,Z] : m_Ack(X,Y) != m_Down(Z) )). fof(axiom_13,axiom,( ! [X,Y,Z] : m_Ack(X,Y) != m_NotNorm(Z) )). fof(axiom_14,axiom,( ! [X,Y,Z] : m_Ack(X,Y) != m_Ldr(Z) )). fof(axiom_15,axiom,( ! [X,Y,Z] : m_Ack(X,Y) != m_NormQ(Z) )). fof(axiom_16,axiom,( ! [X,Y] : m_NotNorm(X) != m_Halt(Y) )). fof(axiom_17,axiom,( ! [X,Y] : m_Down(X) != m_Halt(Y) )). fof(axiom_18,axiom,( ! [X,Y] : m_Down(X) != m_Ldr(Y) )). fof(axiom_19,axiom,( ! [X,Y] : m_Down(X) != m_NotNorm(Y) )). fof(axiom_20,axiom,( ! [X,Y] : m_Down(X) != m_NormQ(Y) )). fof(axiom_21,axiom,( ! [X,Y] : m_NormQ(X) != m_Halt(Y) )). fof(axiom_22,axiom,( ! [X,Y] : m_Ldr(X) != m_Halt(Y) )). fof(axiom_23,axiom,( ! [X,Y] : m_Ldr(X) != m_NormQ(Y) )). fof(axiom_24,axiom,( ! [X,Y] : m_Ldr(X) != m_NotNorm(Y) )). fof(axiom_25,axiom,( ! [X,Y] : m_NormQ(X) != m_NotNorm(Y) )). fof(axiom_26,axiom,( ! [X,Y] : ( X != Y <=> m_Halt(X) != m_Halt(Y) ) )). fof(axiom_27,axiom,( ! [X,Y] : ( X != Y <=> m_NormQ(X) != m_NormQ(Y) ) )). fof(axiom_28,axiom,( ! [X,Y] : ( X != Y <=> m_NotNorm(X) != m_NotNorm(Y) ) )). fof(axiom_29,axiom,( ! [X,Y] : ( X != Y <=> m_Ldr(X) != m_Ldr(Y) ) )). fof(axiom_30,axiom,( ! [X,Y] : ( X != Y <=> m_Down(X) != m_Down(Y) ) )). fof(axiom_31,axiom,( ! [X1,X2,Y1,Y2] : ( X1 != X2 => m_Ack(X1,Y1) != m_Ack(X2,Y2) ) )). fof(axiom_32,axiom,( ! [X1,X2,Y1,Y2] : ( Y1 != Y2 => m_Ack(X1,Y1) != m_Ack(X2,Y2) ) )). %----Axioms for a concurrent system; i.e. Pids and Alive fof(axiom_33,axiom,( ! [Pid,Pid2] : ( host(Pid) != host(Pid2) => Pid != Pid2 ) )). fof(axiom_34,axiom,( ~ setIn(nil,alive) )). %----Axioms for snoc and cons style of queues %----Injective fof(axiom_35,axiom,( ! [X,Q] : head(cons(X,Q)) = X )). fof(axiom_36,axiom,( ! [X,Q] : tail(cons(X,Q)) = Q )). fof(axiom_37,axiom,( ! [Y,Q] : last(snoc(Q,Y)) = Y )). fof(axiom_38,axiom,( ! [Y,Q] : init(snoc(Q,Y)) = Q )). %----Surjective fof(axiom_39,axiom,( ! [Q] : ( Q = q_nil | Q = cons(head(Q),tail(Q)) ) )). fof(axiom_40,axiom,( ! [Q] : ( Q = q_nil | Q = snoc(init(Q),last(Q)) ) )). %----Exclusive fof(axiom_41,axiom,( ! [X,Q] : q_nil != cons(X,Q) )). fof(axiom_42,axiom,( ! [Y,Q] : q_nil != snoc(Q,Y) )). %----Equal singleton queue fof(axiom_43,axiom,( ! [X] : cons(X,q_nil) = snoc(q_nil,X) )). %----Snoc+cons equals cons+snoc fof(axiom_44,axiom,( ! [X,Y,Q] : snoc(cons(X,Q),Y) = cons(X,snoc(Q,Y)) )). %----Elem fof(axiom_45,axiom,( ! [X] : ~ elem(X,q_nil) )). fof(axiom_46,axiom,( ! [X,Y,Q] : ( elem(X,cons(Y,Q)) <=> ( X = Y | elem(X,Q) ) ) )). fof(axiom_47,axiom,( ! [X,Y,Q] : ( elem(X,snoc(Q,Y)) <=> ( X = Y | elem(X,Q) ) ) )). %----Ordered fof(axiom_48,axiom,( ! [X] : ( pidElem(X) <=> ? [Y] : ( X = m_Halt(Y) | X = m_Down(Y) ) ) )). fof(axiom_49,axiom,( ! [X] : pidMsg(m_Halt(X)) = X )). fof(axiom_50,axiom,( ! [X] : pidMsg(m_Down(X)) = X )). fof(axiom_51,axiom,( ordered(q_nil) )). fof(axiom_52,axiom,( ! [X] : ( ordered(cons(X,q_nil)) & ordered(snoc(q_nil,X)) ) )). fof(axiom_53,axiom,( ! [X,Q] : ( ordered(cons(X,Q)) <=> ( ordered(Q) & ! [Y] : ( ( elem(Y,Q) & pidElem(X) & pidElem(Y) & host(pidMsg(Y)) = host(pidMsg(X)) ) => leq(pidMsg(X),pidMsg(Y)) ) ) ) )). fof(axiom_54,axiom,( ! [X,Q] : ( ordered(snoc(Q,X)) <=> ( ordered(Q) & ! [Y] : ( ( elem(Y,Q) & pidElem(X) & pidElem(Y) & host(pidMsg(Y)) = host(pidMsg(X)) ) => leq(pidMsg(Y),pidMsg(X)) ) ) ) )). %----Helper axioms fof(axiom_55,axiom,( ! [Q,X,Y] : ( ordered(Q) => ordered(snoc(Q,m_Ack(X,Y))) ) )). fof(axiom_56,axiom,( ! [Q,X] : ( ordered(Q) => ordered(snoc(Q,m_Ldr(X))) ) )). fof(axiom_57,axiom,( ! [Q,X,Y] : ( ( ordered(cons(m_Halt(X),Q)) & host(X) = host(Y) & elem(m_Down(Y),Q) ) => leq(X,Y) ) )). fof(axiom_58,axiom,( ! [X] : ~ leq(s(X),X) )). fof(axiom_59,axiom,( ! [X] : leq(X,X) )). fof(axiom_60,axiom,( ! [X,Y] : ( leq(X,Y) | leq(Y,X) ) )). fof(axiom_61,axiom,( ! [X,Y] : ( ( leq(X,Y) & leq(Y,X) ) <=> X = Y ) )). fof(axiom_62,axiom,( ! [X,Y,Z] : ( ( leq(X,Y) & leq(Y,Z) ) => leq(X,Z) ) )). fof(axiom_63,axiom,( ! [X,Y] : ( leq(X,Y) <=> leq(s(X),s(Y)) ) )). fof(axiom_64,axiom,( ! [X,Y] : ( leq(X,s(Y)) <=> ( X = s(Y) | leq(X,Y) ) ) )). %----Set axioms fof(axiom_65,axiom,( ! [X] : ~ setIn(X,setEmpty) )). %------------------------------------------------------------------------------