Commit 6546c613 authored by Philipp Meyer's avatar Philipp Meyer

Rename marking to configuration; simplify invariant

parent c9113b43
......@@ -82,23 +82,13 @@ checkProperty pp prop = do
verbosePut 0 $ show prop ++ " " ++ show r
return r
printInvariant :: (Show a, Invariant a) => (Maybe [a], [a]) -> OptIO PropResult
printInvariant (baseInvResult, addedInv) =
case baseInvResult of
Nothing -> do
verbosePut 0 "No invariant found"
return Unknown
Just baseInv -> do
verbosePut 0 "Invariant found"
let baseSize = map invariantSize baseInv
let addedSize = map invariantSize addedInv
verbosePut 2 $ "Number of atoms in base invariants: " ++ show baseSize ++
" (total of " ++ show (sum baseSize) ++ ")"
verbosePut 2 $ "Number of atoms in added invariants: " ++ show addedSize ++
" (total of " ++ show (sum addedSize) ++ ")"
mapM_ (putLine . show) baseInv
mapM_ (putLine . show) addedInv
return Satisfied
printInvariant :: (Show a, Invariant a) => [a] -> OptIO ()
printInvariant inv = do
verbosePut 0 "Invariant found"
let invSize = map invariantSize inv
verbosePut 2 $ "Number of atoms in invariants: " ++ show invSize ++
" (total of " ++ show (sum invSize) ++ ")"
mapM_ (putLine . show) inv
checkStrongConsensus :: PopulationProtocol -> OptIO PropResult
checkStrongConsensus pp = do
......@@ -148,7 +138,7 @@ checkLayeredTermination pp = do
checkLayeredTermination' :: PopulationProtocol -> [Triplet] -> Integer -> Integer -> OptIO PropResult
checkLayeredTermination' pp triplets k kmax = do
verbosePut 1 $ "Checking terminal marking reachable with at most " ++ show k ++ " partitions"
verbosePut 1 $ "Checking layered termination with at most " ++ show k ++ " layers"
r <- checkSatMin $ checkLayeredTerminationSat pp triplets k
case r of
Nothing ->
......@@ -158,10 +148,8 @@ checkLayeredTermination' pp triplets k kmax = do
return Unknown
Just inv -> do
invariant <- opt optInvariant
if invariant then
printInvariant (Just inv, [])
else
return Satisfied
when invariant $ printInvariant inv
return Satisfied
main :: IO ()
main = do
......
......@@ -2,8 +2,8 @@
{-# OPTIONS_GHC -fno-warn-name-shadowing #-}
module PopulationProtocol
(PopulationProtocol,State(..),Transition(..),Marking,FiringVector,
RMarking,RFiringVector,
(PopulationProtocol,State(..),Transition(..),Configuration,FiringVector,
RConfiguration,RFiringVector,
renameState,renameTransition,renameStatesAndTransitions,
name,showNetName,states,transitions,
initialStates,
......@@ -29,8 +29,6 @@ instance Show State where
instance Show Transition where
show (Transition t) = t
type SimpleCut = (S.Set Transition, [S.Set Transition])
type ContextMap a b = M.Map a ([(b, Integer)],[(b, Integer)])
class (Ord a, Ord b) => Nodes a b | a -> b where
......@@ -59,16 +57,14 @@ instance Nodes State Transition where
instance Nodes Transition State where
contextMap = adjacencyT
type Marking = IVector State
type Configuration = IVector State
type FiringVector = IVector Transition
type RMarking = RVector State
type RConfiguration = RVector State
type RFiringVector = RVector Transition
type Trap = [State]
type Siphon = [State]
-- TODO: generalize cut type
type Cut = ([([State], [Transition])], [Transition])
class Invariant a where
invariantSize :: a -> Int
......
......@@ -75,7 +75,7 @@ checkLayeredTerminationSat pp triplets k =
ys = [makeVarMapWith (makeYName i) $ states pp | i <- [1..k]]
b = makeVarMap $ transitions pp
in (minimizeMethod, \sizeLimit ->
("terminal marking reachable", "invariant",
("layered termination", "invariant",
concat (map getNames ys) ++ getNames b,
\fm -> checkLayeredTermination pp triplets k (fmap fm b) (map (fmap fm) ys) sizeLimit,
\fm -> invariantFromAssignment pp k (fmap fm b) (map (fmap fm) ys)))
......
......@@ -19,7 +19,7 @@ import PopulationProtocol
import Property
import Solver
type StrongConsensusCounterExample = (Marking, Marking, Marking, FiringVector, FiringVector)
type StrongConsensusCounterExample = (Configuration, Configuration, Configuration, FiringVector, FiringVector)
type StableInequality = (IMap State, Integer)
......@@ -43,19 +43,19 @@ terminalConstraints pp m =
where checkTransition t = bOr $ map checkState $ lpre pp t
checkState (q,w) = val m q .<= literal (fromInteger (w - 1))
initialMarkingConstraints :: PopulationProtocol -> SIMap State -> SBool
initialMarkingConstraints pp m0 =
initialConfiguration :: PopulationProtocol -> SIMap State -> SBool
initialConfiguration pp m0 =
sum (mval m0 (states pp \\ initialStates pp)) .== 0
differentConsensusConstraints :: PopulationProtocol -> SIMap State -> SIMap State -> SBool
differentConsensusConstraints pp m1 m2 =
(sum (mval m1 (yesStates pp)) .> 0 &&& sum (mval m2 (noStates pp)) .> 0)
unmarkedByMarking :: [State] -> SIMap State -> SBool
unmarkedByMarking r m = sum (mval m r) .== 0
unmarkedByConfiguration :: [State] -> SIMap State -> SBool
unmarkedByConfiguration r m = sum (mval m r) .== 0
markedByMarking :: [State] -> SIMap State -> SBool
markedByMarking r m = sum (mval m r) .> 0
markedByConfiguration :: [State] -> SIMap State -> SBool
markedByConfiguration r m = sum (mval m r) .> 0
sequenceNotIn :: [Transition] -> SIMap Transition -> SBool
sequenceNotIn u x = sum (mval x u) .== 0
......@@ -65,8 +65,8 @@ sequenceIn u x = sum (mval x u) .> 0
checkUTrap :: PopulationProtocol -> SIMap State -> SIMap State -> SIMap State -> SIMap Transition -> SIMap Transition -> Trap -> SBool
checkUTrap pp m0 m1 m2 x1 x2 utrap =
(((sequenceIn upre x1) &&& (sequenceNotIn uunmark x1)) ==> (markedByMarking utrap m1)) &&&
(((sequenceIn upre x2) &&& (sequenceNotIn uunmark x2)) ==> (markedByMarking utrap m2))
(((sequenceIn upre x1) &&& (sequenceNotIn uunmark x1)) ==> (markedByConfiguration utrap m1)) &&&
(((sequenceIn upre x2) &&& (sequenceNotIn uunmark x2)) ==> (markedByConfiguration utrap m2))
where upost = mpost pp utrap
upre = mpre pp utrap
uunmark = upost \\ upre
......@@ -77,8 +77,8 @@ checkUTrapConstraints pp m0 m1 m2 x1 x2 traps =
checkUSiphon :: PopulationProtocol -> SIMap State -> SIMap State -> SIMap State -> SIMap Transition -> SIMap Transition -> Siphon -> SBool
checkUSiphon pp m0 m1 m2 x1 x2 usiphon =
(((sequenceIn upost x1) &&& (sequenceNotIn umark x1)) ==> (markedByMarking usiphon m0)) &&&
(((sequenceIn upost x2) &&& (sequenceNotIn umark x2)) ==> (markedByMarking usiphon m0))
(((sequenceIn upost x1) &&& (sequenceNotIn umark x1)) ==> (markedByConfiguration usiphon m0)) &&&
(((sequenceIn upost x2) &&& (sequenceNotIn umark x2)) ==> (markedByConfiguration usiphon m0))
where upost = mpost pp usiphon
upre = mpre pp usiphon
umark = upre \\ upost
......@@ -101,7 +101,7 @@ checkStrongConsensus :: PopulationProtocol -> SIMap State -> SIMap State -> SIMa
checkStrongConsensus pp m0 m1 m2 x1 x2 utraps usiphons inequalities =
stateEquationConstraints pp m0 m1 x1 &&&
stateEquationConstraints pp m0 m2 x2 &&&
initialMarkingConstraints pp m0 &&&
initialConfiguration pp m0 &&&
nonNegativityConstraints m0 &&&
nonNegativityConstraints m1 &&&
nonNegativityConstraints m2 &&&
......@@ -121,13 +121,13 @@ checkStrongConsensusSat pp utraps usiphons inequalities =
m2 = makeVarMapWith (prime . prime) $ states pp
x1 = makeVarMap $ transitions pp
x2 = makeVarMapWith prime $ transitions pp
in ("unique terminal marking", "(m0, m1, m2, x1, x2)",
in ("strong consensus", "(c0, c1, c2, x1, x2)",
getNames m0 ++ getNames m1 ++ getNames m2 ++ getNames x1 ++ getNames x2,
\fm -> checkStrongConsensus pp (fmap fm m0) (fmap fm m1) (fmap fm m2) (fmap fm x1) (fmap fm x2) utraps usiphons inequalities,
\fm -> markingsFromAssignment (fmap fm m0) (fmap fm m1) (fmap fm m2) (fmap fm x1) (fmap fm x2))
\fm -> configurationsFromAssignment (fmap fm m0) (fmap fm m1) (fmap fm m2) (fmap fm x1) (fmap fm x2))
markingsFromAssignment :: IMap State -> IMap State -> IMap State -> IMap Transition -> IMap Transition -> StrongConsensusCounterExample
markingsFromAssignment m0 m1 m2 x1 x2 =
configurationsFromAssignment :: IMap State -> IMap State -> IMap State -> IMap Transition -> IMap Transition -> StrongConsensusCounterExample
configurationsFromAssignment m0 m1 m2 x1 x2 =
(makeVector m0, makeVector m1, makeVector m2, makeVector x1, makeVector x2)
-- trap and siphon refinement constraints
......@@ -152,11 +152,11 @@ uSiphonConstraints :: PopulationProtocol -> FiringVector -> SIMap State -> SBool
uSiphonConstraints pp x b =
bAnd $ map (siphonConstraint pp b) $ elems x
statesMarkedByMarking :: PopulationProtocol -> Marking -> SIMap State -> SBool
statesMarkedByMarking pp m b = sum (mval b $ elems m) .> 0
statesMarkedByConfiguration :: PopulationProtocol -> Configuration -> SIMap State -> SBool
statesMarkedByConfiguration pp m b = sum (mval b $ elems m) .> 0
statesUnmarkedByMarking :: PopulationProtocol -> Marking -> SIMap State -> SBool
statesUnmarkedByMarking pp m b = sum (mval b $ elems m) .== 0
statesUnmarkedByConfiguration :: PopulationProtocol -> Configuration -> SIMap State -> SBool
statesUnmarkedByConfiguration pp m b = sum (mval b $ elems m) .== 0
statesPostsetOfSequence :: PopulationProtocol -> FiringVector -> SIMap State -> SBool
statesPostsetOfSequence pp x b = sum (mval b $ mpost pp $ elems x) .> 0
......@@ -164,7 +164,7 @@ statesPostsetOfSequence pp x b = sum (mval b $ mpost pp $ elems x) .> 0
statesPresetOfSequence :: PopulationProtocol -> FiringVector -> SIMap State -> SBool
statesPresetOfSequence pp x b = sum (mval b $ mpre pp $ elems x) .> 0
noOutputTransitionEnabled :: PopulationProtocol -> Marking -> SIMap State -> SBool
noOutputTransitionEnabled :: PopulationProtocol -> Configuration -> SIMap State -> SBool
noOutputTransitionEnabled pp m b =
bAnd $ map outputTransitionNotEnabled $ transitions pp
where
......@@ -189,17 +189,17 @@ minimizeMethod 1 curSize = "size smaller than " ++ show curSize
minimizeMethod 2 curSize = "size larger than " ++ show curSize
minimizeMethod _ _ = error "minimization method not supported"
findTrap :: PopulationProtocol -> Marking -> Marking -> Marking -> FiringVector -> FiringVector -> SIMap State -> Maybe (Int, Integer) -> SBool
findTrap :: PopulationProtocol -> Configuration -> Configuration -> Configuration -> FiringVector -> FiringVector -> SIMap State -> Maybe (Int, Integer) -> SBool
findTrap pp m0 m1 m2 x1 x2 b sizeLimit =
checkSizeLimit b sizeLimit &&&
checkBinary b &&&
trapConstraints pp b &&&
(
(statesPostsetOfSequence pp x1 b &&& statesUnmarkedByMarking pp m1 b) |||
(statesPostsetOfSequence pp x2 b &&& statesUnmarkedByMarking pp m2 b)
(statesPostsetOfSequence pp x1 b &&& statesUnmarkedByConfiguration pp m1 b) |||
(statesPostsetOfSequence pp x2 b &&& statesUnmarkedByConfiguration pp m2 b)
)
findTrapConstraintsSat :: PopulationProtocol -> Marking -> Marking -> Marking -> FiringVector -> FiringVector -> MinConstraintProblem Integer Trap Integer
findTrapConstraintsSat :: PopulationProtocol -> Configuration -> Configuration -> Configuration -> FiringVector -> FiringVector -> MinConstraintProblem Integer Trap Integer
findTrapConstraintsSat pp m0 m1 m2 x1 x2 =
let b = makeVarMap $ states pp
in (minimizeMethod, \sizeLimit ->
......@@ -208,16 +208,16 @@ findTrapConstraintsSat pp m0 m1 m2 x1 x2 =
\fm -> findTrap pp m0 m1 m2 x1 x2 (fmap fm b) sizeLimit,
\fm -> statesFromAssignment (fmap fm b)))
findUTrapConstraints :: PopulationProtocol -> Marking -> Marking -> Marking -> FiringVector -> FiringVector -> SIMap State -> Maybe (Int, Integer) -> SBool
findUTrapConstraints :: PopulationProtocol -> Configuration -> Configuration -> Configuration -> FiringVector -> FiringVector -> SIMap State -> Maybe (Int, Integer) -> SBool
findUTrapConstraints pp m0 m1 m2 x1 x2 b sizeLimit =
checkSizeLimit b sizeLimit &&&
checkBinary b &&&
(
(statesPostsetOfSequence pp x1 b &&& uTrapConstraints pp x1 b &&& statesUnmarkedByMarking pp m1 b) |||
(statesPostsetOfSequence pp x2 b &&& uTrapConstraints pp x2 b &&& statesUnmarkedByMarking pp m2 b)
(statesPostsetOfSequence pp x1 b &&& uTrapConstraints pp x1 b &&& statesUnmarkedByConfiguration pp m1 b) |||
(statesPostsetOfSequence pp x2 b &&& uTrapConstraints pp x2 b &&& statesUnmarkedByConfiguration pp m2 b)
)
findUTrapConstraintsSat :: PopulationProtocol -> Marking -> Marking -> Marking -> FiringVector -> FiringVector -> MinConstraintProblem Integer Trap Integer
findUTrapConstraintsSat :: PopulationProtocol -> Configuration -> Configuration -> Configuration -> FiringVector -> FiringVector -> MinConstraintProblem Integer Trap Integer
findUTrapConstraintsSat pp m0 m1 m2 x1 x2 =
let b = makeVarMap $ states pp
in (minimizeMethod, \sizeLimit ->
......@@ -226,17 +226,17 @@ findUTrapConstraintsSat pp m0 m1 m2 x1 x2 =
\fm -> findUTrapConstraints pp m0 m1 m2 x1 x2 (fmap fm b) sizeLimit,
\fm -> statesFromAssignment (fmap fm b)))
findUSiphonConstraints :: PopulationProtocol -> Marking -> Marking -> Marking -> FiringVector -> FiringVector -> SIMap State -> Maybe (Int, Integer) -> SBool
findUSiphonConstraints :: PopulationProtocol -> Configuration -> Configuration -> Configuration -> FiringVector -> FiringVector -> SIMap State -> Maybe (Int, Integer) -> SBool
findUSiphonConstraints pp m0 m1 m2 x1 x2 b sizeLimit =
checkSizeLimit b sizeLimit &&&
checkBinary b &&&
statesUnmarkedByMarking pp m0 b &&&
statesUnmarkedByConfiguration pp m0 b &&&
(
(statesPresetOfSequence pp x1 b &&& uSiphonConstraints pp x1 b) |||
(statesPresetOfSequence pp x2 b &&& uSiphonConstraints pp x2 b)
)
findUSiphonConstraintsSat :: PopulationProtocol -> Marking -> Marking -> Marking -> FiringVector -> FiringVector -> MinConstraintProblem Integer Siphon Integer
findUSiphonConstraintsSat :: PopulationProtocol -> Configuration -> Configuration -> Configuration -> FiringVector -> FiringVector -> MinConstraintProblem Integer Siphon Integer
findUSiphonConstraintsSat pp m0 m1 m2 x1 x2 =
let b = makeVarMap $ states pp
in (minimizeMethod, \sizeLimit ->
......@@ -250,8 +250,8 @@ statesFromAssignment b = (M.keys (M.filter (> 0) b), sum (M.elems b))
-- stable linear inequalities
checkStableInequalityForMarking :: PopulationProtocol -> Marking -> SIMap State -> SInteger -> SBool
checkStableInequalityForMarking pp m k c =
checkStableInequalityForConfiguration :: PopulationProtocol -> Configuration -> SIMap State -> SInteger -> SBool
checkStableInequalityForConfiguration pp m k c =
sum [ (val k q) * literal (val m q) | q <- states pp ] .>= c
checkSemiPositiveConstraints :: (Ord a, Show a) => SIMap a -> SBool
......@@ -275,14 +275,14 @@ checkGeneralizedCoTrap :: PopulationProtocol -> SIMap State -> SInteger -> SBool
checkGeneralizedCoTrap pp k c =
bAnd [ checkGeneralizedTCoTrap pp k c t | t <- transitions pp ]
checkGeneralizedCoTrapConstraints :: PopulationProtocol -> Marking -> Marking -> Marking -> FiringVector -> FiringVector -> SIMap State -> SInteger -> SBool
checkGeneralizedCoTrapConstraints :: PopulationProtocol -> Configuration -> Configuration -> Configuration -> FiringVector -> FiringVector -> SIMap State -> SInteger -> SBool
checkGeneralizedCoTrapConstraints pp m0 m1 m2 x1 x2 k c =
checkSemiNegativeConstraints k &&&
checkGeneralizedCoTrap pp k c &&&
checkStableInequalityForMarking pp m0 k c &&&
((bnot (checkStableInequalityForMarking pp m1 k c)) ||| (bnot (checkStableInequalityForMarking pp m2 k c)))
checkStableInequalityForConfiguration pp m0 k c &&&
((bnot (checkStableInequalityForConfiguration pp m1 k c)) ||| (bnot (checkStableInequalityForConfiguration pp m2 k c)))
checkGeneralizedCoTrapSat :: PopulationProtocol -> Marking -> Marking -> Marking -> FiringVector -> FiringVector -> ConstraintProblem Integer StableInequality
checkGeneralizedCoTrapSat :: PopulationProtocol -> Configuration -> Configuration -> Configuration -> FiringVector -> FiringVector -> ConstraintProblem Integer StableInequality
checkGeneralizedCoTrapSat pp m0 m1 m2 x1 x2 =
let k = makeVarMap $ states pp
c = "'c"
......
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