Commit 1a59eb94 by Philipp J. Meyer

### updated unique terminal marking constraints

parent 6e12e50e
 ... ... @@ -15,9 +15,9 @@ import PetriNet import Property import Solver type UniqueTerminalMarkingCounterExample = (RMarking, RMarking, RMarking, RFiringVector, RFiringVector) type UniqueTerminalMarkingCounterExample = (Marking, Marking, Marking, FiringVector, FiringVector) stateEquationConstraints :: PetriNet -> SRMap Place -> SRMap Place -> SRMap Transition -> SBool stateEquationConstraints :: PetriNet -> SIMap Place -> SIMap Place -> SIMap Transition -> SBool stateEquationConstraints net m0 m x = bAnd \$ map checkStateEquation \$ places net where checkStateEquation p = ... ... @@ -26,18 +26,18 @@ stateEquationConstraints net m0 m x = 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 :: (Ord a, Show a) => SIMap a -> SBool nonNegativityConstraints m = bAnd \$ map checkVal \$ vals m where checkVal x = x .>= 0 terminalConstraints :: PetriNet -> SRMap Place -> SBool terminalConstraints :: PetriNet -> SIMap 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 .== 0 checkPlace (p,w) = val m p .<= literal (fromInteger (w - 1)) nonEqualityConstraints :: (Ord a, Show a) => PetriNet -> SRMap a -> SRMap a -> SBool nonEqualityConstraints :: (Ord a, Show a) => PetriNet -> SIMap a -> SIMap a -> SBool nonEqualityConstraints net m1 m2 = if elemsSet m1 /= elemsSet m2 then false ... ... @@ -45,7 +45,7 @@ nonEqualityConstraints net m1 m2 = bOr \$ map checkNonEquality \$ elems m1 where checkNonEquality x = val m1 x ./= val m2 x checkTrap :: PetriNet -> SRMap Place -> SRMap Place -> SRMap Place -> SRMap Transition -> SRMap 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 = (markedByMarking m0 ==> (markedByMarking m1 &&& markedByMarking m2)) &&& (markedBySequence x1 ==> markedByMarking m1) &&& ... ... @@ -53,21 +53,21 @@ checkTrap net m0 m1 m2 x1 x2 trap = where markedByMarking m = sum (mval m trap) .> 0 markedBySequence x = sum (mval x (mpre net trap)) .> 0 checkTrapConstraints :: PetriNet -> SRMap Place -> SRMap Place -> SRMap Place -> SRMap Transition -> SRMap 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 = bAnd \$ map (checkTrap net m0 m1 m2 x1 x2) traps checkSiphon :: PetriNet -> SRMap Place -> SRMap Place -> SRMap Place -> SRMap Transition -> SRMap Transition -> Siphon -> SBool checkSiphon :: PetriNet -> SIMap Place -> SIMap Place -> SIMap Place -> SIMap Transition -> SIMap 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 (mval m siphon) .== 0 notPresetOfSequence x = sum (mval x (mpost net siphon)) .== 0 checkSiphonConstraints :: PetriNet -> SRMap Place -> SRMap Place -> SRMap Place -> SRMap Transition -> SRMap Transition -> [Siphon] -> SBool 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 -> SRMap Place -> SRMap Place -> SRMap Place -> SRMap Transition -> SRMap Transition -> 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 &&& ... ... @@ -83,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 AlgReal UniqueTerminalMarkingCounterExample checkUniqueTerminalMarkingSat :: PetriNet -> [Trap] -> [Siphon] -> ConstraintProblem Integer UniqueTerminalMarkingCounterExample checkUniqueTerminalMarkingSat net traps siphons = let m0 = makeVarMap \$ places net m1 = makeVarMapWith prime \$ places net ... ... @@ -95,7 +95,7 @@ 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 :: RMap Place -> RMap Place -> RMap Place -> RMap Transition -> RMap Transition -> UniqueTerminalMarkingCounterExample markingsFromAssignment :: IMap Place -> IMap Place -> IMap Place -> IMap Transition -> IMap Transition -> UniqueTerminalMarkingCounterExample markingsFromAssignment m0 m1 m2 x1 x2 = (makeVector m0, makeVector m1, makeVector m2, makeVector x1, makeVector x2) ... ... @@ -113,16 +113,16 @@ trapConstraints net b = where trapConstraint t = sum (mval b \$ pre net t) .> 0 ==> sum (mval b \$ post net t) .> 0 placesMarkedByMarking :: PetriNet -> RMarking -> SIMap Place -> SBool placesMarkedByMarking :: PetriNet -> Marking -> SIMap Place -> SBool placesMarkedByMarking net m b = sum (mval b \$ elems m) .> 0 placesUnmarkedByMarking :: PetriNet -> RMarking -> SIMap Place -> SBool placesUnmarkedByMarking :: PetriNet -> Marking -> SIMap Place -> SBool placesUnmarkedByMarking net m b = sum (mval b \$ elems m) .== 0 placesPostsetOfSequence :: PetriNet -> RFiringVector -> SIMap Place -> SBool placesPostsetOfSequence :: PetriNet -> FiringVector -> SIMap Place -> SBool placesPostsetOfSequence net x b = sum (mval b \$ mpost net \$ elems x) .> 0 placesPresetOfSequence :: PetriNet -> RFiringVector -> SIMap Place -> SBool placesPresetOfSequence :: PetriNet -> FiringVector -> SIMap Place -> SBool placesPresetOfSequence net x b = sum (mval b \$ mpre net \$ elems x) .> 0 nonemptySet :: (Ord a, Show a) => SIMap a -> SBool ... ... @@ -142,7 +142,7 @@ minimizeMethod 1 curSize = "size smaller than " ++ show curSize minimizeMethod 2 curSize = "size larger than " ++ show curSize minimizeMethod _ _ = error "minimization method not supported" checkUnmarkedTrap :: PetriNet -> RMarking -> RMarking -> RMarking -> RFiringVector -> RFiringVector -> SIMap Place -> Maybe (Int, Integer) -> SBool checkUnmarkedTrap :: PetriNet -> Marking -> Marking -> Marking -> FiringVector -> FiringVector -> SIMap Place -> Maybe (Int, Integer) -> SBool checkUnmarkedTrap net m0 m1 m2 x1 x2 b sizeLimit = trapConstraints net b &&& nonemptySet b &&& ... ... @@ -154,7 +154,7 @@ checkUnmarkedTrap net m0 m1 m2 x1 x2 b sizeLimit = (placesPostsetOfSequence net x2 b &&& placesUnmarkedByMarking net m2 b) ) checkUnmarkedTrapSat :: PetriNet -> RMarking -> RMarking -> RMarking -> RFiringVector -> RFiringVector -> MinConstraintProblem Integer Trap Integer checkUnmarkedTrapSat :: PetriNet -> Marking -> Marking -> Marking -> FiringVector -> FiringVector -> MinConstraintProblem Integer Trap Integer checkUnmarkedTrapSat net m0 m1 m2 x1 x2 = let b = makeVarMap \$ places net in (minimizeMethod, \sizeLimit -> ... ... @@ -163,7 +163,7 @@ checkUnmarkedTrapSat net m0 m1 m2 x1 x2 = \fm -> checkUnmarkedTrap net m0 m1 m2 x1 x2 (fmap fm b) sizeLimit, \fm -> placesFromAssignment (fmap fm b))) checkUnmarkedSiphon :: PetriNet -> RMarking -> RMarking -> RMarking -> RFiringVector -> RFiringVector -> SIMap Place -> Maybe (Int, Integer) -> SBool checkUnmarkedSiphon :: PetriNet -> Marking -> Marking -> Marking -> FiringVector -> FiringVector -> SIMap Place -> Maybe (Int, Integer) -> SBool checkUnmarkedSiphon net m0 m1 m2 x1 x2 b sizeLimit = siphonConstraints net b &&& nonemptySet b &&& ... ... @@ -174,7 +174,7 @@ checkUnmarkedSiphon net m0 m1 m2 x1 x2 b sizeLimit = placesPresetOfSequence net x1 b ||| placesPresetOfSequence net x2 b) ) checkUnmarkedSiphonSat :: PetriNet -> RMarking -> RMarking -> RMarking -> RFiringVector -> RFiringVector -> MinConstraintProblem Integer Siphon Integer checkUnmarkedSiphonSat :: PetriNet -> Marking -> Marking -> Marking -> FiringVector -> FiringVector -> MinConstraintProblem Integer Siphon Integer checkUnmarkedSiphonSat net m0 m1 m2 x1 x2 = let b = makeVarMap \$ places net in (minimizeMethod, \sizeLimit -> ... ...
Supports Markdown
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