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

Commit 5d587025 authored by Philipp J. Meyer's avatar Philipp J. Meyer
Browse files

Added trap refinement constraints to unique terminal marking constraints

parent 01e1cc92
......@@ -441,13 +441,43 @@ checkStructuralProperty net struct =
return Unsatisfied
checkConstraintProperty :: PetriNet -> ConstraintProperty -> OptIO PropResult
checkConstraintProperty net cp = do
let c = case cp of
UniqueTerminalMarkingConstraint -> checkUniqueTerminalMarkingSat
r <- checkSat $ c net
checkConstraintProperty net cp =
case cp of
UniqueTerminalMarkingConstraint -> checkUniqueTerminalMarkingProperty net
checkUniqueTerminalMarkingProperty :: PetriNet -> OptIO PropResult
checkUniqueTerminalMarkingProperty net = do
r <- checkUniqueTerminalMarkingProperty' net []
case r of
(Nothing, _) -> return Satisfied
(Just _, _) -> return Unknown
checkUniqueTerminalMarkingProperty' :: PetriNet ->
[Trap] -> OptIO (Maybe (Marking, Marking, Marking, FiringVector, FiringVector), [Trap])
checkUniqueTerminalMarkingProperty' net traps = do
r <- checkSat $ checkUniqueTerminalMarkingSat net traps
case r of
Nothing -> return Satisfied
Just _ -> return Unknown
Nothing -> return (Nothing, traps)
Just m -> do
refine <- opt optRefinementType
if isJust refine then
refineUniqueTerminalMarkingProperty net traps m
else
return (Just m, traps)
refineUniqueTerminalMarkingProperty :: PetriNet ->
[Trap] -> (Marking, Marking, Marking, FiringVector, FiringVector) -> OptIO (Maybe (Marking, Marking, Marking, FiringVector, FiringVector), [Trap])
refineUniqueTerminalMarkingProperty net traps m@(m0, m1, m2, x1, x2) = do
r1 <- checkSat $ checkUnmarkedTrapSat net m0 m1 x1
case r1 of
Nothing -> do
r2 <- checkSat $ checkUnmarkedTrapSat net m0 m2 x2
case r2 of
Nothing -> return (Just m, traps)
Just trap ->
checkUniqueTerminalMarkingProperty' net (trap:traps)
Just trap ->
checkUniqueTerminalMarkingProperty' net (trap:traps)
main :: IO ()
main = do
......
{-# LANGUAGE FlexibleContexts #-}
module Solver.UniqueTerminalMarking
(checkUniqueTerminalMarkingSat)
(checkUniqueTerminalMarkingSat,
checkUnmarkedTrapSat)
where
import Data.SBV
import qualified Data.Map as M
import Util
import PetriNet
......@@ -10,50 +14,111 @@ import Property
import Solver
stateEquationConstraints :: PetriNet -> SIMap Place -> SIMap Place -> SIMap Transition -> SBool
stateEquationConstraints net m1 m2 x =
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 m1 p + sum incoming - sum outgoing .== val m2 p
in val m0 p + sum incoming - sum outgoing .== val m p
addTransition (t,w) = literal w * val x t
nonNegativityConstraints :: PetriNet -> SIMap Place -> SBool
nonNegativityConstraints net m =
bAnd $ map checkVal $ places net
where checkVal p = val m p .>= 0
nonNegativityConstraints :: (Ord a, Show a) => SIMap a -> SBool
nonNegativityConstraints m =
bAnd $ map checkVal $ vals m
where checkVal x = x .>= 0
terminalConstraints :: PetriNet -> SIMap Place -> SBool
terminalConstraints net m =
bAnd $ map checkTransition $ transitions net
where checkTransition :: Transition -> SBool
checkTransition t = bOr $ map checkPlace $ lpre net t
where checkTransition t = bOr $ map checkPlace $ lpre net t
checkPlace (p,w) = val m p .< literal w
nonEqualityConstraints :: PetriNet -> SIMap Place -> SIMap Place -> SBool
nonEqualityConstraints :: (Ord a, Show a) => PetriNet -> SIMap a -> SIMap a -> SBool
nonEqualityConstraints net m1 m2 =
bOr $ map checkNonEquality $ places net
where checkNonEquality p = val m1 p ./= val m2 p
if elemsSet m1 /= elemsSet m2 then
false
else
bOr $ map checkNonEquality $ elems m1
where checkNonEquality x = val m1 x ./= val m2 x
checkTrap :: PetriNet -> SIMap Place -> SIMap Place -> SIMap Place -> SIMap Transition -> SIMap Transition -> Trap -> SBool
checkTrap net m0 m1 m2 x1 x2 trap =
checkMarkingDelta m0 m1 &&&
checkMarkingDelta m0 m2 &&&
checkSequenceDelta x1 m1 &&&
checkSequenceDelta x2 m2
where checkMarkingDelta m0 m =
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 net m0 m1 m2 x1 x2 traps =
bAnd $ map (checkTrap net m0 m1 m2 x1 x2) traps
checkUniqueTerminalMarking :: PetriNet -> SIMap Place -> SIMap Place -> SIMap Transition -> SBool
checkUniqueTerminalMarking net m1 m2 x =
checkUniqueTerminalMarking :: PetriNet -> SIMap Place -> SIMap Place -> SIMap Place -> SIMap Transition -> SIMap Transition -> [Trap] -> SBool
checkUniqueTerminalMarking net m0 m1 m2 x1 x2 traps =
nonEqualityConstraints net m1 m2 &&&
stateEquationConstraints net m1 m2 x &&&
nonNegativityConstraints net m1 &&&
nonNegativityConstraints net m2 &&&
stateEquationConstraints net m0 m1 x1 &&&
stateEquationConstraints net m0 m2 x2 &&&
nonNegativityConstraints m0 &&&
nonNegativityConstraints m1 &&&
nonNegativityConstraints m2 &&&
nonNegativityConstraints x1 &&&
nonNegativityConstraints x2 &&&
terminalConstraints net m1 &&&
terminalConstraints net m2
terminalConstraints net m2 &&&
checkTrapConstraints net m0 m1 m2 x1 x2 traps
checkUniqueTerminalMarkingSat :: PetriNet -> [Trap] -> ConstraintProblem Integer (Marking, Marking, Marking, FiringVector, FiringVector)
checkUniqueTerminalMarkingSat net traps =
let m0 = makeVarMap $ places net
m1 = makeVarMapWith prime $ places net
m2 = makeVarMapWith (prime . prime) $ places net
x1 = makeVarMap $ transitions net
x2 = makeVarMapWith prime $ transitions net
in ("unique terminal marking", "(m0, m1, m2, x1, 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 -> 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 m0 m1 m2 x1 x2 = (makeVector m0, makeVector m1, makeVector m2, makeVector x1, makeVector x2)
-- trap refinement constraints
trapConstraints :: PetriNet -> SBMap Place -> SBool
trapConstraints net b =
bAnd $ map trapConstraint $ transitions net
where trapConstraint t =
bOr (mval b (pre net t)) ==> bOr (mval b (post net t))
trapMarkedByMarking :: PetriNet -> Marking -> SBMap Place -> SBool
trapMarkedByMarking net m b = bOr $ mval b $ elems m
trapMarkedBySequence :: PetriNet -> FiringVector -> SBMap Place -> SBool
trapMarkedBySequence net x b = bOr $ mval b $ mpost net $ elems x
trapUnassigned :: Marking -> SBMap Place -> SBool
trapUnassigned m b = bAnd $ map (bnot . val b) $ elems m
properTrap :: SBMap Place -> SBool
properTrap b = bOr $ vals b
checkUniqueTerminalMarkingSat :: PetriNet -> ConstraintProblem Integer (Marking, Marking, FiringVector)
checkUniqueTerminalMarkingSat net =
let m1 = makeVarMap $ places net
m2 = makeVarMapWith prime $ places net
x = makeVarMap $ transitions net
in ("unique terminal marking", "pair of markings and firing vector",
getNames m1 ++ getNames m2 ++ getNames x,
\fm -> checkUniqueTerminalMarking net (fmap fm m1) (fmap fm m2) (fmap fm x),
\fm -> markingsFromAssignment (fmap fm m1) (fmap fm m2) (fmap fm x))
checkUnmarkedTrap :: PetriNet -> Marking -> Marking -> FiringVector -> SBMap Place -> SBool
checkUnmarkedTrap net m0 m x b =
trapConstraints net b &&&
(trapMarkedByMarking net m0 b ||| trapMarkedBySequence net x b) &&&
trapUnassigned m b &&&
properTrap b
markingsFromAssignment :: IMap Place -> IMap Place -> IMap Transition -> (Marking, Marking, FiringVector)
markingsFromAssignment m1 m2 x = (makeVector m1, makeVector m2, makeVector x)
checkUnmarkedTrapSat :: PetriNet -> Marking -> Marking -> FiringVector -> ConstraintProblem Bool Trap
checkUnmarkedTrapSat net m0 m x =
let b = makeVarMap $ places net
in ("unmarked trap marked by sequence or initial marking", "trap",
getNames b,
\fm -> checkUnmarkedTrap net m0 m x (fmap fm b),
\fm -> trapFromAssignment (fmap fm b))
trapFromAssignment :: BMap Place -> Trap
trapFromAssignment b = M.keys $ M.filter id b
{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, FunctionalDependencies #-}
module Util
(elems,items,size,emap,prime,numPref,
(elems,elemsSet,items,size,emap,prime,numPref,
listSet,listMap,val,vals,mval,zeroVal,positiveVal,sumVal,
makeVarMap,makeVarMapWith,buildVector,makeVector,getNames,
Vector,Model,VarMap,SIMap,SBMap,IMap,BMap,showWeighted,
......@@ -10,6 +10,7 @@ where
import Data.SBV
import qualified Data.Map as M
import qualified Data.Set as S
import Data.List
import Data.Ord
import Data.Function
......@@ -36,6 +37,7 @@ class MapLike c a b | c -> a, c -> b where
val :: c -> a -> b
vals :: c -> [b]
elems :: c -> [a]
elemsSet :: c -> S.Set a
items :: c -> [(a,b)]
size :: c -> Int
......@@ -51,6 +53,7 @@ instance (Ord a, Show a, Show b) => MapLike (M.Map a b) a b where
vals = M.elems
items = M.toList
elems = M.keys
elemsSet = M.keysSet
size = M.size
instance (Ord a, Show a) => MapLike (Vector a) a Integer where
......@@ -58,6 +61,7 @@ instance (Ord a, Show a) => MapLike (Vector a) a Integer where
vals = vals . getVector
items = M.toList . getVector
elems = M.keys . getVector
elemsSet = M.keysSet . getVector
size = M.size . getVector
instance (Show a) => Show (Vector a) where
......
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