Rewrote transition invariant constraints

src/Main.hs

@@ -29,7 +29,7 @@ import Structure
 import Solver
 import Solver.StateEquation
 import Solver.TrapConstraints
---import Solver.TransitionInvariant
+import Solver.TransitionInvariant
 --import Solver.LivenessInvariant
 --import Solver.SComponent
 --import Solver.CommFreeReachability
@@ -343,7 +343,7 @@ transformNet (net, props) TerminationByReachability =
             ps = [sigma, m1, m2] ++
                  places net ++ map primePlace (places net)
             is = [(Place "'m1", 1)] ++
-                 initials net ++ map (first primePlace) (initials net)
+                 linitials net ++ map (first primePlace) (linitials net)
             transformTransition t =
                 let (preT, postT) = context net t
                     pre'  = [(m1,1)] ++ preT  ++ map (first primePlace) preT
@@ -420,7 +420,7 @@ checkProperty verbosity net refine invariant p = do
         verbosePut verbosity 3 $ show p
         r <- case pcont p of
             (Safety pf) -> checkSafetyProperty verbosity net refine invariant pf
-            --(Liveness pf) -> checkLivenessProperty verbosity net refine invariant pf
+            (Liveness pf) -> checkLivenessProperty verbosity net refine invariant pf
             --(Structural ps) -> checkStructuralProperty verbosity net ps
         verbosePut verbosity 0 $ showPropertyName p ++ " " ++
             case r of
@@ -473,16 +473,17 @@ checkSafetyPropertyBySafetyRef verbosity net refine f traps = do
                                                 refine f (trap:traps)
                 else
                     return Unknown
-{-
+
 checkLivenessProperty :: Int -> PetriNet -> Bool -> Bool ->
-        Formula -> IO PropResult
+        Formula Transition -> IO PropResult
 checkLivenessProperty verbosity net refine invariant f = do
         (r, comps) <- checkLivenessPropertyByRef verbosity net refine f []
-        if r == Satisfied && invariant then
-            generateLivenessInvariant verbosity net f comps
-        else
-            return r
-
+        return r
+        --if r == Satisfied && invariant then
+        --    generateLivenessInvariant verbosity net f comps
+        --else
+        --    return r
+{-
 generateLivenessInvariant :: Int -> PetriNet ->
         Formula -> [SCompCut] -> IO PropResult
 generateLivenessInvariant verbosity net f comps = do
@@ -495,35 +496,25 @@ generateLivenessInvariant verbosity net f comps = do
                 let inv = getLivenessInvariant net cuts as
                 mapM_ print inv
                 return Satisfied
-
+-}
 checkLivenessPropertyByRef :: Int -> PetriNet -> Bool ->
-        Formula -> [SCompCut] -> IO (PropResult, [SCompCut])
-checkLivenessPropertyByRef verbosity net refine f comps = do
-        r <- checkSat $ checkTransitionInvariantSat net f comps
+        Formula Transition -> [Cut] -> IO (PropResult, [Cut])
+checkLivenessPropertyByRef verbosity net refine f cuts = do
+        r <- checkSat verbosity $ checkTransitionInvariantSat net f cuts
         case r of
-            Nothing -> return (Satisfied, comps)
-            Just ax -> do
-                let fired = firedTransitionsFromAssignment ax
-                verbosePut verbosity 1 "Assignment found"
-                verbosePut verbosity 2 $ "Transitions fired: " ++ show fired
-                verbosePut verbosity 3 $ "Assignment: " ++ show ax
+            Nothing -> return (Satisfied, cuts)
+            Just x -> do
                 if refine then do
-                    rt <- checkSat $ checkSComponentSat net fired ax
+                    rt <- return Nothing -- checkSat $ checkSComponentSat net x
                     case rt of
                         Nothing -> do
-                            verbosePut verbosity 1 "No S-component found"
-                            return (Unknown, comps)
-                        Just as -> do
-                            let sCompsCut = getSComponentCompsCut net ax as
-                            verbosePut verbosity 1 "S-component found"
-                            verbosePut verbosity 2 $ "Comps/Cut: " ++ show sCompsCut
-                            verbosePut verbosity 3 $ "S-Component assignment: " ++
-                                                      show as
+                            return (Unknown, cuts)
+                        Just cut -> do
                             checkLivenessPropertyByRef verbosity net refine f
-                                                  (sCompsCut:comps)
+                                                  (cut:cuts)
                 else
-                    return (Unknown, comps)
--}
+                    return (Unknown, cuts)
+
 checkStructuralProperty :: Int -> PetriNet -> Structure -> IO PropResult
 checkStructuralProperty _ net struct =
         if checkStructure net struct then

src/PetriNet.hs

@@ -2,12 +2,12 @@
 {-# OPTIONS_GHC -fno-warn-name-shadowing #-}
 
 module PetriNet
-    (PetriNet,Place(..),Transition(..),Marking,tokens,buildMarking,
-     marked,lmarked,makeMarking,
+    (PetriNet,Place(..),Transition(..),Marking,buildVector,
+     value,elems,items,makeVector,FiringVector,
      renamePlace,renameTransition,renamePetriNetPlacesAndTransitions,
-     name,showNetName,places,transitions,initial,initialMarking,
-     pre,lpre,post,lpost,initials,context,ghostTransitions,
-     makePetriNet,makePetriNetWithTrans,makePetriNetWith,Trap)
+     name,showNetName,places,transitions,initialMarking,initial,initials,linitials,
+     pre,lpre,post,lpost,context,ghostTransitions,
+     makePetriNet,makePetriNetWithTrans,makePetriNetWith,Trap,Cut)
 where
 
 import qualified Data.Map as M
@@ -42,30 +42,34 @@ instance Nodes Place Transition where
 instance Nodes Transition Place where
         contextMap = adjacencyT
 
-newtype Marking = Marking { getMarking :: M.Map Place Integer }
+newtype Vector a = Vector { getVector :: M.Map a Integer }
 
-instance Show Marking where
-        show (Marking m) =
-                "[" ++ intercalate "," (map showPlaceMarking (M.toList m)) ++ "]"
-            where showPlaceMarking (n,i) =
-                    show n ++ (if i /= 1 then "(" ++ show i ++ ")" else "")
+type Marking = Vector Place
+type FiringVector = Vector Transition
 
-tokens :: Marking -> Place -> Integer
-tokens m p = M.findWithDefault 0 p (getMarking m)
+instance (Show a) => Show (Vector a) where
+        show (Vector v) =
+                "[" ++ intercalate "," (map showEntry (M.toList v)) ++ "]"
+            where showEntry (v,x) =
+                    show v ++ (if x /= 1 then "(" ++ show x ++ ")" else "")
 
-buildMarking :: [(Place, Integer)] -> Marking
-buildMarking = makeMarking . M.fromList
+value :: (Ord a) => Vector a -> a -> Integer
+value v x = M.findWithDefault 0 x (getVector v)
 
-makeMarking :: M.Map Place Integer -> Marking
-makeMarking = Marking . M.filter (/=0)
+elems :: (Ord a) => Vector a -> [a]
+elems = M.keys . getVector
 
-marked :: Marking -> [Place]
-marked = M.keys . getMarking
+items :: Vector a -> [(a,Integer)]
+items = M.toList . getVector
 
-lmarked :: Marking -> [(Place,Integer)]
-lmarked = M.toList . getMarking
+buildVector :: (Ord a) => [(a, Integer)] -> Vector a
+buildVector = makeVector . M.fromList
+
+makeVector :: (Ord a) => M.Map a Integer -> Vector a
+makeVector = Vector . M.filter (/=0)
 
 type Trap = [Place]
+type Cut = ([[Transition]], [Transition])
 
 data PetriNet = PetriNet {
         name :: String,
@@ -78,10 +82,13 @@ data PetriNet = PetriNet {
 }
 
 initial :: PetriNet -> Place -> Integer
-initial net = tokens (initialMarking net)
+initial net = value (initialMarking net)
+
+initials :: PetriNet -> [Place]
+initials = elems . initialMarking
 
-initials :: PetriNet -> [(Place,Integer)]
-initials net = M.toList (getMarking (initialMarking net))
+linitials :: PetriNet -> [(Place,Integer)]
+linitials = items . initialMarking
 
 showNetName :: PetriNet -> String
 showNetName net = "Petri net" ++
@@ -116,8 +123,8 @@ renamePetriNetPlacesAndTransitions f net =
                     adjacencyP net,
                 adjacencyT  = mapAdjacency (renameTransition f) (renamePlace f) $
                     adjacencyT net,
-                initialMarking = Marking $
-                    M.mapKeys (renamePlace f) $ getMarking $ initialMarking net,
+                initialMarking = Vector $
+                    M.mapKeys (renamePlace f) $ getVector $ initialMarking net,
                 ghostTransitions = map (renameTransition f) $ ghostTransitions net
             }
         where mapAdjacency f g m = M.mapKeys f (M.map (mapContext g) m)
@@ -135,7 +142,7 @@ makePetriNet name places transitions arcs initial gs =
                 transitions = map Transition transitions,
                 adjacencyP = adP,
                 adjacencyT = adT,
-                initialMarking = buildMarking (map (first Place) initial),
+                initialMarking = buildVector (map (first Place) initial),
                 ghostTransitions = map Transition gs
             }
         where
@@ -173,7 +180,7 @@ makePetriNetWith name places ts initial gs =
                 transitions = transitions,
                 adjacencyP = placeMap,
                 adjacencyT = M.fromList ts,
-                initialMarking = buildMarking initial,
+                initialMarking = buildVector initial,
                 ghostTransitions = gs
             }
 

src/Printer/LOLA.hs

@@ -18,7 +18,7 @@ renderNet net =
             ps = "PLACE " <> intercalate ","
                     (map renderPlace (places net)) <> ";\n"
             is = "MARKING " <> intercalate ","
-                    (map showWeight (initials net)) <> ";\n"
+                    (map showWeight (linitials net)) <> ";\n"
             makeTransition t =
                 let (preT,postT) = context net t
                     preS = "CONSUME " <> intercalate ","

src/Printer/SARA.hs

@@ -58,7 +58,7 @@ renderDisjunction propname filename net f =
         "FILE " <> stringUtf8 (reverse (takeWhile (/='/') (reverse filename)))
             <> " TYPE LOLA;\n" <>
         "INITIAL " <> intercalate ","
-            (map (\(p,i) -> renderPlace p <> ":" <> integerDec i) (initials net))
+            (map (\(p,i) -> renderPlace p <> ":" <> integerDec i) (linitials net))
             <> ";\n" <>
         "FINAL COVER;\n" <>
         "CONSTRAINTS " <> renderConjunction f <> ";"

src/Solver.hs

 {-# LANGUAGE TypeSynonymInstances, FlexibleInstances #-}
 
 module Solver
-    (prime,checkSat,ModelReader,val,vals,VarMap,
+    (prime,checkSat,ModelReader,val,vals,valMap,VarMap,
      getNames,makeVarMap,makeVarMapWith,
      IntConstraint,BoolConstraint,IntResult,BoolResult,
      Model,ConstraintProblem)
@@ -34,10 +34,15 @@ val ma x = do
         mb <- ask
         return $ mb M.! (ma M.! x)
 
-vals :: (Ord a) => VarMap a -> ModelReader b (M.Map a b)
+valMap :: (Ord a) => VarMap a -> ModelReader b (M.Map a b)
+valMap ma = do
+        mb <- ask
+        return $ M.map (mb M.!) ma
+
+vals :: (Ord a) => VarMap a -> ModelReader b [b]
 vals ma = do
         mb <- ask
-        return $ fmap (mb M.!) ma
+        return $ M.elems $ M.map (mb M.!) ma
 
 makeVarMap :: (Show a, Ord a) => [a] -> VarMap a
 makeVarMap = makeVarMapWith id

src/Solver/StateEquation.hs

@@ -19,9 +19,7 @@ placeConstraints net m x =
                 outgoing <- mapM addTransition $ lpost net p
                 let pinit = literal $ initial net p
                 return $ pinit + sum incoming - sum outgoing .== mp
-              addTransition (t,w) = do
-                  xt <- val x t
-                  return $ literal w * xt
+              addTransition (t,w) = liftM (literal w *) (val x t)
 
 nonNegativityConstraints :: PetriNet -> VarMap Place -> VarMap Transition ->
         IntConstraint
@@ -63,5 +61,5 @@ checkStateEquationSat net f traps =
 
 markingFromAssignment :: VarMap Place -> IntResult Marking
 markingFromAssignment m =
-        liftM makeMarking (vals m)
+        liftM makeVector $ valMap m
 

src/Solver/TransitionInvariant.hs

 module Solver.TransitionInvariant
-    (checkTransitionInvariant,checkTransitionInvariantSat,
-     firedTransitionsFromAssignment)
+    (checkTransitionInvariantSat)
 where
 
 import Data.SBV
+import Control.Monad
 
 import PetriNet
 import Property
 import Solver
-import Solver.SComponent
+--import Solver.SComponent
 import Solver.Formula
 
-tInvariantConstraints :: PetriNet -> ModelSI -> SBool
-tInvariantConstraints net m =
-            bAnd $ map checkTransitionEquation $ places net
-        where checkTransitionEquation p =
-                let incoming = map addTransition $ lpre net p
-                    outgoing = map addTransition $ lpost net p
-                in  sum incoming - sum outgoing .>= 0
-              addTransition (t,w) = literal w * mVal m t
-
-finalInvariantConstraints :: ModelSI -> SBool
-finalInvariantConstraints m = sum (mValues m) .> 0
-
-nonnegativityConstraints :: ModelSI -> SBool
-nonnegativityConstraints m = bAnd $ map (.>= 0) $ mValues m
-
-checkSComponentTransitions :: [SCompCut] -> ModelSI -> SBool
-checkSComponentTransitions comps m =
+tInvariantConstraints :: PetriNet -> VarMap Transition -> IntConstraint
+tInvariantConstraints net x =
+            liftM bAnd $ mapM checkTransitionEquation $ places net
+        where checkTransitionEquation p = do
+                incoming <- mapM addTransition $ lpre net p
+                outgoing <- mapM addTransition $ lpost net p
+                return $ sum incoming - sum outgoing .>= 0
+              addTransition (t,w) = liftM (literal w *) (val x t)
+
+finalInvariantConstraints :: VarMap Transition -> IntConstraint
+finalInvariantConstraints x = do
+        xs <- vals x
+        return $ sum xs .> 0
+
+nonnegativityConstraints :: VarMap Transition -> IntConstraint
+nonnegativityConstraints x = do
+        xs <- vals x
+        return $ bAnd $ map (.>= 0) xs
+{-
+checkSComponentTransitions :: [Cut] -> VarMap Transition -> IntConstraint
+checkSComponentTransitions cuts x =
             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 Transition ->
+        [Cut] -> VarMap Transition -> IntConstraint
+checkTransitionInvariant net f cuts x = do
+        c1 <- tInvariantConstraints net x
+        c2 <- nonnegativityConstraints x
+        c3 <- finalInvariantConstraints x
+        --c4 <- checkSComponentTransitions cuts x
+        c5 <- evaluateFormula f x
+        return $ c1 &&& c2 &&& c3 &&& c3 &&& c5
+
+checkTransitionInvariantSat :: PetriNet -> Formula Transition -> [Cut] ->
+        ConstraintProblem Integer FiringVector
+checkTransitionInvariantSat net f cuts =
+       let x = makeVarMap $ transitions net
+       in  ("transition invariant constraints", "transition invariant",
+            getNames x,
+            checkTransitionInvariant net f cuts x,
+            firingVectorFromAssignment x)
+
+firingVectorFromAssignment :: VarMap Transition -> IntResult FiringVector
+firingVectorFromAssignment x =
+        liftM makeVector $ valMap x
 
-checkTransitionInvariant :: PetriNet -> Formula ->
-        [SCompCut] -> ModelSI -> SBool
-checkTransitionInvariant net f strans m =
-        tInvariantConstraints net m &&&
-        nonnegativityConstraints m &&&
-        finalInvariantConstraints m &&&
-        checkSComponentTransitions strans m &&&
-        evaluateFormula f m
-
-checkTransitionInvariantSat :: PetriNet -> Formula ->
-        [SCompCut] -> ([String], ModelSI -> SBool)
-checkTransitionInvariantSat net f strans =
-        (transitions net, checkTransitionInvariant net f strans)
-
-firedTransitionsFromAssignment :: ModelI -> [String]
-firedTransitionsFromAssignment = mElemsWith (> 0)

src/Solver/TrapConstraints.hs

@@ -19,11 +19,11 @@ trapConstraints net b =
 
 trapInitiallyMarked :: PetriNet -> VarMap Place -> BoolConstraint
 trapInitiallyMarked net b =
-        liftM bOr $ mapM (val b) $ marked $ initialMarking net
+        liftM bOr $ mapM (val b) $ initials net
 
 trapUnassigned :: Marking -> VarMap Place -> BoolConstraint
 trapUnassigned m b =
-        liftM bAnd $ mapM (liftM bnot . val b) $ marked m
+        liftM bAnd $ mapM (liftM bnot . val b) $ elems m
 
 checkTrap :: PetriNet -> Marking -> VarMap Place -> BoolConstraint
 checkTrap net m b = do
@@ -42,6 +42,6 @@ checkTrapSat net m =
 
 trapFromAssignment :: VarMap Place -> BoolResult Trap
 trapFromAssignment b = do
-        ps <- vals b
-        return $ M.keys $ M.filter id ps
+        bm <- valMap b
+        return $ M.keys $ M.filter id bm