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

Refactored model element methods

parent bd8ccccd
...@@ -3,7 +3,6 @@ module Main where ...@@ -3,7 +3,6 @@ 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
...@@ -39,14 +38,14 @@ checkLivenessProperty net f strans = do ...@@ -39,14 +38,14 @@ checkLivenessProperty net f strans = do
Just ax -> do Just ax -> do
let fired = firedTransitionsFromAssignment ax let fired = firedTransitionsFromAssignment ax
putStrLn $ "Assignment found firing " ++ show fired putStrLn $ "Assignment found firing " ++ show fired
rt <- checkSat $ checkSComponentSat net ax rt <- checkSat $ checkSComponentSat net fired 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 as -> do Just as -> do
let sOutIn = getSComponentInOut net ax as let sOutIn = getSComponentInOut net ax as
putStrLn $ "S-component found: " ++ show (M.filter (> 0) as) putStrLn $ "S-component found: " ++ show (mElemsWith (> 0) as)
putStrLn $ "Out/In: " ++ show sOutIn putStrLn $ "Out/In: " ++ show sOutIn
checkLivenessProperty net f (sOutIn:strans) checkLivenessProperty net f (sOutIn:strans)
......
{-# LANGUAGE TypeSynonymInstances, FlexibleInstances #-}
module Solver module Solver
(checkSat,ModelSI,ModelSB,ModelI,ModelB) (checkSat,ModelSI,ModelSB,ModelI,ModelB,
Model(..),mVal,mValues,mElemsWith,mElemSum,SModel(..),CModel(..))
where where
import Data.SBV import Data.SBV
import qualified Data.Map as M import qualified Data.Map as M
type ModelSI = M.Map String SInteger newtype Model a = Model { getMap :: M.Map String a } deriving Show
type ModelSB = M.Map String SBool
type ModelI = M.Map String Integer type ModelSI = Model SInteger
type ModelB = M.Map String Bool type ModelSB = Model SBool
type ModelI = Model Integer
type ModelB = Model Bool
mVal :: Model a -> String -> a
mVal m x = getMap m M.! x
mValues :: Model a -> [a]
mValues m = M.elems $ getMap m
mElemsWith :: (a -> Bool) -> Model a -> [String]
mElemsWith f m = M.keys $ M.filter f $ getMap m
mElemSum :: (Num a) => Model a -> [String] -> a
mElemSum m xs = sum $ map (mVal m) xs
class SModel a where
mElem :: Model a -> String -> SBool
mNotElem :: Model a -> String -> SBool
mNotElem m x = bnot $ mElem m x
class CModel a where
cElem :: Model a -> String -> Bool
cNotElem :: Model a -> String -> Bool
cNotElem m x = not $ cElem m x
instance SModel SInteger where
mElem m x = mVal m x .> 0
mNotElem m x = mVal m x .== 0
instance SModel SBool where
mElem = mVal
mNotElem m x = bnot $ mVal m x
instance CModel Integer where
cElem m x = mVal m x > 0
cNotElem m x = mVal m x == 0
instance CModel Bool where
cElem = mVal
cNotElem m x = not $ mVal m x
symConstraints :: SymWord a => [String] -> (M.Map String (SBV a) -> SBool) -> symConstraints :: SymWord a => [String] -> (Model (SBV a) -> SBool) ->
Symbolic SBool Symbolic SBool
symConstraints vars constraint = do symConstraints vars constraint = do
syms <- mapM exists vars syms <- mapM exists vars
return $ constraint $ M.fromList $ vars `zip` syms return $ constraint $ Model $ M.fromList $ vars `zip` syms
rebuildModel :: SymWord a => [String] -> Either String (Bool, [a]) -> rebuildModel :: SymWord a => [String] -> Either String (Bool, [a]) ->
Maybe (M.Map String a) Maybe (Model a)
rebuildModel _ (Left _) = Nothing rebuildModel _ (Left _) = Nothing
rebuildModel _ (Right (True, _)) = error "Prover returned unknown" rebuildModel _ (Right (True, _)) = error "Prover returned unknown"
rebuildModel vars (Right (False, m)) = Just $ M.fromList $ vars `zip` m rebuildModel vars (Right (False, m)) = Just $ Model $ M.fromList $ vars `zip` m
checkSat :: (SatModel a, SymWord a) => checkSat :: (SatModel a, SymWord a) =>
([String], M.Map String (SBV a) -> SBool) -> ([String], Model (SBV a) -> SBool) ->
IO (Maybe (M.Map String a)) IO (Maybe (Model a))
checkSat (vars, constraint) = do checkSat (vars, constraint) = do
result <- satWith z3{verbose=False} $ symConstraints vars constraint result <- satWith z3{verbose=False} $ symConstraints vars constraint
return $ rebuildModel vars $ getModel result return $ rebuildModel vars $ getModel result
...@@ -3,14 +3,13 @@ module Solver.Formula ...@@ -3,14 +3,13 @@ module Solver.Formula
where where
import Data.SBV import Data.SBV
import qualified Data.Map as M
import Property import Property
import Solver import Solver
evaluateTerm :: Term -> ModelSI -> SInteger evaluateTerm :: Term -> ModelSI -> SInteger
evaluateTerm (Term xs) m = sum $ map evaluateLinAtom xs evaluateTerm (Term xs) m = sum $ map evaluateLinAtom xs
where evaluateLinAtom (Var c x) = literal c * m M.! x where evaluateLinAtom (Var c x) = literal c * mVal m x
evaluateLinAtom (Const c) = literal c evaluateLinAtom (Const c) = literal c
opToFunction :: Op -> SInteger -> SInteger -> SBool opToFunction :: Op -> SInteger -> SInteger -> SBool
......
...@@ -4,27 +4,11 @@ module Solver.SComponent ...@@ -4,27 +4,11 @@ module Solver.SComponent
where where
import Data.SBV import Data.SBV
import qualified Data.Map as M
import Data.List (partition) import Data.List (partition)
import PetriNet import PetriNet
import Solver import Solver
mElem :: ModelSI -> String -> SBool
mElem m x = (m M.! x) .== 1
mElemI :: ModelI -> String -> Bool
mElemI m x = (m M.! x) == 1
mNotElem :: ModelSI -> String -> SBool
mNotElem m x = (m M.! x) .== 0
mNotElemI :: ModelI -> String -> Bool
mNotElemI m x = (m M.! x) == 0
countElem :: ModelSI -> [String] -> SInteger
countElem m xs = sum $ map (m M.!) xs
prime :: String -> String prime :: String -> String
prime = ('\'':) prime = ('\'':)
...@@ -40,19 +24,19 @@ checkPrePostTransitions :: PetriNet -> ModelSI -> SBool ...@@ -40,19 +24,19 @@ checkPrePostTransitions :: PetriNet -> ModelSI -> SBool
checkPrePostTransitions net m = checkPrePostTransitions net m =
bAnd $ map checkPrePostTransition $ transitions net bAnd $ map checkPrePostTransition $ transitions net
where checkPrePostTransition t = where checkPrePostTransition t =
let incoming = countElem m $ pre net t let incoming = mElemSum m $ pre net t
outgoing = countElem m $ post net t outgoing = mElemSum m $ post net t
in mElem m t ==> incoming .== 1 &&& outgoing .== 1 in mElem m t ==> incoming .== 1 &&& outgoing .== 1
checkSubsetTransitions :: [String] -> ModelSI -> SBool checkSubsetTransitions :: [String] -> ModelSI -> SBool
checkSubsetTransitions fired m = checkSubsetTransitions fired m =
bAnd (map checkTransition fired) &&& bAnd (map checkTransition fired) &&&
countElem m (map prime fired) .< countElem m fired mElemSum m (map prime fired) .< mElemSum m fired
where checkTransition t = where checkTransition t =
mElem m (prime t) ==> mElem m t mElem m (prime t) ==> mElem m t
checkNotEmpty :: [String] -> ModelSI -> SBool checkNotEmpty :: [String] -> ModelSI -> SBool
checkNotEmpty fired m = countElem m (map prime fired) .> 0 checkNotEmpty fired m = mElemSum m (map prime fired) .> 0
checkClosed :: PetriNet -> ModelI -> ModelSI -> SBool checkClosed :: PetriNet -> ModelI -> ModelSI -> SBool
checkClosed net ax m = checkClosed net ax m =
...@@ -60,17 +44,17 @@ checkClosed net ax m = ...@@ -60,17 +44,17 @@ checkClosed net ax m =
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,
ax M.! t > 0 , ax M.! t' > 0 ]) cElem ax t, cElem ax t' ])
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')
checkTokens :: PetriNet -> ModelSI -> SBool checkTokens :: PetriNet -> ModelSI -> SBool
checkTokens net m = checkTokens net m =
sum (map addPlace (initials net)) .== 1 sum (map addPlace (initials net)) .== 1
where addPlace (p,x) = literal x * (m M.! p) where addPlace (p,x) = literal x * mVal m p
checkBinary :: ModelSI -> SBool checkBinary :: ModelSI -> SBool
checkBinary m = bAnd $ map (\x -> x .== 0 ||| x .== 1) $ M.elems m checkBinary m = bAnd $ map (\x -> x .== 0 ||| x .== 1) $ mValues m
checkSComponent :: PetriNet -> [String] -> ModelI -> ModelSI -> SBool checkSComponent :: PetriNet -> [String] -> ModelI -> ModelSI -> SBool
checkSComponent net fired ax m = checkSComponent net fired ax m =
...@@ -82,13 +66,12 @@ checkSComponent net fired ax m = ...@@ -82,13 +66,12 @@ checkSComponent net fired ax m =
checkTokens net m &&& checkTokens net m &&&
checkBinary m checkBinary m
checkSComponentSat :: PetriNet -> ModelI -> ([String], ModelSI -> SBool) checkSComponentSat :: PetriNet -> [String] -> ModelI -> ([String], ModelSI -> SBool)
checkSComponentSat net ax = checkSComponentSat net fired ax =
let fired = M.keys $ M.filter (> 0) ax (places net ++ transitions net ++ map prime fired,
in (places net ++ transitions net ++ map prime fired, checkSComponent net fired ax)
checkSComponent net fired ax)
getSComponentInOut :: PetriNet -> ModelI -> ModelI -> ([String], [String]) getSComponentInOut :: PetriNet -> ModelI -> ModelI -> ([String], [String])
getSComponentInOut net ax as = getSComponentInOut net ax as =
partition (mElemI ax) $ filter (mElemI as) (transitions net) partition (cElem ax) $ filter (cElem as) (transitions net)
...@@ -4,7 +4,6 @@ module Solver.StateEquation ...@@ -4,7 +4,6 @@ module Solver.StateEquation
where where
import Data.SBV import Data.SBV
import qualified Data.Map as M
import PetriNet import PetriNet
import Property import Property
...@@ -17,15 +16,15 @@ placeConstraints net m = bAnd $ map checkPlaceEquation $ places net ...@@ -17,15 +16,15 @@ placeConstraints net m = bAnd $ map checkPlaceEquation $ places net
let incoming = map addTransition $ lpre net p let incoming = map addTransition $ lpre net p
outgoing = map addTransition $ lpost net p outgoing = map addTransition $ lpost net p
pinit = literal $ initial net p pinit = literal $ initial net p
in pinit + sum incoming - sum outgoing .== (m M.! p) in pinit + sum incoming - sum outgoing .== mVal m p
addTransition (t,w) = literal w * (m M.! t) addTransition (t,w) = literal w * mVal m t
nonnegativityConstraints :: ModelSI -> SBool nonnegativityConstraints :: ModelSI -> SBool
nonnegativityConstraints m = bAnd $ map (.>= 0) $ M.elems m nonnegativityConstraints m = bAnd $ map (.>= 0) $ mValues m
checkTraps :: [[String]] -> ModelSI -> SBool checkTraps :: [[String]] -> ModelSI -> SBool
checkTraps traps m = bAnd $ map checkTrapDelta traps checkTraps traps m = bAnd $ map checkTrapDelta traps
where checkTrapDelta trap = sum (map (m M.!) trap) .>= 1 where checkTrapDelta trap = sum (map (mVal m) trap) .>= 1
checkStateEquation :: PetriNet -> Formula -> [[String]] -> ModelSI -> SBool checkStateEquation :: PetriNet -> Formula -> [[String]] -> ModelSI -> SBool
checkStateEquation net f traps m = checkStateEquation net f traps m =
...@@ -40,4 +39,4 @@ checkStateEquationSat net f traps = ...@@ -40,4 +39,4 @@ checkStateEquationSat net f traps =
(places net ++ transitions net, checkStateEquation net f traps) (places net ++ transitions net, checkStateEquation net f traps)
markedPlacesFromAssignment :: PetriNet -> ModelI -> [String] markedPlacesFromAssignment :: PetriNet -> ModelI -> [String]
markedPlacesFromAssignment net a = filter (( > 0) . (a M.!)) $ places net markedPlacesFromAssignment net a = filter (cElem a) $ places net
...@@ -4,7 +4,6 @@ module Solver.TransitionInvariant ...@@ -4,7 +4,6 @@ module Solver.TransitionInvariant
where where
import Data.SBV import Data.SBV
import qualified Data.Map as M
import PetriNet import PetriNet
import Property import Property
...@@ -18,19 +17,19 @@ tInvariantConstraints net m = ...@@ -18,19 +17,19 @@ tInvariantConstraints net m =
let incoming = map addTransition $ lpre net p let incoming = map addTransition $ lpre net p
outgoing = map addTransition $ lpost net p outgoing = map addTransition $ lpost net p
in sum incoming - sum outgoing .>= 0 in sum incoming - sum outgoing .>= 0
addTransition (t,w) = literal w * (m M.! t) addTransition (t,w) = literal w * mVal m t
finalInvariantConstraints :: ModelSI -> SBool finalInvariantConstraints :: ModelSI -> SBool
finalInvariantConstraints m = sum (M.elems m) .> 0 finalInvariantConstraints m = sum (mValues m) .> 0
nonnegativityConstraints :: ModelSI -> SBool nonnegativityConstraints :: ModelSI -> SBool
nonnegativityConstraints m = bAnd $ map (.>= 0) $ M.elems m nonnegativityConstraints m = bAnd $ map (.>= 0) $ mValues m
checkSComponentTransitions :: [([String],[String])] -> ModelSI -> SBool checkSComponentTransitions :: [([String],[String])] -> ModelSI -> SBool
checkSComponentTransitions strans m = bAnd $ map checkInOut strans checkSComponentTransitions strans m = bAnd $ map checkInOut strans
where checkInOut (sOut,sIn) = where checkInOut (sOut,sIn) =
bAnd (map (\t -> m M.! t .> 0) sOut) ==> bAnd (map (\t -> mVal m t .> 0) sOut) ==>
bOr (map (\t -> m M.! t .> 0) sIn) bOr (map (\t -> mVal m t .> 0) sIn)
checkTransitionInvariant :: PetriNet -> Formula -> [([String],[String])] -> checkTransitionInvariant :: PetriNet -> Formula -> [([String],[String])] ->
ModelSI -> SBool ModelSI -> SBool
...@@ -47,4 +46,4 @@ checkTransitionInvariantSat net f strans = ...@@ -47,4 +46,4 @@ checkTransitionInvariantSat net f strans =
(transitions net, checkTransitionInvariant net f strans) (transitions net, checkTransitionInvariant net f strans)
firedTransitionsFromAssignment :: ModelI -> [String] firedTransitionsFromAssignment :: ModelI -> [String]
firedTransitionsFromAssignment a = M.keys $ M.filter ( > 0) a firedTransitionsFromAssignment = mElemsWith (> 0)
...@@ -5,7 +5,6 @@ module Solver.TrapConstraints ...@@ -5,7 +5,6 @@ module Solver.TrapConstraints
where where
import Data.SBV import Data.SBV
import qualified Data.Map as M
import PetriNet import PetriNet
import Solver import Solver
...@@ -14,15 +13,15 @@ trapConstraints :: PetriNet -> ModelSB -> SBool ...@@ -14,15 +13,15 @@ trapConstraints :: PetriNet -> ModelSB -> SBool
trapConstraints net m = trapConstraints net m =
bAnd $ map trapConstraint $ transitions net bAnd $ map trapConstraint $ transitions net
where trapConstraint t = where trapConstraint t =
bOr (map (m M.!) $ pre net t) ==> bOr (map (m M.!) $ post net t) bOr (map (mElem m) $ pre net t) ==> bOr (map (mElem m) $ post net t)
trapInitiallyMarked :: PetriNet -> ModelSB -> SBool trapInitiallyMarked :: PetriNet -> ModelSB -> SBool
trapInitiallyMarked net m = trapInitiallyMarked net m =
let marked = map fst $ filter (( > 0) . snd) $ initials net let marked = map fst $ filter (( > 0) . snd) $ initials net
in bOr $ map (m M.!) marked in bOr $ map (mElem m) marked
trapUnassigned :: [String] -> ModelSB -> SBool trapUnassigned :: [String] -> ModelSB -> SBool
trapUnassigned assigned m = bAnd $ map (bnot . (m M.!)) assigned trapUnassigned assigned m = bAnd $ map (mNotElem m) assigned
checkTrap :: PetriNet -> [String] -> ModelSB -> SBool checkTrap :: PetriNet -> [String] -> ModelSB -> SBool
checkTrap net assigned m = checkTrap net assigned m =
...@@ -35,5 +34,5 @@ checkTrapSat net assigned = ...@@ -35,5 +34,5 @@ checkTrapSat net assigned =
(places net, checkTrap net assigned) (places net, checkTrap net assigned)
trapFromAssignment :: ModelB -> [String] trapFromAssignment :: ModelB -> [String]
trapFromAssignment a = M.keys $ M.filter id a trapFromAssignment = mElemsWith id
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