Notice to GitKraken users: A vulnerability has been found in the SSH key generation of GitKraken versions 7.6.0 to 8.0.0 (https://www.gitkraken.com/blog/weak-ssh-key-fix). If you use GitKraken and have generated a SSH key using one of these versions, please remove it both from your local workstation and from your LRZ GitLab profile.

21.10.2021, 9:00 - 11:00: Due to updates GitLab may be unavailable for some minutes between 09:00 and 11:00.

Commit 6e12e50e authored by Philipp J. Meyer's avatar Philipp J. Meyer
Browse files

added option to check reachability of non-consensus states

parent 7a3e1c37
...@@ -38,6 +38,7 @@ import Solver.SComponentWithCut ...@@ -38,6 +38,7 @@ import Solver.SComponentWithCut
import Solver.SComponent import Solver.SComponent
import Solver.Simplifier import Solver.Simplifier
import Solver.UniqueTerminalMarking import Solver.UniqueTerminalMarking
import Solver.NonConsensusState
--import Solver.Interpolant --import Solver.Interpolant
--import Solver.CommFreeReachability --import Solver.CommFreeReachability
...@@ -165,7 +166,7 @@ transformNet (net, props) TerminationByReachability = ...@@ -165,7 +166,7 @@ transformNet (net, props) TerminationByReachability =
(places net)) (places net))
-- TODO: map existing liveness properties -- TODO: map existing liveness properties
in (makePetriNetWithTrans (name net) ps ts is in (makePetriNetWithTrans (name net) ps ts is
(ghostTransitions net) (fixedTraps net) (fixedSiphons net), prop : props) (ghostTransitions net) (fixedTraps net) (fixedSiphons net) (yesStates net) (noStates net), prop : props)
transformNet (net, props) ValidateIdentifiers = transformNet (net, props) ValidateIdentifiers =
(renamePetriNetPlacesAndTransitions validateId net, (renamePetriNetPlacesAndTransitions validateId net,
map (renameProperty validateId) props) map (renameProperty validateId) props)
...@@ -217,6 +218,8 @@ makeImplicitProperty _ StructCommunicationFree = ...@@ -217,6 +218,8 @@ makeImplicitProperty _ StructCommunicationFree =
Property "communication free" $ Structural CommunicationFree Property "communication free" $ Structural CommunicationFree
makeImplicitProperty _ UniqueTerminalMarking = makeImplicitProperty _ UniqueTerminalMarking =
Property "unique terminal marking" $ Constraint UniqueTerminalMarkingConstraint Property "unique terminal marking" $ Constraint UniqueTerminalMarkingConstraint
makeImplicitProperty _ NonConsensusState =
Property "non-consensus state" $ Constraint NonConsensusStateConstraint
checkProperty :: PetriNet -> Property -> OptIO PropResult checkProperty :: PetriNet -> Property -> OptIO PropResult
checkProperty net p = do checkProperty net p = do
...@@ -444,6 +447,7 @@ checkConstraintProperty :: PetriNet -> ConstraintProperty -> OptIO PropResult ...@@ -444,6 +447,7 @@ checkConstraintProperty :: PetriNet -> ConstraintProperty -> OptIO PropResult
checkConstraintProperty net cp = checkConstraintProperty net cp =
case cp of case cp of
UniqueTerminalMarkingConstraint -> checkUniqueTerminalMarkingProperty net UniqueTerminalMarkingConstraint -> checkUniqueTerminalMarkingProperty net
NonConsensusStateConstraint -> checkNonConsensusStateProperty net
checkUniqueTerminalMarkingProperty :: PetriNet -> OptIO PropResult checkUniqueTerminalMarkingProperty :: PetriNet -> OptIO PropResult
checkUniqueTerminalMarkingProperty net = do checkUniqueTerminalMarkingProperty net = do
...@@ -459,29 +463,66 @@ checkUniqueTerminalMarkingProperty' net traps siphons = do ...@@ -459,29 +463,66 @@ checkUniqueTerminalMarkingProperty' net traps siphons = do
r <- checkSat $ checkUniqueTerminalMarkingSat net traps siphons r <- checkSat $ checkUniqueTerminalMarkingSat net traps siphons
case r of case r of
Nothing -> return (Nothing, traps, siphons) Nothing -> return (Nothing, traps, siphons)
Just m -> do Just c -> do
refine <- opt optRefinementType refine <- opt optRefinementType
if isJust refine then if isJust refine then
refineUniqueTerminalMarkingProperty net traps siphons m refineUniqueTerminalMarkingProperty net traps siphons c
else else
return (Just m, traps, siphons) return (Just c, traps, siphons)
refineUniqueTerminalMarkingProperty :: PetriNet -> refineUniqueTerminalMarkingProperty :: PetriNet ->
[Trap] -> [Siphon] -> UniqueTerminalMarkingCounterExample -> [Trap] -> [Siphon] -> UniqueTerminalMarkingCounterExample ->
OptIO (Maybe UniqueTerminalMarkingCounterExample, [Trap], [Siphon]) OptIO (Maybe UniqueTerminalMarkingCounterExample, [Trap], [Siphon])
refineUniqueTerminalMarkingProperty net traps siphons m@(m0, m1, m2, x1, x2) = do refineUniqueTerminalMarkingProperty net traps siphons c@(m0, m1, m2, x1, x2) = do
r1 <- checkSatMin $ checkUnmarkedTrapSat net m0 m1 m2 x1 x2 r1 <- checkSatMin $ Solver.UniqueTerminalMarking.checkUnmarkedTrapSat net m0 m1 m2 x1 x2
case r1 of case r1 of
Nothing -> do Nothing -> do
r2 <- checkSatMin $ checkUnmarkedSiphonSat net m0 m1 m2 x1 x2 r2 <- checkSatMin $ Solver.UniqueTerminalMarking.checkUnmarkedSiphonSat net m0 m1 m2 x1 x2
case r2 of case r2 of
Nothing -> Nothing ->
return (Just m, traps, siphons) return (Just c, traps, siphons)
Just siphon -> Just siphon ->
checkUniqueTerminalMarkingProperty' net traps (siphon:siphons) checkUniqueTerminalMarkingProperty' net traps (siphon:siphons)
Just trap -> Just trap ->
checkUniqueTerminalMarkingProperty' net (trap:traps) siphons checkUniqueTerminalMarkingProperty' net (trap:traps) siphons
checkNonConsensusStateProperty :: PetriNet -> OptIO PropResult
checkNonConsensusStateProperty net = do
r <- checkNonConsensusStateProperty' net (fixedTraps net) (fixedSiphons net)
case r of
(Nothing, _, _) -> return Satisfied
(Just _, _, _) -> return Unknown
checkNonConsensusStateProperty' :: PetriNet ->
[Trap] -> [Siphon] ->
OptIO (Maybe NonConsensusStateCounterExample, [Trap], [Siphon])
checkNonConsensusStateProperty' net traps siphons = do
r <- checkSat $ checkNonConsensusStateSat net traps siphons
case r of
Nothing -> return (Nothing, traps, siphons)
Just c -> do
refine <- opt optRefinementType
if isJust refine then
refineNonConsensusStateProperty net traps siphons c
else
return (Just c, traps, siphons)
refineNonConsensusStateProperty :: PetriNet ->
[Trap] -> [Siphon] -> NonConsensusStateCounterExample ->
OptIO (Maybe NonConsensusStateCounterExample, [Trap], [Siphon])
refineNonConsensusStateProperty net traps siphons c@(m0, m, x) = do
r1 <- checkSatMin $ Solver.NonConsensusState.checkUnmarkedTrapSat net m0 m x
case r1 of
Nothing -> do
r2 <- checkSatMin $ Solver.NonConsensusState.checkUnmarkedSiphonSat net m0 m x
case r2 of
Nothing ->
return (Just c, traps, siphons)
Just siphon ->
checkNonConsensusStateProperty' net traps (siphon:siphons)
Just trap ->
checkNonConsensusStateProperty' net (trap:traps) siphons
main :: IO () main :: IO ()
main = do main = do
putStrLn "SLAPnet - Safety and Liveness Analysis of Petri Nets with SMT solvers\n" putStrLn "SLAPnet - Safety and Liveness Analysis of Petri Nets with SMT solvers\n"
......
...@@ -32,6 +32,7 @@ data ImplicitProperty = Termination ...@@ -32,6 +32,7 @@ data ImplicitProperty = Termination
| StructFinalPlace | StructFinalPlace
| StructCommunicationFree | StructCommunicationFree
| UniqueTerminalMarking | UniqueTerminalMarking
| NonConsensusState
deriving (Show,Read) deriving (Show,Read)
data RefinementType = TrapRefinement | SComponentRefinement | SComponentWithCutRefinement data RefinementType = TrapRefinement | SComponentRefinement | SComponentWithCutRefinement
...@@ -184,6 +185,12 @@ options = ...@@ -184,6 +185,12 @@ options =
})) }))
"Prove that all markings of the net have a unique terminal marking" "Prove that all markings of the net have a unique terminal marking"
, Option "" ["non-consensus-state"]
(NoArg (\opt -> Right opt {
optProperties = NonConsensusState : optProperties opt
}))
"Prove that no non-consensus terminal state is reachable from an initial marking"
, Option "i" ["invariant"] , Option "i" ["invariant"]
(NoArg (\opt -> Right opt { optInvariant = True })) (NoArg (\opt -> Right opt { optInvariant = True }))
"Generate an invariant" "Generate an invariant"
......
...@@ -57,7 +57,7 @@ net = do ...@@ -57,7 +57,7 @@ net = do
initial <- option [] markingList initial <- option [] markingList
_ <- semi _ <- semi
ts <- many1 transition ts <- many1 transition
return $ makePetriNetWithTransFromStrings "" ps ts initial [] [] [] return $ makePetriNetWithTransFromStrings "" ps ts initial [] [] [] [] []
placeLists :: Parser [String] placeLists :: Parser [String]
placeLists = placeLists =
......
...@@ -58,7 +58,7 @@ net = do ...@@ -58,7 +58,7 @@ net = do
reserved "init" reserved "init"
(is,initTrans) <- initial (is,initTrans) <- initial
return $ makePetriNetWithTransFromStrings "" ps (initTrans ++ ts) is return $ makePetriNetWithTransFromStrings "" ps (initTrans ++ ts) is
(map fst initTrans) [] [] (map fst initTrans) [] [] [] []
prop :: Parser Property prop :: Parser Property
prop = do prop = do
......
...@@ -87,6 +87,12 @@ trap = reserved "trap" *> identList ...@@ -87,6 +87,12 @@ trap = reserved "trap" *> identList
siphon :: Parser [String] siphon :: Parser [String]
siphon = reserved "siphon" *> identList siphon = reserved "siphon" *> identList
yesStates :: Parser [String]
yesStates = reserved "yes" *> identList
noStates :: Parser [String]
noStates = reserved "no" *> identList
arc :: Parser [(String,String,Integer)] arc :: Parser [(String,String,Integer)]
arc = do arc = do
lhs <- identList lhs <- identList
...@@ -108,7 +114,8 @@ arcs = do ...@@ -108,7 +114,8 @@ arcs = do
data Statement = Places [String] | Transitions [String] | data Statement = Places [String] | Transitions [String] |
Arcs [(String,String,Integer)] | Initial [(String,Integer)] | Arcs [(String,String,Integer)] | Initial [(String,Integer)] |
TrapStatement [String] | SiphonStatement [String] TrapStatement [String] | SiphonStatement [String] |
YesStatement [String] | NoStatement [String]
statement :: Parser Statement statement :: Parser Statement
statement = Places <$> places <|> statement = Places <$> places <|>
...@@ -116,7 +123,9 @@ statement = Places <$> places <|> ...@@ -116,7 +123,9 @@ statement = Places <$> places <|>
Arcs <$> arcs <|> Arcs <$> arcs <|>
Initial <$> initial <|> Initial <$> initial <|>
TrapStatement <$> trap <|> TrapStatement <$> trap <|>
SiphonStatement <$> siphon SiphonStatement <$> siphon <|>
YesStatement <$> yesStates <|>
NoStatement <$> noStates
petriNet :: Parser PetriNet petriNet :: Parser PetriNet
petriNet = do petriNet = do
...@@ -124,16 +133,18 @@ petriNet = do ...@@ -124,16 +133,18 @@ petriNet = do
reserved "net" reserved "net"
name <- option "" ident name <- option "" ident
statements <- braces (many statement) statements <- braces (many statement)
let (p,t,a,i,traps,siphons) = foldl splitStatement ([],[],[],[],[],[]) statements let (p,t,a,i,traps,siphons,yesStates,noStates) = foldl splitStatement ([],[],[],[],[],[],[],[]) statements
return $ makePetriNetFromStrings name p t a i [] traps siphons return $ makePetriNetFromStrings name p t a i [] traps siphons yesStates noStates
where where
splitStatement (ps,ts,as,is,traps,siphons) stmnt = case stmnt of splitStatement (ps,ts,as,is,traps,siphons,ys,ns) stmnt = case stmnt of
Places p -> (p ++ ps,ts,as,is,traps,siphons) Places p -> (p ++ ps,ts,as,is,traps,siphons,ys,ns)
Transitions t -> (ps,t ++ ts,as,is,traps,siphons) Transitions t -> (ps,t ++ ts,as,is,traps,siphons,ys,ns)
Arcs a -> (ps,ts,a ++ as,is,traps,siphons) Arcs a -> (ps,ts,a ++ as,is,traps,siphons,ys,ns)
Initial i -> (ps,ts,as,i ++ is,traps,siphons) Initial i -> (ps,ts,as,i ++ is,traps,siphons,ys,ns)
TrapStatement trap -> (ps,ts,as,is,trap:traps,siphons) TrapStatement trap -> (ps,ts,as,is,trap:traps,siphons,ys,ns)
SiphonStatement siphon -> (ps,ts,as,is,traps,siphon:siphons) SiphonStatement siphon -> (ps,ts,as,is,traps,siphon:siphons,ys,ns)
YesStatement y -> (ps,ts,as,is,traps,siphons,y ++ ys,ns)
NoStatement n -> (ps,ts,as,is,traps,siphons,ys,n ++ ns)
binary :: String -> (a -> a -> a) -> Assoc -> Operator String () Identity a binary :: String -> (a -> a -> a) -> Assoc -> Operator String () Identity a
binary name fun = Infix ( reservedOp name *> return fun ) binary name fun = Infix ( reservedOp name *> return fun )
......
...@@ -77,7 +77,7 @@ petriNet = do ...@@ -77,7 +77,7 @@ petriNet = do
ts <- many transition ts <- many transition
let places = [ p | (p,_) <- ps ] let places = [ p | (p,_) <- ps ]
initial = [ (p,i) | (p,Just i) <- ps ] initial = [ (p,i) | (p,Just i) <- ps ]
return $ makePetriNetWithTransFromStrings "" places ts initial [] [] [] return $ makePetriNetWithTransFromStrings "" places ts initial [] [] [] [] []
parseContent :: Parser (PetriNet,[Property]) parseContent :: Parser (PetriNet,[Property])
parseContent = do parseContent = do
......
...@@ -8,6 +8,7 @@ module PetriNet ...@@ -8,6 +8,7 @@ module PetriNet
name,showNetName,places,transitions, name,showNetName,places,transitions,
initialMarking,initial,initials,linitials, initialMarking,initial,initials,linitials,
pre,lpre,post,lpost,mpre,mpost,context,ghostTransitions,fixedTraps,fixedSiphons, pre,lpre,post,lpost,mpre,mpost,context,ghostTransitions,fixedTraps,fixedSiphons,
yesStates,noStates,
makePetriNet,makePetriNetWithTrans, makePetriNet,makePetriNetWithTrans,
makePetriNetFromStrings,makePetriNetWithTransFromStrings,Trap,Siphon,Cut, makePetriNetFromStrings,makePetriNetWithTransFromStrings,Trap,Siphon,Cut,
constructCut,SimpleCut,Invariant(..)) constructCut,SimpleCut,Invariant(..))
...@@ -81,7 +82,9 @@ data PetriNet = PetriNet { ...@@ -81,7 +82,9 @@ data PetriNet = PetriNet {
initialMarking :: Marking, initialMarking :: Marking,
ghostTransitions :: [Transition], ghostTransitions :: [Transition],
fixedTraps :: [Trap], fixedTraps :: [Trap],
fixedSiphons :: [Siphon] fixedSiphons :: [Siphon],
yesStates :: [Place],
noStates :: [Place]
} }
initial :: PetriNet -> Place -> Integer initial :: PetriNet -> Place -> Integer
...@@ -108,7 +111,9 @@ instance Show PetriNet where ...@@ -108,7 +111,9 @@ instance Show PetriNet where
"\nInitial: " ++ show (initialMarking net) ++ "\nInitial: " ++ show (initialMarking net) ++
"\nGhost transitions: " ++ show (ghostTransitions net) ++ "\nGhost transitions: " ++ show (ghostTransitions net) ++
"\nFixed traps: " ++ show (fixedTraps net) ++ "\nFixed traps: " ++ show (fixedTraps net) ++
"\nFixed siphons: " ++ show (fixedSiphons net) "\nFixed siphons: " ++ show (fixedSiphons net) ++
"\nYes states: " ++ show (yesStates net) ++
"\nNo states: " ++ show (noStates net)
where showContext (s,(l,r)) = where showContext (s,(l,r)) =
show l ++ " -> " ++ show s ++ " -> " ++ show r show l ++ " -> " ++ show s ++ " -> " ++ show r
...@@ -149,7 +154,9 @@ renamePetriNetPlacesAndTransitions f net = ...@@ -149,7 +154,9 @@ renamePetriNetPlacesAndTransitions f net =
ghostTransitions = ghostTransitions =
listSet $ map (renameTransition f) $ ghostTransitions net, listSet $ map (renameTransition f) $ ghostTransitions net,
fixedTraps = map (map $ renamePlace f) $ fixedTraps net, fixedTraps = map (map $ renamePlace f) $ fixedTraps net,
fixedSiphons = map (map $ renamePlace f) $ fixedSiphons net fixedSiphons = map (map $ renamePlace f) $ fixedSiphons net,
yesStates = map (renamePlace f) $ yesStates net,
noStates = map (renamePlace f) $ noStates net
} }
where mapAdjacency f g m = M.mapKeys f (M.map (mapContext g) m) where mapAdjacency f g m = M.mapKeys f (M.map (mapContext g) m)
mapContext f (pre, post) = mapContext f (pre, post) =
...@@ -157,8 +164,8 @@ renamePetriNetPlacesAndTransitions f net = ...@@ -157,8 +164,8 @@ renamePetriNetPlacesAndTransitions f net =
makePetriNet :: String -> [Place] -> [Transition] -> makePetriNet :: String -> [Place] -> [Transition] ->
[Either (Transition, Place, Integer) (Place, Transition, Integer)] -> [Either (Transition, Place, Integer) (Place, Transition, Integer)] ->
[(Place, Integer)] -> [Transition] -> [Trap] -> [Siphon] -> PetriNet [(Place, Integer)] -> [Transition] -> [Trap] -> [Siphon] -> [Place] -> [Place] -> PetriNet
makePetriNet name places transitions arcs initial gs fixedTraps fixedSiphons = makePetriNet name places transitions arcs initial gs fixedTraps fixedSiphons yesStates noStates =
PetriNet { PetriNet {
name = name, name = name,
places = listSet places, places = listSet places,
...@@ -168,7 +175,9 @@ makePetriNet name places transitions arcs initial gs fixedTraps fixedSiphons = ...@@ -168,7 +175,9 @@ makePetriNet name places transitions arcs initial gs fixedTraps fixedSiphons =
initialMarking = buildVector initial, initialMarking = buildVector initial,
ghostTransitions = listSet gs, ghostTransitions = listSet gs,
fixedTraps = map listSet fixedTraps, fixedTraps = map listSet fixedTraps,
fixedSiphons = map listSet fixedSiphons fixedSiphons = map listSet fixedSiphons,
yesStates = listSet yesStates,
noStates = listSet noStates
} }
where where
(adP, adT) = foldl buildMaps (M.empty, M.empty) arcs (adP, adT) = foldl buildMaps (M.empty, M.empty) arcs
...@@ -190,8 +199,8 @@ makePetriNet name places transitions arcs initial gs fixedTraps fixedSiphons = ...@@ -190,8 +199,8 @@ makePetriNet name places transitions arcs initial gs fixedTraps fixedSiphons =
makePetriNetFromStrings :: String -> [String] -> [String] -> makePetriNetFromStrings :: String -> [String] -> [String] ->
[(String, String, Integer)] -> [(String, String, Integer)] ->
[(String, Integer)] -> [String] -> [[String]] -> [[String]] -> PetriNet [(String, Integer)] -> [String] -> [[String]] -> [[String]] -> [String] -> [String] -> PetriNet
makePetriNetFromStrings name places transitions arcs initial gs fixedTraps fixedSiphons = makePetriNetFromStrings name places transitions arcs initial gs fixedTraps fixedSiphons yesStates noStates =
makePetriNet makePetriNet
name name
(map Place (S.toAscList placeSet)) (map Place (S.toAscList placeSet))
...@@ -201,6 +210,8 @@ makePetriNetFromStrings name places transitions arcs initial gs fixedTraps fixed ...@@ -201,6 +210,8 @@ makePetriNetFromStrings name places transitions arcs initial gs fixedTraps fixed
(map Transition gs) (map Transition gs)
(map (map Place) fixedTraps) (map (map Place) fixedTraps)
(map (map Place) fixedSiphons) (map (map Place) fixedSiphons)
(map Place yesStates)
(map Place noStates)
where where
placeSet = S.fromList places placeSet = S.fromList places
transitionSet = S.fromList transitions transitionSet = S.fromList transitions
...@@ -225,17 +236,17 @@ makePetriNetFromStrings name places transitions arcs initial gs fixedTraps fixed ...@@ -225,17 +236,17 @@ makePetriNetFromStrings name places transitions arcs initial gs fixedTraps fixed
makePetriNetWithTrans :: String -> [Place] -> makePetriNetWithTrans :: String -> [Place] ->
[(Transition, ([(Place, Integer)], [(Place, Integer)]))] -> [(Transition, ([(Place, Integer)], [(Place, Integer)]))] ->
[(Place, Integer)] -> [Transition] -> [Trap] -> [Siphon] ->PetriNet [(Place, Integer)] -> [Transition] -> [Trap] -> [Siphon] -> [Place] -> [Place] -> PetriNet
makePetriNetWithTrans name places ts fixedTraps fixedSiphons = makePetriNetWithTrans name places ts fixedTraps fixedSiphons yesStates noStates =
makePetriNet name places (map fst ts) arcs fixedTraps fixedSiphons makePetriNet name places (map fst ts) arcs fixedTraps fixedSiphons yesStates noStates
where where
arcs = [ Right (p,t,w) | (t,(is,_)) <- ts, (p,w) <- is ] ++ arcs = [ Right (p,t,w) | (t,(is,_)) <- ts, (p,w) <- is ] ++
[ Left (t,p,w) | (t,(_,os)) <- ts, (p,w) <- os ] [ Left (t,p,w) | (t,(_,os)) <- ts, (p,w) <- os ]
makePetriNetWithTransFromStrings :: String -> [String] -> makePetriNetWithTransFromStrings :: String -> [String] ->
[(String, ([(String, Integer)], [(String, Integer)]))] -> [(String, ([(String, Integer)], [(String, Integer)]))] ->
[(String, Integer)] -> [String] -> [[String]] -> [[String]] -> PetriNet [(String, Integer)] -> [String] -> [[String]] -> [[String]] -> [String] -> [String] -> PetriNet
makePetriNetWithTransFromStrings name places arcs initial gs fixedTraps fixedSiphons = makePetriNetWithTransFromStrings name places arcs initial gs fixedTraps fixedSiphons yesStates noStates =
makePetriNetWithTrans makePetriNetWithTrans
name name
(map Place places) (map Place places)
...@@ -244,6 +255,8 @@ makePetriNetWithTransFromStrings name places arcs initial gs fixedTraps fixedSip ...@@ -244,6 +255,8 @@ makePetriNetWithTransFromStrings name places arcs initial gs fixedTraps fixedSip
(map Transition gs) (map Transition gs)
(map (map Place) fixedTraps) (map (map Place) fixedTraps)
(map (map Place) fixedSiphons) (map (map Place) fixedSiphons)
(map Place yesStates)
(map Place noStates)
where where
toTArc (t, (is, os)) = toTArc (t, (is, os)) =
(Transition t, (map (first Place) is, map (first Place) os)) (Transition t, (map (first Place) is, map (first Place) os))
...@@ -93,9 +93,11 @@ data PropertyType = SafetyType ...@@ -93,9 +93,11 @@ data PropertyType = SafetyType
| ConstraintType | ConstraintType
data ConstraintProperty = UniqueTerminalMarkingConstraint data ConstraintProperty = UniqueTerminalMarkingConstraint
| NonConsensusStateConstraint
instance Show ConstraintProperty where instance Show ConstraintProperty where
show UniqueTerminalMarkingConstraint = "unique terminal marking" show UniqueTerminalMarkingConstraint = "unique terminal marking"
show NonConsensusStateConstraint = "non-consensus state"
data PropertyContent = Safety (Formula Place) data PropertyContent = Safety (Formula Place)
| Liveness (Formula Transition) | Liveness (Formula Transition)
......
{-# LANGUAGE FlexibleContexts #-}
module Solver.NonConsensusState
(checkNonConsensusStateSat,
NonConsensusStateCounterExample,
checkUnmarkedTrapSat,
checkUnmarkedSiphonSat)
where
import Data.SBV
import qualified Data.Map as M
import Data.List ((\\))
import Util
import PetriNet
import Property
import Solver
type NonConsensusStateCounterExample = (RMarking, RMarking, RFiringVector)
stateEquationConstraints :: PetriNet -> SRMap Place -> SRMap Place -> SRMap Transition -> SBool
stateEquationConstraints net m0 m x =
bAnd $ map checkStateEquation $ places net
where checkStateEquation p =
let incoming = map addTransition $ lpre net p
outgoing = map addTransition $ lpost net p
in val m0 p + sum incoming - sum outgoing .== val m p
addTransition (t,w) = literal (fromInteger w) * val x t
nonNegativityConstraints :: (Ord a, Show a) => SRMap a -> SBool
nonNegativityConstraints m =
bAnd $ map checkVal $ vals m
where checkVal x = x .>= 0
terminalMarkingConstraints :: PetriNet -> SRMap Place -> SBool
terminalMarkingConstraints net m =
bAnd $ map checkTransition $ transitions net
where checkTransition t = bOr $ map checkPlace $ lpre net t
checkPlace (p,w) = val m p .== 0
initialMarkingConstraints :: PetriNet -> SRMap Place -> SBool
initialMarkingConstraints net m0 =
sum (mval m0 (places net \\ initials net)) .== 0
nonConsensusStateConstraints :: PetriNet -> SRMap Place -> SBool
nonConsensusStateConstraints net m =
sum (mval m (yesStates net)) .> 0 &&&
sum (mval m (noStates net)) .> 0
checkTrap :: PetriNet -> SRMap Place -> SRMap Place -> SRMap Transition -> Trap -> SBool
checkTrap net m0 m x trap =
(markedByMarking m0 ==> markedByMarking m) &&&
(markedBySequence x ==> markedByMarking m)
where markedByMarking m = sum (mval m trap) .> 0
markedBySequence x = sum (mval x (mpre net trap)) .> 0
checkTrapConstraints :: PetriNet -> SRMap Place -> SRMap Place -> SRMap Transition -> [Trap] -> SBool
checkTrapConstraints net m0 m x traps =
bAnd $ map (checkTrap net m0 m x) traps
checkSiphon :: PetriNet -> SRMap Place -> SRMap Place -> SRMap Transition -> Siphon -> SBool
checkSiphon net m0 m x siphon =
unmarkedByMarking m0 ==> (unmarkedByMarking m &&& notPresetOfSequence x)
where unmarkedByMarking m = sum (mval m siphon) .== 0
notPresetOfSequence x = sum (mval x (mpost net siphon)) .== 0
checkSiphonConstraints :: PetriNet -> SRMap Place -> SRMap Place -> SRMap Transition -> [Siphon] -> SBool
checkSiphonConstraints net m0 m x siphons =
bAnd $ map (checkSiphon net m0 m x) siphons
checkNonConsensusState :: PetriNet -> SRMap Place -> SRMap Place -> SRMap Transition -> [Trap] -> [Siphon] -> SBool
checkNonConsensusState net m0 m x traps siphons =
stateEquationConstraints net m0 m x &&&
nonNegativityConstraints m0 &&&
nonNegativityConstraints m &&&
nonNegativityConstraints x &&&
initialMarkingConstraints net m0 &&&
terminalMarkingConstraints net m &&&
nonConsensusStateConstraints net m &&&
checkTrapConstraints net m0 m x traps &&&
checkSiphonConstraints net m0 m x siphons
checkNonConsensusStateSat :: PetriNet -> [Trap] -> [Siphon] -> ConstraintProblem AlgReal NonConsensusStateCounterExample
checkNonConsensusStateSat net traps siphons =
let m0 = makeVarMap $ places net
m = makeVarMapWith prime $ places net
x = makeVarMap $ transitions net
in ("non-consensus state", "(m0, m, x)",
getNames m0 ++ getNames m ++ getNames x,
\fm -> checkNonConsensusState net (fmap fm m0) (fmap fm m) (fmap fm x) traps siphons,
\fm -> markingsFromAssignment (fmap fm m0) (fmap fm m) (fmap fm x))
markingsFromAssignment :: RMap Place -> RMap Place -> RMap Transition -> NonConsensusStateCounterExample
markingsFromAssignment m0 m x =
(makeVector m0, makeVector m, makeVector x)
-- trap and siphon refinement constraints
siphonConstraints :: PetriNet -> SIMap Place -> SBool
siphonConstraints net b =
bAnd $ map siphonConstraint $ transitions net
where siphonConstraint t =
sum (mval b $ post net t) .> 0 ==> sum (mval b $ pre net t) .> 0
trapConstraints :: PetriNet -> SIMap Place -> SBool
trapConstraints net b =
bAnd $ map trapConstraint $ transitions net
where trapConstraint t =
sum (mval b $ pre net t) .> 0 ==> sum (mval b $ post net t) .> 0
placesMarkedByMarking :: PetriNet -> RMarking -> SIMap Place -> SBool
placesMarkedByMarking net m b = sum (mval b $ elems m) .> 0
placesUnmarkedByMarking :: PetriNet -> RMarking -> SIMap Place -> SBool
placesUnmarkedByMarking net m b = sum (mval b $ elems m) .== 0