Add option to specifiy initial predicate

src/Parser/PP.hs

@@ -141,6 +141,17 @@ quantFormula =
           <|>
         (ExQuantFormula [] <$> formula)
 
+instance FromJSON (Formula String) where
+          parseJSON (String v) = do
+                  let f = parse formula "" (T.unpack v)
+                  case f of
+                    Left e -> fail "Predicate formula not well-formed."
+                    Right r -> return r
+          parseJSON _ = fail "Expect string for predicate."
+
+instance ToJSON (Formula String) where
+        toJSON x = String ""
+
 instance FromJSON (QuantFormula String) where
           parseJSON (String v) = do
                   let formula = parse quantFormula "" (T.unpack v)
@@ -164,6 +175,7 @@ data RecordPP = RecordPP {
         transitions :: [RecordTransition],
         initialStates :: [String],
         trueStates :: [String],
+        initialPredicate :: Maybe (Formula String),
         predicate :: Maybe (QuantFormula String),
         description :: Maybe String
 } deriving (Show)
@@ -172,20 +184,22 @@ $(deriveJSON defaultOptions ''RecordTransition)
 $(deriveJSON defaultOptions ''RecordPP)
 
 recordPP2PopulationProtocol :: RecordPP -> PopulationProtocol
-recordPP2PopulationProtocol r = 
-  makePopulationProtocolFromStrings (title r) (states r) (map name (transitions r)) (initialStates r) (trueStates r) falseStates p  arcs where
+recordPP2PopulationProtocol r =
+  makePopulationProtocolFromStrings (title r) (states r) (map name (transitions r)) (initialStates r) (trueStates r) falseStates p ip arcs where
         falseStates = [q | q <- states r, not (S.member q (S.fromList (trueStates r)))]
-        arcs = [(q, name t, 1) |  t <- transitions r, q <- pre t] ++ 
+        arcs = [(q, name t, 1) |  t <- transitions r, q <- pre t] ++
                [(name t, q, 1) | t <- transitions r, q <- post t]
-        p = case predicate r of Nothing -> ExQuantFormula [] FTrue 
+        p = case predicate r of Nothing -> ExQuantFormula [] FTrue
                                 (Just p') -> p'
+        ip = case initialPredicate r of Nothing -> FTrue
+                                        (Just p') -> p'
 
 parseContent :: Parser PopulationProtocol
-parseContent  = do 
+parseContent  = do
   str <- manyTill anyChar eof
   let r = eitherDecode (BS.pack str)
   case r of
     (Left e) ->  fail e
     (Right pp) -> return (recordPP2PopulationProtocol pp)
- 
+
 

src/PopulationProtocol.hs

@@ -78,6 +78,7 @@ data PopulationProtocol = PopulationProtocol {
         trueStates :: [State],
         falseStates :: [State],
         predicate :: QuantFormula State,
+        initialPredicate :: Formula State,
         adjacencyQ :: M.Map State ([(Transition,Integer)], [(Transition,Integer)]),
         adjacencyT :: M.Map Transition ([(State,Integer)], [(State,Integer)])
 }
@@ -94,6 +95,7 @@ instance Show PopulationProtocol where
                    "\nTrue states    : " ++ show (trueStates pp) ++
                    "\nFalse states   : " ++ show (falseStates pp) ++
                    "\nPredicate      : " ++ show (predicate pp) ++
+                   "\nInitial pred.  : " ++ show (initialPredicate pp) ++
                    "\nState arcs     :\n" ++ unlines
                         (map showContext (M.toList (adjacencyQ pp))) ++
                    "\nTransition arcs:\n" ++ unlines
@@ -123,6 +125,8 @@ renameStatesAndTransitions f pp =
                     listSet $ map (renameState f) $ falseStates pp,
                 predicate =
                     fmap (renameState f) $ predicate pp,
+                initialPredicate =
+                    fmap (renameState f) $ initialPredicate pp,
                 adjacencyQ  = mapAdjacency (renameState f) (renameTransition f) $
                     adjacencyQ pp,
                 adjacencyT  = mapAdjacency (renameTransition f) (renameState f) $
@@ -142,6 +146,7 @@ invertPopulationProtocol pp =
                 trueStates       = trueStates pp,
                 falseStates      = falseStates pp,
                 predicate        = predicate pp,
+                initialPredicate = initialPredicate pp,
                 adjacencyQ       = M.map swap $ adjacencyQ pp,
                 adjacencyT       = M.map swap $ adjacencyT pp
             }
@@ -149,10 +154,10 @@ invertPopulationProtocol pp =
 
 
 makePopulationProtocol :: String -> [State] -> [Transition] ->
-        [State] -> [State] -> [State] -> QuantFormula State ->
+        [State] -> [State] -> [State] -> QuantFormula State -> Formula State ->
         [Either (Transition, State, Integer) (State, Transition, Integer)] ->
         PopulationProtocol
-makePopulationProtocol name states transitions initialStates trueStates falseStates predicate arcs =
+makePopulationProtocol name states transitions initialStates trueStates falseStates predicate initialPredicate arcs =
             PopulationProtocol {
                 name = name,
                 states = listSet states,
@@ -161,6 +166,7 @@ makePopulationProtocol name states transitions initialStates trueStates falseSta
                 trueStates = listSet trueStates,
                 falseStates = listSet falseStates,
                 predicate = predicate,
+                initialPredicate = initialPredicate,
                 adjacencyQ = M.map (listMap *** listMap) adQ,
                 adjacencyT = M.map (listMap *** listMap) adT
             }
@@ -183,8 +189,8 @@ makePopulationProtocol name states transitions initialStates trueStates falseSta
             addArc (lNew,rNew) (lOld,rOld) = (lNew ++ lOld,rNew ++ rOld)
 
 makePopulationProtocolFromStrings :: String -> [String] -> [String] -> [String] -> [String] -> [String] ->
-        QuantFormula String -> [(String, String, Integer)] -> PopulationProtocol
-makePopulationProtocolFromStrings name states transitions initialStates trueStates falseStates predicate arcs =
+        QuantFormula String -> Formula String -> [(String, String, Integer)] -> PopulationProtocol
+makePopulationProtocolFromStrings name states transitions initialStates trueStates falseStates predicate initialPredicate arcs =
             makePopulationProtocol
                 name
                 (map State (S.toAscList stateSet))
@@ -193,6 +199,7 @@ makePopulationProtocolFromStrings name states transitions initialStates trueStat
                 (map State trueStates)
                 (map State falseStates)
                 (fmap State predicate)
+                (fmap State initialPredicate)
                 (map toEitherArc arcs)
         where
             stateSet = S.fromList states
@@ -217,18 +224,18 @@ makePopulationProtocolFromStrings name states transitions initialStates trueStat
                             error $ l ++ " and " ++ r ++ " both transitions"
 
 makePopulationProtocolWithTrans :: String -> [State] -> [State] -> [State] -> [State] ->
-        QuantFormula State -> [(Transition, ([(State, Integer)], [(State, Integer)]))] ->
+        QuantFormula State -> Formula State -> [(Transition, ([(State, Integer)], [(State, Integer)]))] ->
         PopulationProtocol
-makePopulationProtocolWithTrans name states initialStates trueStates falseStates predicate ts =
-            makePopulationProtocol name states (map fst ts) initialStates trueStates falseStates predicate arcs
+makePopulationProtocolWithTrans name states initialStates trueStates falseStates predicate initialPredicate ts =
+            makePopulationProtocol name states (map fst ts) initialStates trueStates falseStates predicate initialPredicate arcs
         where
             arcs = [ Right (q,t,w) | (t,(is,_)) <- ts, (q,w) <- is ] ++
                    [ Left  (t,q,w) | (t,(_,os)) <- ts, (q,w) <- os ]
 
 makePopulationProtocolWithTransFromStrings :: String -> [String] -> [String] -> [String] -> [String] ->
-        QuantFormula String -> [(String, ([(String, Integer)], [(String, Integer)]))] ->
+        QuantFormula String -> Formula String -> [(String, ([(String, Integer)], [(String, Integer)]))] ->
         PopulationProtocol
-makePopulationProtocolWithTransFromStrings name states initialStates trueStates falseStates predicate arcs =
+makePopulationProtocolWithTransFromStrings name states initialStates trueStates falseStates predicate initialPredicate arcs =
             makePopulationProtocolWithTrans
                 name
                 (map State states)
@@ -236,6 +243,7 @@ makePopulationProtocolWithTransFromStrings name states initialStates trueStates
                 (map State trueStates)
                 (map State falseStates)
                 (fmap State predicate)
+                (fmap State initialPredicate)
                 (map toTArc arcs)
         where
             toTArc (t, (iq, oq)) =