Commit 5168f823 authored by Philipp Meyer's avatar Philipp Meyer
Browse files

Rewrote transition invariant constraints

parent 559d93aa
......@@ -29,7 +29,7 @@ import Structure
import Solver
import Solver.StateEquation
import Solver.TrapConstraints
--import Solver.TransitionInvariant
import Solver.TransitionInvariant
--import Solver.SubnetEmptyTrap
--import Solver.LivenessInvariant
--import Solver.SComponent
......@@ -421,7 +421,7 @@ checkProperty verbosity net refine invariant p = do
verbosePut verbosity 3 $ show p
r <- case pcont p of
(Safety pf) -> checkSafetyProperty verbosity net refine invariant pf
-- (Liveness pf) -> checkLivenessProperty verbosity net refine invariant pf
(Liveness pf) -> checkLivenessProperty verbosity net refine invariant pf
(Structural ps) -> checkStructuralProperty verbosity net ps
verbosePut verbosity 0 $ showPropertyName p ++ " " ++
case r of
......@@ -465,7 +465,7 @@ refineSafetyProperty verbosity net f traps m = do
return (Just m, traps)
Just trap ->
checkSafetyProperty' verbosity net True f (trap:traps)
{-
checkLivenessProperty :: Int -> PetriNet -> Bool -> Bool ->
Formula Transition -> IO PropResult
checkLivenessProperty verbosity net refine invariant f = do
......@@ -479,7 +479,7 @@ checkLivenessProperty verbosity net refine invariant f = do
return Satisfied
(Just _, _) ->
return Unknown
-}
{-
generateLivenessInvariant :: Int -> PetriNet ->
Formula -> [SCompCut] -> IO PropResult
......@@ -494,7 +494,7 @@ generateLivenessInvariant verbosity net f comps = do
mapM_ print inv
return Satisfied
-}
{-
checkLivenessProperty' :: Int -> PetriNet -> Bool ->
Formula Transition -> [Cut] -> IO (Maybe FiringVector, [Cut])
checkLivenessProperty' verbosity net refine f cuts = do
......@@ -503,7 +503,8 @@ checkLivenessProperty' verbosity net refine f cuts = do
Nothing -> return (Nothing, cuts)
Just x ->
if refine then do
rt <- findLivenessRefinement verbosity net x
--rt <- findLivenessRefinement verbosity net x
let rt = Nothing
case rt of
Nothing ->
return (Just x, cuts)
......@@ -512,7 +513,7 @@ checkLivenessProperty' verbosity net refine f cuts = do
(cut:cuts)
else
return (Just x, cuts)
{-
findLivenessRefinement :: Int -> PetriNet -> FiringVector ->
IO (Maybe Cut)
findLivenessRefinement verbosity net x = do
......
......@@ -3,7 +3,6 @@ module Solver.TransitionInvariant
where
import Data.SBV
import Control.Monad
import Util
import PetriNet
......@@ -11,44 +10,37 @@ import Property
import Solver
import Solver.Formula
tInvariantConstraints :: PetriNet -> VarMap Transition -> IntConstraint
tInvariantConstraints :: PetriNet -> SIMap Transition -> SBool
tInvariantConstraints net x =
liftM bAnd $ mapM checkTransitionEquation $ places net
where checkTransitionEquation p = do
incoming <- mapM addTransition $ lpre net p
outgoing <- mapM addTransition $ lpost net p
return $ sum incoming - sum outgoing .>= 0
addTransition (t,w) = liftM (literal w *) (val x t)
bAnd $ map checkTransitionEquation $ places net
where checkTransitionEquation p =
let incoming = map addTransition $ lpre net p
outgoing = map addTransition $ lpost net p
in sum incoming - sum outgoing .>= 0
addTransition (t,w) = literal w * val x t
finalInvariantConstraints :: VarMap Transition -> IntConstraint
finalInvariantConstraints x = do
xs <- vals x
return $ sum xs .> 0
finalInvariantConstraints :: SIMap Transition -> SBool
finalInvariantConstraints x = sum (vals x) .> 0
nonnegativityConstraints :: VarMap Transition -> IntConstraint
nonnegativityConstraints x = do
xs <- vals x
return $ bAnd $ map (.>= 0) xs
nonnegativityConstraints :: SIMap Transition -> SBool
nonnegativityConstraints x = bAnd $ map (.>= 0) (vals x)
-- TODO: check how changing the representation changes result
checkCuts :: [Cut] -> VarMap Transition -> IntConstraint
checkCuts cuts x =
liftM bAnd $ mapM checkCut cuts
where checkCut (ts, u) = do
cPre <- mapM (liftM (bnot . bOr) . mapM positive) ts
cPost <- mapM positive u
return $ bOr cPre ||| bOr cPost
positive t = liftM (.> 0) (val x t)
checkCuts :: [Cut] -> SIMap Transition -> SBool
checkCuts cuts x = bAnd $ map checkCut cuts
where checkCut (ts, u) =
let cPre = map ((bnot . bOr) . map (positiveVal x)) ts
cPost = map (positiveVal x) u
in bOr cPre ||| bOr cPost
checkTransitionInvariant :: PetriNet -> Formula Transition ->
[Cut] -> VarMap Transition -> IntConstraint
checkTransitionInvariant net f cuts x = do
c1 <- tInvariantConstraints net x
c2 <- nonnegativityConstraints x
c3 <- finalInvariantConstraints x
c4 <- checkCuts cuts x
c5 <- evaluateFormula f x
return $ c1 &&& c2 &&& c3 &&& c4 &&& c5
[Cut] -> SIMap Transition -> SBool
checkTransitionInvariant net f cuts x =
tInvariantConstraints net x &&&
nonnegativityConstraints x &&&
finalInvariantConstraints x &&&
checkCuts cuts x &&&
evaluateFormula f x
checkTransitionInvariantSat :: PetriNet -> Formula Transition -> [Cut] ->
ConstraintProblem Integer FiringVector
......@@ -56,10 +48,9 @@ checkTransitionInvariantSat net f cuts =
let x = makeVarMap $ transitions net
in ("transition invariant constraints", "transition invariant",
getNames x,
checkTransitionInvariant net f cuts x,
firingVectorFromAssignment x)
\fm -> checkTransitionInvariant net f cuts (fmap fm x),
\fm -> firingVectorFromAssignment (fmap fm x))
firingVectorFromAssignment :: VarMap Transition -> IntResult FiringVector
firingVectorFromAssignment x =
liftM makeVector $ valMap x
firingVectorFromAssignment :: IMap Transition -> FiringVector
firingVectorFromAssignment = makeVector
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