Commit bd8ccccd authored by Philipp Meyer's avatar Philipp Meyer
Browse files

Added refinement via s-components for t-invariants

parent d6b41fdc
...@@ -3,6 +3,7 @@ module Main where ...@@ -3,6 +3,7 @@ module Main where
import System.Environment (getArgs) import System.Environment (getArgs)
import System.Exit import System.Exit
import qualified Data.Map as M
import Parser (parseFile) import Parser (parseFile)
import PetriNet import PetriNet
import Property import Property
...@@ -30,31 +31,31 @@ checkSafetyProperty net f traps = do ...@@ -30,31 +31,31 @@ checkSafetyProperty net f traps = do
putStrLn $ "Trap found with places " ++ show trap putStrLn $ "Trap found with places " ++ show trap
checkSafetyProperty net f (trap:traps) checkSafetyProperty net f (trap:traps)
checkLivenessProperty :: PetriNet -> Formula -> IO Bool checkLivenessProperty :: PetriNet -> Formula -> [([String],[String])] -> IO Bool
checkLivenessProperty net f = do checkLivenessProperty net f strans = do
r <- checkSat $ checkTransitionInvariantSat net f r <- checkSat $ checkTransitionInvariantSat net f strans
case r of case r of
Nothing -> return True Nothing -> return True
Just a -> do Just ax -> do
let fired = firedTransitionsFromAssignment a let fired = firedTransitionsFromAssignment ax
putStrLn $ "Assignment found firing " ++ show fired putStrLn $ "Assignment found firing " ++ show fired
rt <- checkSat $ checkSComponentSat net a rt <- checkSat $ checkSComponentSat net ax
case rt of case rt of
Nothing -> do Nothing -> do
putStrLn "No S-component found" putStrLn "No S-component found"
return False return False
Just at -> do Just as -> do
--let trap = trapFromAssignment at let sOutIn = getSComponentInOut net ax as
putStrLn $ "S-component found: " ++ show at putStrLn $ "S-component found: " ++ show (M.filter (> 0) as)
-- checkLivenessProperty net f (trap:traps) putStrLn $ "Out/In: " ++ show sOutIn
return False checkLivenessProperty net f (sOutIn:strans)
checkProperty :: PetriNet -> Property -> IO Bool checkProperty :: PetriNet -> Property -> IO Bool
checkProperty net p = do checkProperty net p = do
putStrLn $ "\nChecking " ++ showPropertyName p putStrLn $ "\nChecking " ++ showPropertyName p
r <- case ptype p of r <- case ptype p of
Safety -> checkSafetyProperty net (pformula p) [] Safety -> checkSafetyProperty net (pformula p) []
Liveness -> checkLivenessProperty net (pformula p) Liveness -> checkLivenessProperty net (pformula p) []
putStrLn $ if r then "Property is satisfied." putStrLn $ if r then "Property is satisfied."
else "Property may not be satisfied." else "Property may not be satisfied."
return r return r
......
module Solver.SComponent module Solver.SComponent
(checkSComponent,checkSComponentSat) (checkSComponent,checkSComponentSat,
getSComponentInOut)
where where
import Data.SBV import Data.SBV
import qualified Data.Map as M import qualified Data.Map as M
import Data.List (partition)
import PetriNet import PetriNet
import Solver import Solver
...@@ -11,9 +13,15 @@ import Solver ...@@ -11,9 +13,15 @@ import Solver
mElem :: ModelSI -> String -> SBool mElem :: ModelSI -> String -> SBool
mElem m x = (m M.! x) .== 1 mElem m x = (m M.! x) .== 1
mElemI :: ModelI -> String -> Bool
mElemI m x = (m M.! x) == 1
mNotElem :: ModelSI -> String -> SBool mNotElem :: ModelSI -> String -> SBool
mNotElem m x = (m M.! x) .== 0 mNotElem m x = (m M.! x) .== 0
mNotElemI :: ModelI -> String -> Bool
mNotElemI m x = (m M.! x) == 0
countElem :: ModelSI -> [String] -> SInteger countElem :: ModelSI -> [String] -> SInteger
countElem m xs = sum $ map (m M.!) xs countElem m xs = sum $ map (m M.!) xs
...@@ -47,12 +55,12 @@ checkNotEmpty :: [String] -> ModelSI -> SBool ...@@ -47,12 +55,12 @@ checkNotEmpty :: [String] -> ModelSI -> SBool
checkNotEmpty fired m = countElem m (map prime fired) .> 0 checkNotEmpty fired m = countElem m (map prime fired) .> 0
checkClosed :: PetriNet -> ModelI -> ModelSI -> SBool checkClosed :: PetriNet -> ModelI -> ModelSI -> SBool
checkClosed net a m = checkClosed net ax m =
bAnd (map checkPlaceClosed (places net)) bAnd (map checkPlaceClosed (places net))
where checkPlaceClosed p = mElem m p ==> where checkPlaceClosed p = mElem m p ==>
bAnd (map checkTransition bAnd (map checkTransition
[(t,t') | t <- pre net p, t' <- post net p, [(t,t') | t <- pre net p, t' <- post net p,
a M.! t > 0 , a M.! t' > 0 ]) ax M.! t > 0 , ax M.! t' > 0 ])
checkTransition (t,t') = checkTransition (t,t') =
mElem m (prime t) &&& mElem m t' ==> mElem m (prime t') mElem m (prime t) &&& mElem m t' ==> mElem m (prime t')
...@@ -65,17 +73,22 @@ checkBinary :: ModelSI -> SBool ...@@ -65,17 +73,22 @@ checkBinary :: ModelSI -> SBool
checkBinary m = bAnd $ map (\x -> x .== 0 ||| x .== 1) $ M.elems m checkBinary m = bAnd $ map (\x -> x .== 0 ||| x .== 1) $ M.elems m
checkSComponent :: PetriNet -> [String] -> ModelI -> ModelSI -> SBool checkSComponent :: PetriNet -> [String] -> ModelI -> ModelSI -> SBool
checkSComponent net fired a m = checkSComponent net fired ax m =
checkPrePostPlaces net m &&& checkPrePostPlaces net m &&&
checkPrePostTransitions net m &&& checkPrePostTransitions net m &&&
checkSubsetTransitions fired m &&& checkSubsetTransitions fired m &&&
checkNotEmpty fired m &&& checkNotEmpty fired m &&&
checkClosed net a m &&& checkClosed net ax m &&&
checkTokens net m &&& checkTokens net m &&&
checkBinary m checkBinary m
checkSComponentSat :: PetriNet -> ModelI -> ([String], ModelSI -> SBool) checkSComponentSat :: PetriNet -> ModelI -> ([String], ModelSI -> SBool)
checkSComponentSat net a = checkSComponentSat net ax =
let fired = M.keys $ M.filter (> 0) a let fired = M.keys $ M.filter (> 0) ax
in (places net ++ transitions net ++ map prime fired, in (places net ++ transitions net ++ map prime fired,
checkSComponent net fired a) checkSComponent net fired ax)
getSComponentInOut :: PetriNet -> ModelI -> ModelI -> ([String], [String])
getSComponentInOut net ax as =
partition (mElemI ax) $ filter (mElemI as) (transitions net)
...@@ -26,16 +26,25 @@ finalInvariantConstraints m = sum (M.elems m) .> 0 ...@@ -26,16 +26,25 @@ finalInvariantConstraints m = sum (M.elems m) .> 0
nonnegativityConstraints :: ModelSI -> SBool nonnegativityConstraints :: ModelSI -> SBool
nonnegativityConstraints m = bAnd $ map (.>= 0) $ M.elems m nonnegativityConstraints m = bAnd $ map (.>= 0) $ M.elems m
checkTransitionInvariant :: PetriNet -> Formula -> ModelSI -> SBool checkSComponentTransitions :: [([String],[String])] -> ModelSI -> SBool
checkTransitionInvariant net f m = checkSComponentTransitions strans m = bAnd $ map checkInOut strans
where checkInOut (sOut,sIn) =
bAnd (map (\t -> m M.! t .> 0) sOut) ==>
bOr (map (\t -> m M.! t .> 0) sIn)
checkTransitionInvariant :: PetriNet -> Formula -> [([String],[String])] ->
ModelSI -> SBool
checkTransitionInvariant net f strans m =
tInvariantConstraints net m &&& tInvariantConstraints net m &&&
nonnegativityConstraints m &&& nonnegativityConstraints m &&&
finalInvariantConstraints m &&& finalInvariantConstraints m &&&
checkSComponentTransitions strans m &&&
evaluateFormula f m evaluateFormula f m
checkTransitionInvariantSat :: PetriNet -> Formula -> ([String], ModelSI -> SBool) checkTransitionInvariantSat :: PetriNet -> Formula -> [([String],[String])] ->
checkTransitionInvariantSat net f = ([String], ModelSI -> SBool)
(transitions net, checkTransitionInvariant net f) checkTransitionInvariantSat net f strans =
(transitions net, checkTransitionInvariant net f strans)
firedTransitionsFromAssignment :: ModelI -> [String] firedTransitionsFromAssignment :: ModelI -> [String]
firedTransitionsFromAssignment a = M.keys $ M.filter ( > 0) a firedTransitionsFromAssignment a = M.keys $ M.filter ( > 0) a
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