Commit f800ee96 authored by Philipp J. Meyer's avatar Philipp J. Meyer

removed obsolete flag for non-consensus terminal markings

parent 384039ae
......@@ -39,7 +39,6 @@ import Solver.SComponentWithCut
import Solver.SComponent
import Solver.Simplifier
import Solver.TerminalMarkingsUniqueConsensus
import Solver.NonConsensusTerminalMarking
import Solver.TerminalMarkingReachable
--import Solver.Interpolant
--import Solver.CommFreeReachability
......@@ -220,8 +219,6 @@ makeImplicitProperty _ StructCommunicationFree =
Property "communication free" $ Structural CommunicationFree
makeImplicitProperty _ TerminalMarkingsUniqueConsensus =
Property "reachable terminal markings have a unique consensus" $ Constraint TerminalMarkingsUniqueConsensusConstraint
makeImplicitProperty _ NonConsensusTerminalMarking =
Property "no non-consensus terminal marking reachable" $ Constraint NonConsensusTerminalMarkingConstraint
makeImplicitProperty _ TerminalMarkingReachable =
Property "terminal marking reachable" $ Constraint TerminalMarkingReachableConstraint
......@@ -451,7 +448,6 @@ checkConstraintProperty :: PetriNet -> ConstraintProperty -> OptIO PropResult
checkConstraintProperty net cp =
case cp of
TerminalMarkingsUniqueConsensusConstraint -> checkTerminalMarkingsUniqueConsensusProperty net
NonConsensusTerminalMarkingConstraint -> checkNonConsensusTerminalMarkingProperty net
TerminalMarkingReachableConstraint -> checkTerminalMarkingReachableProperty net
checkTerminalMarkingsUniqueConsensusProperty :: PetriNet -> OptIO PropResult
......@@ -491,43 +487,6 @@ refineTerminalMarkingsUniqueConsensusProperty net traps siphons c@(m0, m1, m2, x
Just trap ->
checkTerminalMarkingsUniqueConsensusProperty' net (trap:traps) siphons
checkNonConsensusTerminalMarkingProperty :: PetriNet -> OptIO PropResult
checkNonConsensusTerminalMarkingProperty net = do
r <- checkNonConsensusTerminalMarkingProperty' net (fixedTraps net) (fixedSiphons net)
case r of
(Nothing, _, _) -> return Satisfied
(Just _, _, _) -> return Unknown
checkNonConsensusTerminalMarkingProperty' :: PetriNet ->
[Trap] -> [Siphon] ->
OptIO (Maybe NonConsensusTerminalMarkingCounterExample, [Trap], [Siphon])
checkNonConsensusTerminalMarkingProperty' net traps siphons = do
r <- checkSat $ checkNonConsensusTerminalMarkingSat net traps siphons
case r of
Nothing -> return (Nothing, traps, siphons)
Just c -> do
refine <- opt optRefinementType
if isJust refine then
refineNonConsensusTerminalMarkingProperty net traps siphons c
else
return (Just c, traps, siphons)
refineNonConsensusTerminalMarkingProperty :: PetriNet ->
[Trap] -> [Siphon] -> NonConsensusTerminalMarkingCounterExample ->
OptIO (Maybe NonConsensusTerminalMarkingCounterExample, [Trap], [Siphon])
refineNonConsensusTerminalMarkingProperty net traps siphons c@(m0, m, x) = do
r1 <- checkSatMin $ Solver.NonConsensusTerminalMarking.checkUnmarkedTrapSat net m0 m x
case r1 of
Nothing -> do
r2 <- checkSatMin $ Solver.NonConsensusTerminalMarking.checkUnmarkedSiphonSat net m0 m x
case r2 of
Nothing ->
return (Just c, traps, siphons)
Just siphon ->
checkNonConsensusTerminalMarkingProperty' net traps (siphon:siphons)
Just trap ->
checkNonConsensusTerminalMarkingProperty' net (trap:traps) siphons
checkTerminalMarkingReachableProperty :: PetriNet -> OptIO PropResult
checkTerminalMarkingReachableProperty net = do
let nonTrivialTriplets = filter (not . trivialTriplet) $ generateTriplets net
......
......@@ -32,7 +32,6 @@ data ImplicitProperty = Termination
| StructFinalPlace
| StructCommunicationFree
| TerminalMarkingsUniqueConsensus
| NonConsensusTerminalMarking
| TerminalMarkingReachable
deriving (Show,Read)
......@@ -186,12 +185,6 @@ options =
}))
"Prove that terminal markings have a unique consensus"
, Option "" ["non-consensus-terminal-marking"]
(NoArg (\opt -> Right opt {
optProperties = NonConsensusTerminalMarking : optProperties opt
}))
"Prove that no non-consensus terminal marking is reachable from an initial marking"
, Option "" ["terminal-marking-reachable"]
(NoArg (\opt -> Right opt {
optProperties = TerminalMarkingReachable : optProperties opt
......
......@@ -93,12 +93,10 @@ data PropertyType = SafetyType
| ConstraintType
data ConstraintProperty = TerminalMarkingsUniqueConsensusConstraint
| NonConsensusTerminalMarkingConstraint
| TerminalMarkingReachableConstraint
instance Show ConstraintProperty where
show TerminalMarkingsUniqueConsensusConstraint = "reachable terminal markings have a unique consensus"
show NonConsensusTerminalMarkingConstraint = "no non-consensus terminal marking reachable"
show TerminalMarkingReachableConstraint = "terminal marking reachable"
data PropertyContent = Safety (Formula Place)
......
{-# LANGUAGE FlexibleContexts #-}
module Solver.NonConsensusTerminalMarking
(checkNonConsensusTerminalMarkingSat,
NonConsensusTerminalMarkingCounterExample,
checkUnmarkedTrapSat,
checkUnmarkedSiphonSat)
where
import Data.SBV
import qualified Data.Map as M
import Data.List ((\\))
import Util
import PetriNet
import Property
import Solver
type NonConsensusTerminalMarkingCounterExample = (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
checkNonConsensusTerminalMarking :: PetriNet -> SRMap Place -> SRMap Place -> SRMap Transition -> [Trap] -> [Siphon] -> SBool
checkNonConsensusTerminalMarking 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
checkNonConsensusTerminalMarkingSat :: PetriNet -> [Trap] -> [Siphon] -> ConstraintProblem AlgReal NonConsensusTerminalMarkingCounterExample
checkNonConsensusTerminalMarkingSat 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 -> checkNonConsensusTerminalMarking 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 -> NonConsensusTerminalMarkingCounterExample
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
placesPostsetOfSequence :: PetriNet -> RFiringVector -> SIMap Place -> SBool
placesPostsetOfSequence net x b = sum (mval b $ mpost net $ elems x) .> 0
placesPresetOfSequence :: PetriNet -> RFiringVector -> SIMap Place -> SBool
placesPresetOfSequence net x b = sum (mval b $ mpre net $ elems x) .> 0
nonemptySet :: (Ord a, Show a) => SIMap a -> SBool
nonemptySet b = sum (vals b) .> 0
checkBinary :: SIMap Place -> SBool
checkBinary = bAnd . map (\x -> x .== 0 ||| x .== 1) . vals
checkSizeLimit :: SIMap Place -> Maybe (Int, Integer) -> SBool
checkSizeLimit _ Nothing = true
checkSizeLimit b (Just (1, curSize)) = (.< literal curSize) $ sumVal b
checkSizeLimit b (Just (2, curSize)) = (.> literal curSize) $ sumVal b
checkSizeLimit _ (Just (_, _)) = error "minimization method not supported"
minimizeMethod :: Int -> Integer -> String
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 -> RFiringVector -> SIMap Place -> Maybe (Int, Integer) -> SBool
checkUnmarkedTrap net m0 m x b sizeLimit =
trapConstraints net b &&&
nonemptySet b &&&
checkSizeLimit b sizeLimit &&&
checkBinary b &&&
(
(placesMarkedByMarking net m0 b &&& placesUnmarkedByMarking net m b) |||
(placesPostsetOfSequence net x b &&& placesUnmarkedByMarking net m b)
)
checkUnmarkedTrapSat :: PetriNet -> RMarking -> RMarking -> RFiringVector -> MinConstraintProblem Integer Trap Integer
checkUnmarkedTrapSat net m0 m x =
let b = makeVarMap $ places net
in (minimizeMethod, \sizeLimit ->
("trap marked in m and unmarked in m, or marked by x and unmarked in m", "trap",
getNames b,
\fm -> checkUnmarkedTrap net m0 m x (fmap fm b) sizeLimit,
\fm -> placesFromAssignment (fmap fm b)))
checkUnmarkedSiphon :: PetriNet -> RMarking -> RMarking -> RFiringVector -> SIMap Place -> Maybe (Int, Integer) -> SBool
checkUnmarkedSiphon net m0 m x b sizeLimit =
siphonConstraints net b &&&
nonemptySet b &&&
checkSizeLimit b sizeLimit &&&
checkBinary b &&&
(placesUnmarkedByMarking net m0 b &&& (placesMarkedByMarking net m b ||| placesPresetOfSequence net x b))
checkUnmarkedSiphonSat :: PetriNet -> RMarking -> RMarking -> RFiringVector -> MinConstraintProblem Integer Siphon Integer
checkUnmarkedSiphonSat net m0 m x =
let b = makeVarMap $ places net
in (minimizeMethod, \sizeLimit ->
("siphon unmarked in m0 and marked in m or used as input in x", "siphon",
getNames b,
\fm -> checkUnmarkedSiphon net m0 m x (fmap fm b) sizeLimit,
\fm -> placesFromAssignment (fmap fm b)))
placesFromAssignment :: IMap Place -> ([Place], Integer)
placesFromAssignment b = (M.keys (M.filter (> 0) b), sum (M.elems b))
......@@ -15,6 +15,8 @@ import Property
import Solver
import StructuralComputation
type InvariantSize = ([Int], [Integer], [Int])
type TerminalMarkingReachableInvariant = [BlockInvariant]
data BlockInvariant =
BlockInvariant (Integer, [Transition], IVector Place)
......@@ -59,7 +61,7 @@ blockOrderConstraints net triplets k b =
bAnd $ map checkTriplet triplets
where checkTriplet (s,t,ts) = (val b s .> val b t) ==> bOr (map (\t' -> val b t' .== val b t) ts)
checkTerminalMarkingReachable :: PetriNet -> [Triplet] -> Integer -> SIMap Transition -> [SIMap Place] -> Maybe (Int, (Int, [Int])) -> SBool
checkTerminalMarkingReachable :: PetriNet -> [Triplet] -> Integer -> SIMap Transition -> [SIMap Place] -> Maybe (Int, InvariantSize) -> SBool
checkTerminalMarkingReachable net triplets k b ys sizeLimit =
blockConstraints net k b &&&
terminationConstraints net k b ys &&&
......@@ -67,7 +69,7 @@ checkTerminalMarkingReachable net triplets k b ys sizeLimit =
checkNonNegativityConstraints ys &&&
checkSizeLimit k b ys sizeLimit
checkTerminalMarkingReachableSat :: PetriNet -> [Triplet] -> Integer -> MinConstraintProblem Integer TerminalMarkingReachableInvariant (Int, [Int])
checkTerminalMarkingReachableSat :: PetriNet -> [Triplet] -> Integer -> MinConstraintProblem Integer TerminalMarkingReachableInvariant InvariantSize
checkTerminalMarkingReachableSat net triplets k =
let makeYName i = (++) (genericReplicate i '\'')
ys = [makeVarMapWith (makeYName i) $ places net | i <- [1..k]]
......@@ -78,25 +80,46 @@ checkTerminalMarkingReachableSat net triplets k =
\fm -> checkTerminalMarkingReachable net triplets k (fmap fm b) (map (fmap fm) ys) sizeLimit,
\fm -> invariantFromAssignment net k (fmap fm b) (map (fmap fm) ys)))
minimizeMethod :: Int -> (Int, [Int]) -> String
minimizeMethod 1 (curYSize, _) = "number of places in y less than " ++ show curYSize
minimizeMethod 2 (_, curTSize) = "number of transitions in last block less than " ++ show (last curTSize)
minimizeMethod 3 (curYSize, curTSize) = "number of transitions in last block less than " ++ show (last curTSize) ++
minimizeMethod :: Int -> InvariantSize -> String
minimizeMethod 1 (curYSize, _, _) = "number of places in y less than " ++ show (sum curYSize)
minimizeMethod 2 (_, _, curTSize) = "number of transitions in last block less than " ++ show (last curTSize)
minimizeMethod 3 (curYSize, _, curTSize) = "number of transitions in last block less than " ++ show (last curTSize) ++
" or same number of transitions and number of places in y less than " ++ show curYSize
minimizeMethod 4 (_, curYMax, _) = "maximum coefficient in y is less than " ++ show (maximum curYMax)
minimizeMethod 5 (curYSize, curYMax, _) = "number of places in y less than " ++ show (sum curYSize) ++
" or same number of places and maximum coefficient in y is less than " ++ show (maximum curYMax)
minimizeMethod 6 (curYSize, curYMax, curTSize) = "number of transitions in last block less than " ++ show (last curTSize) ++
" or same number of transitions and number of places in y less than " ++ show (sum curYSize) ++
" or same number of transitions and same number of places and maximum coefficient in y less than " ++ show (maximum curYMax)
minimizeMethod _ _ = error "minimization method not supported"
checkSizeLimit :: Integer -> SIMap Transition -> [SIMap Place] -> Maybe (Int, (Int, [Int])) -> SBool
checkSizeLimit :: Integer -> SIMap Transition -> [SIMap Place] -> Maybe (Int, InvariantSize) -> SBool
checkSizeLimit _ _ _ Nothing = true
checkSizeLimit k b ys (Just (1, (curYSize, _))) = (sum (map (\y -> sum (map (\yi -> ite (yi .> 0) (1::SInteger) 0) (vals y))) ys) .< literal (fromIntegral curYSize))
checkSizeLimit k b ys (Just (2, (_, curTSize))) = (sum (map (\tb -> ite (tb .== (literal k)) (1::SInteger) 0) (vals b))) .< literal (fromIntegral (last curTSize))
checkSizeLimit k b ys (Just (3, (curYSize, curTSize))) =
checkSizeLimit k b ys (Just (1, (curYSize, _, _))) = (sum (map (\y -> sum (map (\yi -> ite (yi .> 0) (1::SInteger) 0) (vals y))) ys) .< literal (fromIntegral (sum curYSize)))
checkSizeLimit k b ys (Just (2, (_, _, curTSize))) = (sum (map (\tb -> ite (tb .== (literal k)) (1::SInteger) 0) (vals b))) .< literal (fromIntegral (last curTSize))
checkSizeLimit k b ys (Just (3, (curYSize, _, curTSize))) =
((sum (map (\tb -> ite (tb .== (literal k)) (1::SInteger) 0) (vals b))) .< literal (fromIntegral (last curTSize))) ||| (
((sum (map (\tb -> ite (tb .== (literal k)) (1::SInteger) 0) (vals b))) .== literal (fromIntegral (last curTSize))) &&&
(sum (map (\y -> sum (map (\yi -> ite (yi .> 0) (1::SInteger) 0) (vals y))) ys) .< literal (fromIntegral curYSize))
(sum (map (\y -> sum (map (\yi -> ite (yi .> 0) (1::SInteger) 0) (vals y))) ys) .< literal (fromIntegral (sum curYSize)))
)
checkSizeLimit k b ys (Just (4, (_, curYMax, _))) = ((foldl smax 0 (concatMap vals ys)) .< literal (fromIntegral (maximum curYMax)))
checkSizeLimit k b ys (Just (5, (curYSize, curYMax, _))) =
(sum (map (\y -> sum (map (\yi -> ite (yi .> 0) (1::SInteger) 0) (vals y))) ys) .< literal (fromIntegral (sum curYSize))) ||| (
(sum (map (\y -> sum (map (\yi -> ite (yi .> 0) (1::SInteger) 0) (vals y))) ys) .== literal (fromIntegral (sum curYSize))) &&&
((foldl smax 0 (concatMap vals ys)) .< literal (fromIntegral (maximum curYMax))))
checkSizeLimit k b ys (Just (6, (curYSize, curYMax, curTSize))) =
((sum (map (\tb -> ite (tb .== (literal k)) (1::SInteger) 0) (vals b))) .< literal (fromIntegral (last curTSize))) ||| (
((sum (map (\tb -> ite (tb .== (literal k)) (1::SInteger) 0) (vals b))) .== literal (fromIntegral (last curTSize))) &&&
((sum (map (\y -> sum (map (\yi -> ite (yi .> 0) (1::SInteger) 0) (vals y))) ys) .< literal (fromIntegral (sum curYSize))) ||| (
(sum (map (\y -> sum (map (\yi -> ite (yi .> 0) (1::SInteger) 0) (vals y))) ys) .== literal (fromIntegral (sum curYSize))) &&&
((foldl smax 0 (concatMap vals ys)) .< literal (fromIntegral (maximum curYMax))))))
checkSizeLimit _ _ _ (Just (_, _)) = error "minimization method not supported"
invariantFromAssignment :: PetriNet -> Integer -> IMap Transition -> [IMap Place] -> (TerminalMarkingReachableInvariant, (Int, [Int]))
invariantFromAssignment :: PetriNet -> Integer -> IMap Transition -> [IMap Place] -> (TerminalMarkingReachableInvariant, InvariantSize)
invariantFromAssignment net k b ys =
let invariant = [BlockInvariant (i, M.keys (M.filter (== i) b), makeVector y) | (i,y) <- zip [1..] ys]
in (invariant, (sum $ map invariantSize invariant, map (\(BlockInvariant (_, ts, _)) -> length ts) invariant))
(invariant, (map invariantLength invariant, map invariantMaxCoefficient invariant, map blockSize invariant))
where
invariant = [BlockInvariant (i, M.keys (M.filter (== i) b), makeVector y) | (i,y) <- zip [1..] ys]
invariantMaxCoefficient (BlockInvariant (_, _, yi)) = maximum $ vals yi
invariantLength (BlockInvariant (_, _, yi)) = size yi
blockSize (BlockInvariant (_, ti, _)) = length ti
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