Commit 4518c194 authored by Philipp J. Meyer's avatar Philipp J. Meyer
Browse files

Added refinement with siphons

parent 5d587025
...@@ -447,37 +447,40 @@ checkConstraintProperty net cp = ...@@ -447,37 +447,40 @@ checkConstraintProperty net cp =
checkUniqueTerminalMarkingProperty :: PetriNet -> OptIO PropResult checkUniqueTerminalMarkingProperty :: PetriNet -> OptIO PropResult
checkUniqueTerminalMarkingProperty net = do checkUniqueTerminalMarkingProperty net = do
r <- checkUniqueTerminalMarkingProperty' net [] r <- checkUniqueTerminalMarkingProperty' net [] []
case r of case r of
(Nothing, _) -> return Satisfied (Nothing, _, _) -> return Satisfied
(Just _, _) -> return Unknown (Just _, _, _) -> return Unknown
checkUniqueTerminalMarkingProperty' :: PetriNet -> checkUniqueTerminalMarkingProperty' :: PetriNet ->
[Trap] -> OptIO (Maybe (Marking, Marking, Marking, FiringVector, FiringVector), [Trap]) [Trap] -> [Siphon] ->
checkUniqueTerminalMarkingProperty' net traps = do OptIO (Maybe (Marking, Marking, Marking, FiringVector, FiringVector), [Trap], [Siphon])
r <- checkSat $ checkUniqueTerminalMarkingSat net traps checkUniqueTerminalMarkingProperty' net traps siphons = do
r <- checkSat $ checkUniqueTerminalMarkingSat net traps siphons
case r of case r of
Nothing -> return (Nothing, traps) Nothing -> return (Nothing, traps, siphons)
Just m -> do Just m -> do
refine <- opt optRefinementType refine <- opt optRefinementType
if isJust refine then if isJust refine then
refineUniqueTerminalMarkingProperty net traps m refineUniqueTerminalMarkingProperty net traps siphons m
else else
return (Just m, traps) return (Just m, traps, siphons)
refineUniqueTerminalMarkingProperty :: PetriNet -> refineUniqueTerminalMarkingProperty :: PetriNet ->
[Trap] -> (Marking, Marking, Marking, FiringVector, FiringVector) -> OptIO (Maybe (Marking, Marking, Marking, FiringVector, FiringVector), [Trap]) [Trap] -> [Siphon] -> (Marking, Marking, Marking, FiringVector, FiringVector) ->
refineUniqueTerminalMarkingProperty net traps m@(m0, m1, m2, x1, x2) = do OptIO (Maybe (Marking, Marking, Marking, FiringVector, FiringVector), [Trap], [Siphon])
r1 <- checkSat $ checkUnmarkedTrapSat net m0 m1 x1 refineUniqueTerminalMarkingProperty net traps siphons m@(m0, m1, m2, x1, x2) = do
r1 <- checkSat $ checkUnmarkedTrapSat net m0 m1 m2 x1 x2
case r1 of case r1 of
Nothing -> do Nothing -> do
r2 <- checkSat $ checkUnmarkedTrapSat net m0 m2 x2 r2 <- checkSat $ checkUnmarkedSiphonSat net m0 m1 m2 x1 x2
case r2 of case r2 of
Nothing -> return (Just m, traps) Nothing ->
Just trap -> return (Just m, traps, siphons)
checkUniqueTerminalMarkingProperty' net (trap:traps) Just siphon ->
checkUniqueTerminalMarkingProperty' net traps (siphon:siphons)
Just trap -> Just trap ->
checkUniqueTerminalMarkingProperty' net (trap:traps) checkUniqueTerminalMarkingProperty' net (trap:traps) siphons
main :: IO () main :: IO ()
main = do main = do
......
...@@ -8,7 +8,7 @@ module PetriNet ...@@ -8,7 +8,7 @@ module PetriNet
initialMarking,initial,initials,linitials, initialMarking,initial,initials,linitials,
pre,lpre,post,lpost,mpre,mpost,context,ghostTransitions, pre,lpre,post,lpost,mpre,mpost,context,ghostTransitions,
makePetriNet,makePetriNetWithTrans, makePetriNet,makePetriNetWithTrans,
makePetriNetFromStrings,makePetriNetWithTransFromStrings,Trap,Cut, makePetriNetFromStrings,makePetriNetWithTransFromStrings,Trap,Siphon,Cut,
constructCut,SimpleCut,Invariant(..)) constructCut,SimpleCut,Invariant(..))
where where
...@@ -61,6 +61,7 @@ type Marking = Vector Place ...@@ -61,6 +61,7 @@ type Marking = Vector Place
type FiringVector = Vector Transition type FiringVector = Vector Transition
type Trap = [Place] type Trap = [Place]
type Siphon = [Place]
-- TODO: generalize cut type -- TODO: generalize cut type
type Cut = ([([Place], [Transition])], [Transition]) type Cut = ([([Place], [Transition])], [Transition])
......
...@@ -2,7 +2,8 @@ ...@@ -2,7 +2,8 @@
module Solver.UniqueTerminalMarking module Solver.UniqueTerminalMarking
(checkUniqueTerminalMarkingSat, (checkUniqueTerminalMarkingSat,
checkUnmarkedTrapSat) checkUnmarkedTrapSat,
checkUnmarkedSiphonSat)
where where
import Data.SBV import Data.SBV
...@@ -43,21 +44,29 @@ nonEqualityConstraints net m1 m2 = ...@@ -43,21 +44,29 @@ nonEqualityConstraints net m1 m2 =
checkTrap :: PetriNet -> SIMap Place -> SIMap Place -> SIMap Place -> SIMap Transition -> SIMap Transition -> Trap -> SBool checkTrap :: PetriNet -> SIMap Place -> SIMap Place -> SIMap Place -> SIMap Transition -> SIMap Transition -> Trap -> SBool
checkTrap net m0 m1 m2 x1 x2 trap = checkTrap net m0 m1 m2 x1 x2 trap =
checkMarkingDelta m0 m1 &&& (markedByMarking m0 ==> (markedByMarking m1 &&& markedByMarking m2)) &&&
checkMarkingDelta m0 m2 &&& (markedBySequence x1 ==> markedByMarking m1) &&&
checkSequenceDelta x1 m1 &&& (markedBySequence x2 ==> markedByMarking m2)
checkSequenceDelta x2 m2 where markedByMarking m = sum (map (val m) trap) .>= 1
where checkMarkingDelta m0 m = markedBySequence x = sum (map (val x) (mpre net trap)) .>= 1
sum (map (val m0) trap) .>= 1 ==> sum (map (val m) trap) .>= 1
checkSequenceDelta x m =
sum (map (val x) (mpre net trap)) .>= 1 ==> sum (map (val m) trap) .>= 1
checkTrapConstraints :: PetriNet -> SIMap Place -> SIMap Place -> SIMap Place -> SIMap Transition -> SIMap Transition -> [Trap] -> SBool checkTrapConstraints :: PetriNet -> SIMap Place -> SIMap Place -> SIMap Place -> SIMap Transition -> SIMap Transition -> [Trap] -> SBool
checkTrapConstraints net m0 m1 m2 x1 x2 traps = checkTrapConstraints net m0 m1 m2 x1 x2 traps =
bAnd $ map (checkTrap net m0 m1 m2 x1 x2) traps bAnd $ map (checkTrap net m0 m1 m2 x1 x2) traps
checkUniqueTerminalMarking :: PetriNet -> SIMap Place -> SIMap Place -> SIMap Place -> SIMap Transition -> SIMap Transition -> [Trap] -> SBool checkSiphon :: PetriNet -> SIMap Place -> SIMap Place -> SIMap Place -> SIMap Transition -> SIMap Transition -> Siphon -> SBool
checkUniqueTerminalMarking net m0 m1 m2 x1 x2 traps = checkSiphon net m0 m1 m2 x1 x2 siphon =
unmarkedByMarking m0 ==> (unmarkedByMarking m1 &&& unmarkedByMarking m2 &&& notPresetOfSequence x1 &&& notPresetOfSequence x2)
where unmarkedByMarking m = sum (map (val m) siphon) .== 0
notPresetOfSequence x = sum (map (val x) (mpost net siphon)) .== 0
checkSiphonConstraints :: PetriNet -> SIMap Place -> SIMap Place -> SIMap Place -> SIMap Transition -> SIMap Transition -> [Siphon] -> SBool
checkSiphonConstraints net m0 m1 m2 x1 x2 siphons =
bAnd $ map (checkSiphon net m0 m1 m2 x1 x2) siphons
checkUniqueTerminalMarking :: PetriNet -> SIMap Place -> SIMap Place -> SIMap Place -> SIMap Transition -> SIMap Transition ->
[Trap] -> [Siphon] -> SBool
checkUniqueTerminalMarking net m0 m1 m2 x1 x2 traps siphons =
nonEqualityConstraints net m1 m2 &&& nonEqualityConstraints net m1 m2 &&&
stateEquationConstraints net m0 m1 x1 &&& stateEquationConstraints net m0 m1 x1 &&&
stateEquationConstraints net m0 m2 x2 &&& stateEquationConstraints net m0 m2 x2 &&&
...@@ -68,10 +77,11 @@ checkUniqueTerminalMarking net m0 m1 m2 x1 x2 traps = ...@@ -68,10 +77,11 @@ checkUniqueTerminalMarking net m0 m1 m2 x1 x2 traps =
nonNegativityConstraints x2 &&& nonNegativityConstraints x2 &&&
terminalConstraints net m1 &&& terminalConstraints net m1 &&&
terminalConstraints net m2 &&& terminalConstraints net m2 &&&
checkTrapConstraints net m0 m1 m2 x1 x2 traps checkTrapConstraints net m0 m1 m2 x1 x2 traps &&&
checkSiphonConstraints net m0 m1 m2 x1 x2 siphons
checkUniqueTerminalMarkingSat :: PetriNet -> [Trap] -> ConstraintProblem Integer (Marking, Marking, Marking, FiringVector, FiringVector) checkUniqueTerminalMarkingSat :: PetriNet -> [Trap] -> [Siphon] -> ConstraintProblem Integer (Marking, Marking, Marking, FiringVector, FiringVector)
checkUniqueTerminalMarkingSat net traps = checkUniqueTerminalMarkingSat net traps siphons =
let m0 = makeVarMap $ places net let m0 = makeVarMap $ places net
m1 = makeVarMapWith prime $ places net m1 = makeVarMapWith prime $ places net
m2 = makeVarMapWith (prime . prime) $ places net m2 = makeVarMapWith (prime . prime) $ places net
...@@ -79,13 +89,19 @@ checkUniqueTerminalMarkingSat net traps = ...@@ -79,13 +89,19 @@ checkUniqueTerminalMarkingSat net traps =
x2 = makeVarMapWith prime $ transitions net x2 = makeVarMapWith prime $ transitions net
in ("unique terminal marking", "(m0, m1, m2, x1, x2)", in ("unique terminal marking", "(m0, m1, m2, x1, x2)",
getNames m0 ++ getNames m1 ++ getNames m2 ++ getNames x1 ++ getNames x2, getNames m0 ++ getNames m1 ++ getNames m2 ++ getNames x1 ++ getNames x2,
\fm -> checkUniqueTerminalMarking net (fmap fm m0) (fmap fm m1) (fmap fm m2) (fmap fm x1) (fmap fm x2) traps, \fm -> checkUniqueTerminalMarking net (fmap fm m0) (fmap fm m1) (fmap fm m2) (fmap fm x1) (fmap fm x2) traps siphons,
\fm -> markingsFromAssignment (fmap fm m0) (fmap fm m1) (fmap fm m2) (fmap fm x1) (fmap fm x2)) \fm -> markingsFromAssignment (fmap fm m0) (fmap fm m1) (fmap fm m2) (fmap fm x1) (fmap fm x2))
markingsFromAssignment :: IMap Place -> IMap Place -> IMap Place -> IMap Transition -> IMap Transition -> (Marking, Marking, Marking, FiringVector, FiringVector) markingsFromAssignment :: IMap Place -> IMap Place -> IMap Place -> IMap Transition -> IMap Transition -> (Marking, Marking, Marking, FiringVector, FiringVector)
markingsFromAssignment m0 m1 m2 x1 x2 = (makeVector m0, makeVector m1, makeVector m2, makeVector x1, makeVector x2) markingsFromAssignment m0 m1 m2 x1 x2 = (makeVector m0, makeVector m1, makeVector m2, makeVector x1, makeVector x2)
-- trap refinement constraints -- trap and siphon refinement constraints
siphonConstraints :: PetriNet -> SBMap Place -> SBool
siphonConstraints net b =
bAnd $ map siphonConstraint $ transitions net
where siphonConstraint t =
bOr (mval b (post net t)) ==> bOr (mval b (pre net t))
trapConstraints :: PetriNet -> SBMap Place -> SBool trapConstraints :: PetriNet -> SBMap Place -> SBool
trapConstraints net b = trapConstraints net b =
...@@ -93,32 +109,55 @@ trapConstraints net b = ...@@ -93,32 +109,55 @@ trapConstraints net b =
where trapConstraint t = where trapConstraint t =
bOr (mval b (pre net t)) ==> bOr (mval b (post net t)) bOr (mval b (pre net t)) ==> bOr (mval b (post net t))
trapMarkedByMarking :: PetriNet -> Marking -> SBMap Place -> SBool placesMarkedByMarking :: PetriNet -> Marking -> SBMap Place -> SBool
trapMarkedByMarking net m b = bOr $ mval b $ elems m placesMarkedByMarking net m b = bOr $ mval b $ elems m
trapMarkedBySequence :: PetriNet -> FiringVector -> SBMap Place -> SBool placesUnmarkedByMarking :: PetriNet -> Marking -> SBMap Place -> SBool
trapMarkedBySequence net x b = bOr $ mval b $ mpost net $ elems x placesUnmarkedByMarking net m b = bAnd $ map (bnot . val b) $ elems m
trapUnassigned :: Marking -> SBMap Place -> SBool placesPostsetOfSequence :: PetriNet -> FiringVector -> SBMap Place -> SBool
trapUnassigned m b = bAnd $ map (bnot . val b) $ elems m placesPostsetOfSequence net x b = bOr $ mval b $ mpost net $ elems x
properTrap :: SBMap Place -> SBool placesPresetOfSequence :: PetriNet -> FiringVector -> SBMap Place -> SBool
properTrap b = bOr $ vals b placesPresetOfSequence net x b = bOr $ mval b $ mpre net $ elems x
checkUnmarkedTrap :: PetriNet -> Marking -> Marking -> FiringVector -> SBMap Place -> SBool nonemptySet :: (Ord a, Show a) => SBMap a -> SBool
checkUnmarkedTrap net m0 m x b = nonemptySet b = bOr $ vals b
trapConstraints net b &&&
(trapMarkedByMarking net m0 b ||| trapMarkedBySequence net x b) &&&
trapUnassigned m b &&&
properTrap b
checkUnmarkedTrapSat :: PetriNet -> Marking -> Marking -> FiringVector -> ConstraintProblem Bool Trap checkUnmarkedTrap :: PetriNet -> Marking -> Marking -> Marking -> FiringVector -> FiringVector -> SBMap Place -> SBool
checkUnmarkedTrapSat net m0 m x = checkUnmarkedTrap net m0 m1 m2 x1 x2 b =
trapConstraints net b &&&
nonemptySet b &&&
(
(placesMarkedByMarking net m0 b &&& (placesUnmarkedByMarking net m1 b ||| placesUnmarkedByMarking net m2 b)) |||
(placesPostsetOfSequence net x1 b &&& placesUnmarkedByMarking net m1 b) |||
(placesPostsetOfSequence net x2 b &&& placesUnmarkedByMarking net m2 b)
)
checkUnmarkedTrapSat :: PetriNet -> Marking -> Marking -> Marking -> FiringVector -> FiringVector -> ConstraintProblem Bool Siphon
checkUnmarkedTrapSat net m0 m1 m2 x1 x2 =
let b = makeVarMap $ places net
in ("trap marked in m and unmarked in m1 or m2, or marked by x1 and unmarked in m1, or marked by x2 and unmarked in m2", "trap",
getNames b,
\fm -> checkUnmarkedTrap net m0 m1 m2 x1 x2 (fmap fm b),
\fm -> placesFromAssignment (fmap fm b))
checkUnmarkedSiphon :: PetriNet -> Marking -> Marking -> Marking -> FiringVector -> FiringVector -> SBMap Place -> SBool
checkUnmarkedSiphon net m0 m1 m2 x1 x2 b =
siphonConstraints net b &&&
nonemptySet b &&&
(placesUnmarkedByMarking net m0 b &&&
(placesMarkedByMarking net m1 b ||| placesMarkedByMarking net m2 b |||
placesPresetOfSequence net x1 b ||| placesPresetOfSequence net x2 b)
)
checkUnmarkedSiphonSat :: PetriNet -> Marking -> Marking -> Marking -> FiringVector -> FiringVector -> ConstraintProblem Bool Siphon
checkUnmarkedSiphonSat net m0 m1 m2 x1 x2 =
let b = makeVarMap $ places net let b = makeVarMap $ places net
in ("unmarked trap marked by sequence or initial marking", "trap", in ("siphon unmarked in m0 and marked in m1 or m2 or used as input in x1 or x2", "siphon",
getNames b, getNames b,
\fm -> checkUnmarkedTrap net m0 m x (fmap fm b), \fm -> checkUnmarkedSiphon net m0 m1 m2 x1 x2 (fmap fm b),
\fm -> trapFromAssignment (fmap fm b)) \fm -> placesFromAssignment (fmap fm b))
trapFromAssignment :: BMap Place -> Trap placesFromAssignment :: BMap Place -> Trap
trapFromAssignment b = M.keys $ M.filter id b placesFromAssignment b = M.keys $ M.filter id b
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment