Commit c896169b authored by Philipp Meyer's avatar Philipp Meyer
Browse files

Add initial predicate to solver

parent 7b8da344
Loading
Loading
Loading
Loading
+1 −1
Original line number Diff line number Diff line
@@ -6,7 +6,7 @@ module PopulationProtocol
     Configuration,FlowVector,RConfiguration,RFlowVector,
     renameState,renameTransition,renameStatesAndTransitions,
     invertPopulationProtocol,
     name,showNetName,states,transitions,initialStates,trueStates,falseStates,predicate,
     name,showNetName,states,transitions,initialStates,trueStates,falseStates,predicate,initialPredicate,
     pre,lpre,post,lpost,mpre,mpost,context,
     makePopulationProtocol,makePopulationProtocolWithTrans,
     makePopulationProtocolFromStrings,makePopulationProtocolWithTransFromStrings,
+2 −1
Original line number Diff line number Diff line
@@ -48,7 +48,8 @@ terminalConstraints pp m =
initialConfiguration :: PopulationProtocol -> SIMap State -> SBool
initialConfiguration pp m0 =
        (sum (mval m0 (initialStates pp)) .>= 2) &&&
        (sum (mval m0 (states pp \\ initialStates pp)) .== 0)
        (sum (mval m0 (states pp \\ initialStates pp)) .== 0) &&&
        (evaluateFormula (initialPredicate pp) m0)

differentConsensusConstraints :: Bool -> PopulationProtocol -> SIMap State -> SIMap State -> SIMap State -> SIMap State -> SIMap State -> SBool
differentConsensusConstraints checkCorrectness pp m0 m1 m2 qe qa =