Commit 813ebf78 authored by Philipp J. Meyer's avatar Philipp J. Meyer

renamed property for reachability of non-consensus terminal marking

parent 94cbefa8
......@@ -39,7 +39,7 @@ import Solver.SComponentWithCut
import Solver.SComponent
import Solver.Simplifier
import Solver.TerminalMarkingsUniqueConsensus
import Solver.NonConsensusState
import Solver.NonConsensusTerminalMarking
import Solver.TerminalMarkingReachable
--import Solver.Interpolant
--import Solver.CommFreeReachability
......@@ -219,9 +219,9 @@ makeImplicitProperty _ StructFinalPlace =
makeImplicitProperty _ StructCommunicationFree =
Property "communication free" $ Structural CommunicationFree
makeImplicitProperty _ TerminalMarkingsUniqueConsensus =
Property "terminal markings have a unique consensus" $ Constraint TerminalMarkingsUniqueConsensusConstraint
makeImplicitProperty _ NonConsensusState =
Property "non-consensus state" $ Constraint NonConsensusStateConstraint
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 +451,7 @@ checkConstraintProperty :: PetriNet -> ConstraintProperty -> OptIO PropResult
checkConstraintProperty net cp =
case cp of
TerminalMarkingsUniqueConsensusConstraint -> checkTerminalMarkingsUniqueConsensusProperty net
NonConsensusStateConstraint -> checkNonConsensusStateProperty net
NonConsensusTerminalMarkingConstraint -> checkNonConsensusTerminalMarkingProperty net
TerminalMarkingReachableConstraint -> checkTerminalMarkingReachableProperty net
checkTerminalMarkingsUniqueConsensusProperty :: PetriNet -> OptIO PropResult
......@@ -491,42 +491,42 @@ refineTerminalMarkingsUniqueConsensusProperty net traps siphons c@(m0, m1, m2, x
Just trap ->
checkTerminalMarkingsUniqueConsensusProperty' net (trap:traps) siphons
checkNonConsensusStateProperty :: PetriNet -> OptIO PropResult
checkNonConsensusStateProperty net = do
r <- checkNonConsensusStateProperty' net (fixedTraps net) (fixedSiphons net)
checkNonConsensusTerminalMarkingProperty :: PetriNet -> OptIO PropResult
checkNonConsensusTerminalMarkingProperty net = do
r <- checkNonConsensusTerminalMarkingProperty' net (fixedTraps net) (fixedSiphons net)
case r of
(Nothing, _, _) -> return Satisfied
(Just _, _, _) -> return Unknown
checkNonConsensusStateProperty' :: PetriNet ->
checkNonConsensusTerminalMarkingProperty' :: PetriNet ->
[Trap] -> [Siphon] ->
OptIO (Maybe NonConsensusStateCounterExample, [Trap], [Siphon])
checkNonConsensusStateProperty' net traps siphons = do
r <- checkSat $ checkNonConsensusStateSat net traps siphons
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
refineNonConsensusStateProperty net traps siphons c
refineNonConsensusTerminalMarkingProperty net traps siphons c
else
return (Just c, traps, siphons)
refineNonConsensusStateProperty :: PetriNet ->
[Trap] -> [Siphon] -> NonConsensusStateCounterExample ->
OptIO (Maybe NonConsensusStateCounterExample, [Trap], [Siphon])
refineNonConsensusStateProperty net traps siphons c@(m0, m, x) = do
r1 <- checkSatMin $ Solver.NonConsensusState.checkUnmarkedTrapSat net m0 m x
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.NonConsensusState.checkUnmarkedSiphonSat net m0 m x
r2 <- checkSatMin $ Solver.NonConsensusTerminalMarking.checkUnmarkedSiphonSat net m0 m x
case r2 of
Nothing ->
return (Just c, traps, siphons)
Just siphon ->
checkNonConsensusStateProperty' net traps (siphon:siphons)
checkNonConsensusTerminalMarkingProperty' net traps (siphon:siphons)
Just trap ->
checkNonConsensusStateProperty' net (trap:traps) siphons
checkNonConsensusTerminalMarkingProperty' net (trap:traps) siphons
checkTerminalMarkingReachableProperty :: PetriNet -> OptIO PropResult
checkTerminalMarkingReachableProperty net = do
......
......@@ -32,7 +32,7 @@ data ImplicitProperty = Termination
| StructFinalPlace
| StructCommunicationFree
| TerminalMarkingsUniqueConsensus
| NonConsensusState
| NonConsensusTerminalMarking
| TerminalMarkingReachable
deriving (Show,Read)
......@@ -186,11 +186,11 @@ options =
}))
"Prove that terminal markings have a unique consensus"
, Option "" ["non-consensus-state"]
, Option "" ["non-consensus-terminal-marking"]
(NoArg (\opt -> Right opt {
optProperties = NonConsensusState : optProperties opt
optProperties = NonConsensusTerminalMarking : optProperties opt
}))
"Prove that no non-consensus terminal state is reachable from an initial marking"
"Prove that no non-consensus terminal marking is reachable from an initial marking"
, Option "" ["terminal-marking-reachable"]
(NoArg (\opt -> Right opt {
......
......@@ -93,12 +93,12 @@ data PropertyType = SafetyType
| ConstraintType
data ConstraintProperty = TerminalMarkingsUniqueConsensusConstraint
| NonConsensusStateConstraint
| NonConsensusTerminalMarkingConstraint
| TerminalMarkingReachableConstraint
instance Show ConstraintProperty where
show TerminalMarkingsUniqueConsensusConstraint = "terminal markings have a unique consensus"
show NonConsensusStateConstraint = "non-consensus state"
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.NonConsensusState
(checkNonConsensusStateSat,
NonConsensusStateCounterExample,
module Solver.NonConsensusTerminalMarking
(checkNonConsensusTerminalMarkingSat,
NonConsensusTerminalMarkingCounterExample,
checkUnmarkedTrapSat,
checkUnmarkedSiphonSat)
where
......@@ -16,7 +16,7 @@ import PetriNet
import Property
import Solver
type NonConsensusStateCounterExample = (RMarking, RMarking, RFiringVector)
type NonConsensusTerminalMarkingCounterExample = (RMarking, RMarking, RFiringVector)
stateEquationConstraints :: PetriNet -> SRMap Place -> SRMap Place -> SRMap Transition -> SBool
stateEquationConstraints net m0 m x =
......@@ -68,8 +68,8 @@ checkSiphonConstraints :: PetriNet -> SRMap Place -> SRMap Place -> SRMap Transi
checkSiphonConstraints net m0 m x siphons =
bAnd $ map (checkSiphon net m0 m x) siphons
checkNonConsensusState :: PetriNet -> SRMap Place -> SRMap Place -> SRMap Transition -> [Trap] -> [Siphon] -> SBool
checkNonConsensusState net m0 m x traps 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 &&&
......@@ -80,17 +80,17 @@ checkNonConsensusState net m0 m x traps siphons =
checkTrapConstraints net m0 m x traps &&&
checkSiphonConstraints net m0 m x siphons
checkNonConsensusStateSat :: PetriNet -> [Trap] -> [Siphon] -> ConstraintProblem AlgReal NonConsensusStateCounterExample
checkNonConsensusStateSat net traps 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 -> checkNonConsensusState net (fmap fm m0) (fmap fm m) (fmap fm x) traps siphons,
\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 -> NonConsensusStateCounterExample
markingsFromAssignment :: RMap Place -> RMap Place -> RMap Transition -> NonConsensusTerminalMarkingCounterExample
markingsFromAssignment m0 m x =
(makeVector m0, makeVector m, makeVector x)
......
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