Better liveness invariant generation and display

src/Main.hs

@@ -435,16 +435,17 @@ checkProperty verbosity net refine invariant p = do
 checkSafetyProperty :: Int -> PetriNet -> Bool -> Bool ->
         Formula -> IO PropResult
 checkSafetyProperty verbosity net refine invariant f =
-        -- TODO: add invariant generation
-        if invariant then
-            error "Invariant generation for safety properties not yet supported"
-        else
-            -- TODO: add flag for this kind of structural check
-            if checkCommunicationFree net then do
-                verbosePut verbosity 1 "Net found to be communication-free"
-                checkSafetyPropertyByCommFree verbosity net f
+        -- TODO: add flag for this kind of structural check
+        if checkCommunicationFree net then do
+            verbosePut verbosity 1 "Net found to be communication-free"
+            checkSafetyPropertyByCommFree verbosity net f
+        else do
+            r <- checkSafetyPropertyBySafetyRef verbosity net refine f []
+            if r == Satisfied && invariant then
+                -- TODO: add invariant generation
+                error "Invariant generation for safety properties not yet supported"
             else
-                checkSafetyPropertyBySafetyRef verbosity net refine f []
+                return r
 
 checkSafetyPropertyByCommFree :: Int -> PetriNet -> Formula -> IO PropResult
 checkSafetyPropertyByCommFree verbosity net f = do
@@ -489,7 +490,7 @@ checkLivenessProperty :: Int -> PetriNet -> Bool -> Bool ->
         Formula -> IO PropResult
 checkLivenessProperty verbosity net refine invariant f = do
         (r, comps) <- checkLivenessPropertyByRef verbosity net refine f []
-        if (r == Satisfied && invariant) then
+        if r == Satisfied && invariant then
             generateLivenessInvariant verbosity net f comps
         else
             return r
@@ -498,15 +499,14 @@ generateLivenessInvariant :: Int -> PetriNet ->
         Formula -> [SCompCut] -> IO PropResult
 generateLivenessInvariant verbosity net f comps = do
         verbosePut verbosity 1 "Generating invariant"
-        if f /= FTrue then
-            error "formula not yet supported"
-        else do
-            r <- checkSat $ checkLivenessInvariantSat net comps
-            case r of
-                Nothing -> return Unsatisfied
-                Just as -> do
-                    putStrLn $ show as
-                    return Satisfied
+        let cuts = generateCuts f comps
+        r <- checkSat $ checkLivenessInvariantSat net cuts
+        case r of
+            Nothing -> return Unsatisfied
+            Just as -> do
+                let inv = getLivenessInvariant net cuts as
+                mapM_ print inv
+                return Satisfied
 
 checkLivenessPropertyByRef :: Int -> PetriNet -> Bool ->
         Formula -> [SCompCut] -> IO (PropResult, [SCompCut])

src/Property.hs

@@ -90,6 +90,8 @@ renameFormula f (Neg p) = Neg (renameFormula f p)
 renameFormula f (p :&: q) = renameFormula f p :&: renameFormula f q
 renameFormula f (p :|: q) = renameFormula f p :|: renameFormula f q
 
+-- TODO: add functions to transform formula to CNF/DNF
+
 data PropertyType = SafetyType
                   | LivenessType
                   | StructuralType

src/Solver/LivenessInvariant.hs

 module Solver.LivenessInvariant (
     checkLivenessInvariant
   , checkLivenessInvariantSat
+  , generateCuts
   , getLivenessInvariant
   , PlaceVector
-  , LivenessInvariant
+  , LivenessInvariant(..)
 ) where
 
 import Data.SBV
+import Data.List (intercalate)
 
 import Solver
 import Solver.SComponent
+import Property
 import PetriNet
 
 type PlaceVector = [(String, Integer)]
-type LivenessInvariant = [PlaceVector]
+newtype LivenessInvariant =
+        LivenessInvariant { getInv :: (String, [Cut], PlaceVector) }
+
+instance Show LivenessInvariant where
+        show (LivenessInvariant (n, cs, xs)) = n ++ " [" ++
+                    intercalate " ∧ " (map showTrans cs) ++ "]: " ++
+                    intercalate " + " (map showPlace (filter ((> 0) . snd) xs))
+                where showPlace (p, w) = show w ++ p
+                      showTrans (ts, b) =
+                          if b then
+                               intercalate " ∧ " (map (++ " ∉ σ") ts)
+                          else
+                               let d = intercalate " ∨ " (map (++ " ∈ σ") ts)
+                               in  if length ts == 1 then d else "(" ++ d ++ ")"
 
 type Cut = ([String], Bool)
 type NamedCut = (String, [(String, Cut)])
 
-nameCuts :: [[Cut]] -> [NamedCut]
-nameCuts cuts =
-            map (\(n, c) -> (n, numPref "@comp" `zip` c)) $
-                numPref "@cut" `zip` cuts
+generateCuts :: Formula -> [SCompCut] -> [NamedCut]
+generateCuts f comps =
+            zipWith nameCut
+                (numPref "@part")
+                (foldl combine [formulaToCut f] comps)
         where
+            nameCut n c = (n, numPref "@comp" `zip` c)
             numPref s = map (\i -> s ++ show i) [(1::Integer)..]
+            combine cuts compCut = [x : c | x <- compCut, c <- cuts]
 
 varNames :: PetriNet -> [NamedCut] -> [String]
 varNames net = concatMap cutNames
@@ -33,12 +52,25 @@ varNames net = concatMap cutNames
                 map (\p -> n ++ "@p" ++ p) (places net) ++
                 map (\(n', _) -> n ++ n') c
 
-foldComps :: [SCompCut] -> [[Cut]]
-foldComps = foldl combine [[]]
+formulaToCut :: Formula -> SCompCut
+formulaToCut = transformConj
         where
-            combine cuts (t1, t2, u) =
-                concatMap
-                    (\c -> [(t1, True) : c, (t2, True) : c, (u, False) : c]) cuts
+            transformConj FTrue = []
+            transformConj (p :&: q) = transformConj p ++ transformConj q
+            transformConj (Atom lieq) = transformLieq lieq
+            transformConj form =
+                error $ "formula not supported for invariant: " ++ show form
+            transformLieq (LinIneq ts Gt (Const 0)) = [(transformTerm ts, False)]
+            transformLieq (LinIneq ts Ge (Const 1)) = [(transformTerm ts, False)]
+            transformLieq (LinIneq ts Eq (Const 0)) = [(transformTerm ts, True)]
+            transformLieq (LinIneq ts Le (Const 0)) = [(transformTerm ts, True)]
+            transformLieq (LinIneq ts Lt (Const 1)) = [(transformTerm ts, True)]
+            transformLieq l =
+                error $ "linear inequation not supported for invariant: " ++ show l
+            transformTerm (t :+: u) = transformTerm t ++ transformTerm u
+            transformTerm (Var x) = [x]
+            transformTerm t =
+                error $ "term not supported for invariant: " ++ show t
 
 checkCut :: PetriNet -> ModelSI -> NamedCut -> SBool
 checkCut net m (n, comps) =
@@ -67,13 +99,14 @@ checkLivenessInvariant :: PetriNet -> [NamedCut] ->
 checkLivenessInvariant net cuts m =
         bAnd (map (checkCut net m) cuts)
 
-checkLivenessInvariantSat :: PetriNet -> [SCompCut] ->
+checkLivenessInvariantSat :: PetriNet -> [NamedCut] ->
         ([String], ModelSI -> SBool)
-checkLivenessInvariantSat net comps =
-        let cuts = foldComps comps
-            namedCuts = nameCuts cuts
-            names = varNames net namedCuts
-        in  (names, checkLivenessInvariant net namedCuts)
+checkLivenessInvariantSat net cuts =
+        (varNames net cuts, checkLivenessInvariant net cuts)
+
+getLivenessInvariant :: PetriNet -> [NamedCut] -> ModelI -> [LivenessInvariant]
+getLivenessInvariant net cuts as = map lookupCut cuts
+        where lookupCut (n, c) = LivenessInvariant
+               (n, map snd c, map (\p -> (p, mVal as (n ++ "@p" ++ p))) (places net))
+
 
-getLivenessInvariant :: PetriNet -> [SCompCut] -> ModelI -> LivenessInvariant
-getLivenessInvariant net ax as = undefined

src/Solver/SComponent.hs

@@ -11,7 +11,7 @@ import Data.List (partition)
 import PetriNet
 import Solver
 
-type SCompCut = ([String], [String], [String])
+type SCompCut = [([String], Bool)]
 
 checkPrePostPlaces :: PetriNet -> ModelSI -> SBool
 checkPrePostPlaces net m =
@@ -81,5 +81,5 @@ getSComponentCompsCut :: PetriNet -> ModelI -> ModelI -> SCompCut
 getSComponentCompsCut net ax as =
         let (t, u) = partition (cElem ax) $ filter (cElem as) (transitions net)
             (t1, t2) = partition (cElem as . prime) t
-        in  (t1, t2, u)
+        in  [(t1, True), (t2, True), (u, False)]
 

src/Solver/TransitionInvariant.hs

@@ -27,11 +27,12 @@ nonnegativityConstraints :: ModelSI -> SBool
 nonnegativityConstraints m = bAnd $ map (.>= 0) $ mValues m
 
 checkSComponentTransitions :: [SCompCut] -> ModelSI -> SBool
-checkSComponentTransitions strans m = bAnd $ map checkCompsCut strans
-        where checkCompsCut (t1,t2,u) =
-                bOr (map (\t -> mVal m t .> 0) t1) &&&
-                bOr (map (\t -> mVal m t .> 0) t2) ==>
-                bOr (map (\t -> mVal m t .> 0) u)
+checkSComponentTransitions comps m =
+            bAnd $ map (bOr . map checkCompsCut) comps
+        where checkCompsCut (ts,w) =
+              -- TODO: check how changing the representation changes result
+                let tc t = mVal m t .> 0
+                in  if w then bnot (bOr (map tc ts)) else bOr (map tc ts)
 
 checkTransitionInvariant :: PetriNet -> Formula ->
         [SCompCut] -> ModelSI -> SBool