fact: Definition network_invariant (net : @network _ PB_multi_params) : Prop := (nwPackets net = [] /\ state (nwState net Primary) = state (nwState net Backup)) \/ (exists i is, nwPackets net = [mkPacket Primary Backup (BackItUp i)] /\ queue (nwState net Primary) = i :: is /\ state (nwState net Primary) = state (nwState net Backup)) \/ (nwPackets net = [mkPacket Backup Primary Ack] /\ exists i is, queue (nwState net Primary) = i :: is /\ snd (handler i (state (nwState net Primary))) = state (nwState net Backup)).
imports: Verdi(Verdi HandlerMonad)