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

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

Added constraint checking over the reals

parent 4518c194
......@@ -454,7 +454,7 @@ checkUniqueTerminalMarkingProperty net = do
checkUniqueTerminalMarkingProperty' :: PetriNet ->
[Trap] -> [Siphon] ->
OptIO (Maybe (Marking, Marking, Marking, FiringVector, FiringVector), [Trap], [Siphon])
OptIO (Maybe UniqueTerminalMarkingCounterExample, [Trap], [Siphon])
checkUniqueTerminalMarkingProperty' net traps siphons = do
r <- checkSat $ checkUniqueTerminalMarkingSat net traps siphons
case r of
......@@ -467,8 +467,8 @@ checkUniqueTerminalMarkingProperty' net traps siphons = do
return (Just m, traps, siphons)
refineUniqueTerminalMarkingProperty :: PetriNet ->
[Trap] -> [Siphon] -> (Marking, Marking, Marking, FiringVector, FiringVector) ->
OptIO (Maybe (Marking, Marking, Marking, FiringVector, FiringVector), [Trap], [Siphon])
[Trap] -> [Siphon] -> UniqueTerminalMarkingCounterExample ->
OptIO (Maybe UniqueTerminalMarkingCounterExample, [Trap], [Siphon])
refineUniqueTerminalMarkingProperty net traps siphons m@(m0, m1, m2, x1, x2) = do
r1 <- checkSat $ checkUnmarkedTrapSat net m0 m1 m2 x1 x2
case r1 of
......
......@@ -3,6 +3,7 @@
module PetriNet
(PetriNet,Place(..),Transition(..),Marking,FiringVector,
RMarking,RFiringVector,
renamePlace,renameTransition,renamePetriNetPlacesAndTransitions,
name,showNetName,places,transitions,
initialMarking,initial,initials,linitials,
......@@ -57,8 +58,11 @@ instance Nodes Place Transition where
instance Nodes Transition Place where
contextMap = adjacencyT
type Marking = Vector Place
type FiringVector = Vector Transition
type Marking = IVector Place
type FiringVector = IVector Transition
type RMarking = RVector Place
type RFiringVector = RVector Transition
type Trap = [Place]
type Siphon = [Place]
......
......@@ -18,7 +18,7 @@ import Property
import PetriNet
data LivenessInvariant =
RankingFunction (SimpleCut, Vector Place)
RankingFunction (SimpleCut, IVector Place)
| ComponentCut (SimpleCut, [Trap]) -- TODO: add proof why
instance Invariant LivenessInvariant where
......
......@@ -16,7 +16,7 @@ import Solver
import Property
import PetriNet
type SimpleTerm = (Vector Place, Integer)
type SimpleTerm = (IVector Place, Integer)
type NamedTerm = (String, SimpleTerm)
data SafetyInvariant =
......
......@@ -2,6 +2,7 @@
module Solver.UniqueTerminalMarking
(checkUniqueTerminalMarkingSat,
UniqueTerminalMarkingCounterExample,
checkUnmarkedTrapSat,
checkUnmarkedSiphonSat)
where
......@@ -14,27 +15,29 @@ import PetriNet
import Property
import Solver
stateEquationConstraints :: PetriNet -> SIMap Place -> SIMap Place -> SIMap Transition -> SBool
type UniqueTerminalMarkingCounterExample = (RMarking, RMarking, RMarking, RFiringVector, 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 w * val x t
addTransition (t,w) = literal (fromInteger w) * val x t
nonNegativityConstraints :: (Ord a, Show a) => SIMap a -> SBool
nonNegativityConstraints :: (Ord a, Show a) => SRMap a -> SBool
nonNegativityConstraints m =
bAnd $ map checkVal $ vals m
where checkVal x = x .>= 0
terminalConstraints :: PetriNet -> SIMap Place -> SBool
terminalConstraints :: PetriNet -> SRMap Place -> SBool
terminalConstraints net m =
bAnd $ map checkTransition $ transitions net
where checkTransition t = bOr $ map checkPlace $ lpre net t
checkPlace (p,w) = val m p .< literal w
checkPlace (p,w) = val m p .== 0
nonEqualityConstraints :: (Ord a, Show a) => PetriNet -> SIMap a -> SIMap a -> SBool
nonEqualityConstraints :: (Ord a, Show a) => PetriNet -> SRMap a -> SRMap a -> SBool
nonEqualityConstraints net m1 m2 =
if elemsSet m1 /= elemsSet m2 then
false
......@@ -42,29 +45,29 @@ nonEqualityConstraints net m1 m2 =
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 :: PetriNet -> SRMap Place -> SRMap Place -> SRMap Place -> SRMap Transition -> SRMap Transition -> Trap -> SBool
checkTrap net m0 m1 m2 x1 x2 trap =
(markedByMarking m0 ==> (markedByMarking m1 &&& markedByMarking m2)) &&&
(markedBySequence x1 ==> markedByMarking m1) &&&
(markedBySequence x2 ==> markedByMarking m2)
where markedByMarking m = sum (map (val m) trap) .>= 1
markedBySequence x = sum (map (val x) (mpre net trap)) .>= 1
where markedByMarking m = sum (map (val m) trap) .> 0
markedBySequence x = sum (map (val x) (mpre net trap)) .> 0
checkTrapConstraints :: PetriNet -> SIMap Place -> SIMap Place -> SIMap Place -> SIMap Transition -> SIMap Transition -> [Trap] -> SBool
checkTrapConstraints :: PetriNet -> SRMap Place -> SRMap Place -> SRMap Place -> SRMap Transition -> SRMap Transition -> [Trap] -> SBool
checkTrapConstraints net m0 m1 m2 x1 x2 traps =
bAnd $ map (checkTrap net m0 m1 m2 x1 x2) traps
checkSiphon :: PetriNet -> SIMap Place -> SIMap Place -> SIMap Place -> SIMap Transition -> SIMap Transition -> Siphon -> SBool
checkSiphon :: PetriNet -> SRMap Place -> SRMap Place -> SRMap Place -> SRMap Transition -> SRMap Transition -> Siphon -> SBool
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 :: PetriNet -> SRMap Place -> SRMap Place -> SRMap Place -> SRMap Transition -> SRMap 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 ->
checkUniqueTerminalMarking :: PetriNet -> SRMap Place -> SRMap Place -> SRMap Place -> SRMap Transition -> SRMap Transition ->
[Trap] -> [Siphon] -> SBool
checkUniqueTerminalMarking net m0 m1 m2 x1 x2 traps siphons =
nonEqualityConstraints net m1 m2 &&&
......@@ -80,7 +83,7 @@ checkUniqueTerminalMarking net m0 m1 m2 x1 x2 traps siphons =
checkTrapConstraints net m0 m1 m2 x1 x2 traps &&&
checkSiphonConstraints net m0 m1 m2 x1 x2 siphons
checkUniqueTerminalMarkingSat :: PetriNet -> [Trap] -> [Siphon] -> ConstraintProblem Integer (Marking, Marking, Marking, FiringVector, FiringVector)
checkUniqueTerminalMarkingSat :: PetriNet -> [Trap] -> [Siphon] -> ConstraintProblem AlgReal UniqueTerminalMarkingCounterExample
checkUniqueTerminalMarkingSat net traps siphons =
let m0 = makeVarMap $ places net
m1 = makeVarMapWith prime $ places net
......@@ -92,8 +95,9 @@ checkUniqueTerminalMarkingSat net traps siphons =
\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))
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 :: RMap Place -> RMap Place -> RMap Place -> RMap Transition -> RMap Transition -> UniqueTerminalMarkingCounterExample
markingsFromAssignment m0 m1 m2 x1 x2 =
(makeVector m0, makeVector m1, makeVector m2, makeVector x1, makeVector x2)
-- trap and siphon refinement constraints
......@@ -109,22 +113,22 @@ trapConstraints net b =
where trapConstraint t =
bOr (mval b (pre net t)) ==> bOr (mval b (post net t))
placesMarkedByMarking :: PetriNet -> Marking -> SBMap Place -> SBool
placesMarkedByMarking :: PetriNet -> RMarking -> SBMap Place -> SBool
placesMarkedByMarking net m b = bOr $ mval b $ elems m
placesUnmarkedByMarking :: PetriNet -> Marking -> SBMap Place -> SBool
placesUnmarkedByMarking :: PetriNet -> RMarking -> SBMap Place -> SBool
placesUnmarkedByMarking net m b = bAnd $ map (bnot . val b) $ elems m
placesPostsetOfSequence :: PetriNet -> FiringVector -> SBMap Place -> SBool
placesPostsetOfSequence :: PetriNet -> RFiringVector -> SBMap Place -> SBool
placesPostsetOfSequence net x b = bOr $ mval b $ mpost net $ elems x
placesPresetOfSequence :: PetriNet -> FiringVector -> SBMap Place -> SBool
placesPresetOfSequence :: PetriNet -> RFiringVector -> SBMap Place -> SBool
placesPresetOfSequence net x b = bOr $ mval b $ mpre net $ elems x
nonemptySet :: (Ord a, Show a) => SBMap a -> SBool
nonemptySet b = bOr $ vals b
checkUnmarkedTrap :: PetriNet -> Marking -> Marking -> Marking -> FiringVector -> FiringVector -> SBMap Place -> SBool
checkUnmarkedTrap :: PetriNet -> RMarking -> RMarking -> RMarking -> RFiringVector -> RFiringVector -> SBMap Place -> SBool
checkUnmarkedTrap net m0 m1 m2 x1 x2 b =
trapConstraints net b &&&
nonemptySet b &&&
......@@ -134,7 +138,7 @@ checkUnmarkedTrap net m0 m1 m2 x1 x2 b =
(placesPostsetOfSequence net x2 b &&& placesUnmarkedByMarking net m2 b)
)
checkUnmarkedTrapSat :: PetriNet -> Marking -> Marking -> Marking -> FiringVector -> FiringVector -> ConstraintProblem Bool Siphon
checkUnmarkedTrapSat :: PetriNet -> RMarking -> RMarking -> RMarking -> RFiringVector -> RFiringVector -> ConstraintProblem Bool Trap
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",
......@@ -142,7 +146,7 @@ checkUnmarkedTrapSat net m0 m1 m2 x1 x2 =
\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 :: PetriNet -> RMarking -> RMarking -> RMarking -> RFiringVector -> RFiringVector -> SBMap Place -> SBool
checkUnmarkedSiphon net m0 m1 m2 x1 x2 b =
siphonConstraints net b &&&
nonemptySet b &&&
......@@ -151,7 +155,7 @@ checkUnmarkedSiphon net m0 m1 m2 x1 x2 b =
placesPresetOfSequence net x1 b ||| placesPresetOfSequence net x2 b)
)
checkUnmarkedSiphonSat :: PetriNet -> Marking -> Marking -> Marking -> FiringVector -> FiringVector -> ConstraintProblem Bool Siphon
checkUnmarkedSiphonSat :: PetriNet -> RMarking -> RMarking -> RMarking -> RFiringVector -> RFiringVector -> ConstraintProblem Bool Siphon
checkUnmarkedSiphonSat net m0 m1 m2 x1 x2 =
let b = makeVarMap $ places net
in ("siphon unmarked in m0 and marked in m1 or m2 or used as input in x1 or x2", "siphon",
......
......@@ -4,7 +4,7 @@ module Util
(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,
Vector,IVector,RVector,Model,VarMap,SIMap,SRMap,SBMap,IMap,RMap,BMap,showWeighted,
OptIO,verbosePut,opt,putLine,parallelIO)
where
......@@ -25,12 +25,16 @@ import Options
- Various maps and functions on them
-}
newtype Vector a = Vector { getVector :: M.Map a Integer }
newtype Vector a b = Vector { getVector :: M.Map a b }
type IVector a = Vector a Integer
type RVector a = Vector a AlgReal
type Model a = M.Map String a
type VarMap a = M.Map a String
type SIMap a = M.Map a SInteger
type SRMap a = M.Map a SReal
type SBMap a = M.Map a SBool
type IMap a = M.Map a Integer
type RMap a = M.Map a AlgReal
type BMap a = M.Map a Bool
class MapLike c a b | c -> a, c -> b where
......@@ -56,7 +60,7 @@ instance (Ord a, Show a, Show b) => MapLike (M.Map a b) a b where
elemsSet = M.keysSet
size = M.size
instance (Ord a, Show a) => MapLike (Vector a) a Integer where
instance (Ord a, Show a, Num b, Show b) => MapLike (Vector a b) a b where
val (Vector v) x = M.findWithDefault 0 x v
vals = vals . getVector
items = M.toList . getVector
......@@ -64,13 +68,13 @@ instance (Ord a, Show a) => MapLike (Vector a) a Integer where
elemsSet = M.keysSet . getVector
size = M.size . getVector
instance (Show a) => Show (Vector a) where
instance (Show a, Show b, Num b, Eq b) => Show (Vector a b) where
show (Vector v) =
"[" ++ intercalate "," (map showEntry (M.toList v)) ++ "]"
where showEntry (i,x) =
show i ++ (if x /= 1 then "(" ++ show x ++ ")" else "")
emap :: (Ord a, Ord b) => (a -> b) -> Vector a -> Vector b
emap :: (Ord a, Ord b) => (a -> b) -> Vector a c -> Vector b c
emap f = Vector . M.mapKeys f . getVector
zeroVal :: (Ord a, Show a) => M.Map a SInteger -> a -> SBool
......@@ -88,10 +92,10 @@ makeVarMapWith f xs = M.fromList $ xs `zip` map (f . show) xs
getNames :: VarMap a -> [String]
getNames = M.elems
buildVector :: (Ord a) => [(a, Integer)] -> Vector a
buildVector :: (Ord a, Num b, Eq b) => [(a, b)] -> Vector a b
buildVector = makeVector . M.fromList
makeVector :: (Ord a) => M.Map a Integer -> Vector a
makeVector :: (Ord a, Num b, Eq b) => M.Map a b -> Vector a b
makeVector = Vector . M.filter (/=0)
{-
......
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