Commit 46c2f0be authored by Philipp Meyer's avatar Philipp Meyer
Browse files

Added liveness invariant generation back

parent 59d672f9
......@@ -31,7 +31,7 @@ import Solver.StateEquation
import Solver.TrapConstraints
import Solver.TransitionInvariant
import Solver.SubnetEmptyTrap
--import Solver.LivenessInvariant
import Solver.LivenessInvariant
import Solver.SComponent
--import Solver.CommFreeReachability
......@@ -471,10 +471,17 @@ checkLivenessProperty :: Int -> PetriNet -> Bool -> Bool ->
checkLivenessProperty verbosity net refine invariant f = do
r <- checkLivenessProperty' verbosity net refine f []
case r of
(Nothing, _) ->
if invariant then
-- TODO: add invariant generation
error "Invariant generation for liveness properties not yet supported"
(Nothing, cuts) ->
if invariant then do
r' <- checkSat verbosity $ checkLivenessInvariantSat net f cuts
case r' of
Nothing -> do
verbosePut verbosity 0 "No invariant found"
return Unknown
Just inv -> do
verbosePut verbosity 0 "Invariant found"
mapM_ print inv
return Satisfied
else
return Satisfied
(Just _, _) ->
......
......@@ -7,11 +7,12 @@ module PetriNet
name,showNetName,places,transitions,
initialMarking,initial,initials,linitials,
pre,lpre,post,lpost,mpre,mpost,context,ghostTransitions,
makePetriNet,makePetriNetWithTrans,makePetriNetWith,Trap,Cut,constructCut)
makePetriNet,makePetriNetWithTrans,makePetriNetWith,Trap,Cut,
constructCut)
where
import qualified Data.Map as M
import Control.Arrow (first)
import Control.Arrow (first,(***))
import Data.List (sort)
import Util
......@@ -56,7 +57,8 @@ type Marking = Vector Place
type FiringVector = Vector Transition
type Trap = [Place]
type Cut = ([[Transition]], [Transition])
-- TODO: generalize cut type
type Cut = ([([Place], [Transition])], [Transition])
data PetriNet = PetriNet {
name :: String,
......@@ -117,10 +119,17 @@ renamePetriNetPlacesAndTransitions f net =
mapContext f (pre, post) = (map (first f) pre, map (first f) post)
-- TODO: use strongly connected components and min cuts
constructCut :: PetriNet -> FiringVector -> [Trap] -> Cut
constructCut' :: Cut -> Cut
constructCut' (ts, u) =
(nubOrd (map (sort *** sort) ts), nubOrd u)
constructCut:: PetriNet -> FiringVector -> [Trap] -> Cut
constructCut net x traps =
(nubOrd (map (sort . filter (\t -> val x t > 0) . mpre net) traps),
nubOrd (concatMap (filter (\t -> val x t == 0) . mpost net) traps))
constructCut' (map trapComponent traps, concatMap trapOutput traps)
where trapComponent trap =
(trap, filter (\t -> val x t > 0) (mpre net trap))
trapOutput trap =
filter (\t -> val x t == 0) (mpost net trap)
-- TODO: better constructors, only one main constructor
-- TODO: enforce sorted lists
......
module Solver.LivenessInvariant (
checkLivenessInvariant
, checkLivenessInvariantSat
, generateCuts
, getLivenessInvariant
, PlaceVector
, LivenessInvariant(..)
checkLivenessInvariantSat
, LivenessInvariant
) where
import Data.SBV
import Data.List (intercalate)
import qualified Data.Map as M
import Util
import Solver
import Solver.SComponent
import Property
import PetriNet
type PlaceVector = [(String, Integer)]
newtype LivenessInvariant =
LivenessInvariant { getInv :: (String, [Cut], PlaceVector) }
data LivenessInvariant =
RankingFunction (String, [SimpleCut], Vector Place)
| ComponentCut (String, [SimpleCut], [Trap])
showSimpleCuts :: [SimpleCut] -> Bool -> String
showSimpleCuts cs inv = intercalate " ∧ " (map showTrans cs)
where showTrans (ts, b) =
if b && inv || not b && not inv then
intercalate " ∧ " (map (\t -> show t ++ " ∉ σ") ts)
else
let d = intercalate " ∨ "
(map (\t -> show t ++ " ∈ σ") ts)
in if length ts == 1 then d else "(" ++ d ++ ")"
instance Show LivenessInvariant where
show (LivenessInvariant (n, cs, xs)) = n ++ " [" ++
intercalate " ∧ " (map showTrans cs) ++ "]: " ++
intercalate " + " (map showPlace (filter ((> 0) . snd) xs))
where showPlace (p, w) = show w ++ p
showTrans (ts, b) =
if b then
intercalate " ∧ " (map (++ " ∉ σ") ts)
else
let d = intercalate " ∨ " (map (++ " ∈ σ") ts)
in if length ts == 1 then d else "(" ++ d ++ ")"
type Cut = ([String], Bool)
type NamedCut = (String, [(String, Cut)])
generateCuts :: Formula -> [SCompCut] -> [NamedCut]
generateCuts f comps =
show (RankingFunction (n, cs, xs)) = n ++
" [" ++ showSimpleCuts cs True ++ "]: " ++
intercalate " + " (map showPlace (items xs))
where showPlace (p, w) = show w ++ show p
show (ComponentCut (n, cs, ps)) = n ++
" [" ++ showSimpleCuts cs False ++ "]: " ++
show ps
type SimpleCut = ([Transition], Bool)
type NamedCut = (String, [(String, SimpleCut)])
placeName :: String -> Place -> String
placeName n p = n ++ "@p" ++ show p
numPref :: String -> [String]
numPref s = map (\i -> s ++ show i) [(1::Integer)..]
generateCuts :: Formula Transition -> [Cut] -> [NamedCut]
generateCuts f cuts =
zipWith nameCut
(numPref "@part")
(foldl combine [formulaToCut f] comps)
(numPref "@r")
(foldl combine [formulaToCut f] (map cutToSimpleCuts cuts))
where
nameCut n c = (n, numPref "@comp" `zip` c)
numPref s = map (\i -> s ++ show i) [(1::Integer)..]
combine cuts compCut = [x : c | x <- compCut, c <- cuts]
combine curCuts compCut = [x : c | x <- compCut, c <- curCuts]
varNames :: PetriNet -> [NamedCut] -> [String]
varNames net = concatMap cutNames
where
cutNames (n, c) =
[n ++ "@comp0"] ++
map (\p -> n ++ "@p" ++ p) (places net) ++
map (placeName n) (places net) ++
map (\(n', _) -> n ++ n') c
formulaToCut :: Formula -> SCompCut
formulaToCut = transformConj
cutToSimpleCuts :: Cut -> [SimpleCut]
cutToSimpleCuts (ts,u) = (u, False) : map (\(_, t) -> (t, True)) ts
formulaToCut :: Formula Transition -> [SimpleCut]
formulaToCut = transformF
where
transformConj FTrue = []
transformConj (p :&: q) = transformConj p ++ transformConj q
transformConj (Atom lieq) = transformLieq lieq
transformConj form =
error $ "formula not supported for invariant: " ++ show form
transformLieq (LinIneq ts Gt (Const 0)) = [(transformTerm ts, False)]
transformLieq (LinIneq ts Ge (Const 1)) = [(transformTerm ts, False)]
transformLieq (LinIneq ts Eq (Const 0)) = [(transformTerm ts, True)]
transformLieq (LinIneq ts Le (Const 0)) = [(transformTerm ts, True)]
transformLieq (LinIneq ts Lt (Const 1)) = [(transformTerm ts, True)]
transformLieq l =
error $ "linear inequation not supported for invariant: " ++ show l
transformF FTrue = []
transformF (p :&: q) = transformF p ++ transformF q
transformF (LinearInequation ts Gt (Const 0)) =
[(transformTerm ts, False)]
transformF (LinearInequation ts Ge (Const 1)) =
[(transformTerm ts, False)]
transformF (LinearInequation ts Eq (Const 0)) =
[(transformTerm ts, True)]
transformF (LinearInequation ts Le (Const 0)) =
[(transformTerm ts, True)]
transformF (LinearInequation ts Lt (Const 1)) =
[(transformTerm ts, True)]
transformF f =
error $ "formula not supported for invariant: " ++ show f
transformTerm (t :+: u) = transformTerm t ++ transformTerm u
transformTerm (Var x) = [x]
transformTerm t =
error $ "term not supported for invariant: " ++ show t
checkCut :: PetriNet -> ModelSI -> NamedCut -> SBool
checkCut :: PetriNet -> SIMap String -> NamedCut -> SBool
checkCut net m (n, comps) =
bAnd (map checkTransition (transitions net)) &&&
mVal m (n ++ "@comp0") + sum (map addComp2 comps) .> 0 &&&
bAnd (map (\p -> checkNonNegativity (n ++ "@p" ++ p)) (places net)) &&&
val m (n ++ "@comp0") + sum (map addComp2 comps) .> 0 &&&
bAnd (map (checkNonNegativity . placeName n) (places net)) &&&
checkNonNegativity (n ++ "@comp0") &&&
bAnd (map (\(n', _) -> checkNonNegativity (n ++ n')) comps)
where checkTransition t =
let incoming = map addPlace $ lpre net t
outgoing = map addPlace $ lpost net t
zeroComp = mVal m (n ++ "@comp0")
zeroComp = val m (n ++ "@comp0")
addComp1 (n', (ts, xv)) =
if t `elem` ts then
(if xv then 1 else (-1)) * mVal m (n ++ n')
(if xv then 1 else (-1)) * val m (n ++ n')
else
0
cutComps = map addComp1 comps
in sum outgoing - sum incoming + zeroComp .<= sum cutComps
addPlace (p,w) = literal w * mVal m (n ++ "@p" ++ p)
addComp2 (n', (_, w)) = if w then 0 else mVal m (n ++ n')
checkNonNegativity x = mVal m x .>= 0
addPlace (p,w) = literal w * val m (placeName n p)
addComp2 (n', (_, w)) = if w then 0 else val m (n ++ n')
checkNonNegativity x = val m x .>= 0
checkLivenessInvariant :: PetriNet -> [NamedCut] ->
ModelSI -> SBool
checkLivenessInvariant :: PetriNet -> [NamedCut] -> SIMap String -> SBool
checkLivenessInvariant net cuts m =
bAnd (map (checkCut net m) cuts)
checkLivenessInvariantSat :: PetriNet -> [NamedCut] ->
([String], ModelSI -> SBool)
checkLivenessInvariantSat net cuts =
(varNames net cuts, checkLivenessInvariant net cuts)
checkLivenessInvariantSat :: PetriNet -> Formula Transition -> [Cut] ->
ConstraintProblem Integer [LivenessInvariant]
checkLivenessInvariantSat net f cuts =
let namedCuts = generateCuts f cuts
names = varNames net namedCuts
myVarMap fvm = M.fromList $ names `zip` fmap fvm names
in ("liveness invariant constraints", "liveness invariant",
names,
checkLivenessInvariant net namedCuts . myVarMap,
getLivenessInvariant net cuts namedCuts . myVarMap)
getLivenessInvariant :: PetriNet -> [NamedCut] -> ModelI -> [LivenessInvariant]
getLivenessInvariant net cuts as = map lookupCut cuts
where lookupCut (n, c) = LivenessInvariant
(n, map snd c, map (\p -> (p, mVal as (n ++ "@p" ++ p))) (places net))
getLivenessInvariant :: PetriNet -> [Cut] -> [NamedCut] -> IMap String ->
[LivenessInvariant]
getLivenessInvariant net cuts namedCuts y =
map rankCut namedCuts ++ zipWith compCut (numPref "@cut") cuts
where rankCut (n, c) = RankingFunction
(n, map snd c,
buildVector (map (\p -> (p, val y (placeName n p))) (places net)))
compCut n c = ComponentCut
(n, cutToSimpleCuts c, map fst (fst c))
......@@ -93,7 +93,6 @@ cutFromAssignment :: PetriNet -> FiringVector -> IMap Place ->
cutFromAssignment net x p' t' y =
let ts = filter (\t -> val x t > 0) $ elems $ M.filter (> 0) t'
(t1, t2) = partition (\t -> val y t > 0) ts
--let (ts, u) = partition (\t -> val x t > 0) $ elems $ M.filter (> 0) t'
s1 = filter (\p -> val p' p > 0) $ mpre net t1
s2 = filter (\p -> val p' p > 0) $ mpre net t2
in constructCut net x [s1,s2]
......
......@@ -28,7 +28,7 @@ nonnegativityConstraints x = bAnd $ map (.>= 0) (vals x)
checkCuts :: [Cut] -> SIMap Transition -> SBool
checkCuts cuts x = bAnd $ map checkCut cuts
where checkCut (ts, u) =
let cPre = map (bOr . map (positiveVal x)) ts
let cPre = map (bOr . map (positiveVal x) . snd) ts
cPost = map (positiveVal x) u
in bAnd cPre ==> bOr cPost
......
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