21.10.2021, 9:00 - 11:00: Due to updates GitLab may be unavailable for some minutes between 09:00 and 11:00.

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

Moved map definitons and functions to util

parent de472ac8
......@@ -516,7 +516,9 @@ checkLivenessProperty' verbosity net refine f cuts = do
findLivenessRefinement :: Int -> PetriNet -> FiringVector ->
IO (Maybe Cut)
findLivenessRefinement verbosity net x = do
r1 <- findLivenessRefinementBySComponent verbosity net x
r1 <- findLivenessRefinementByEmptyTraps verbosity net
(initialMarking net) x []
--r1 <- findLivenessRefinementBySComponent verbosity net x
case r1 of
Nothing -> findLivenessRefinementByEmptyTraps verbosity net
(initialMarking net) x []
......@@ -535,24 +537,27 @@ findLivenessRefinementByEmptyTraps verbosity net m x traps = do
Nothing -> do
rm <- refineSafetyProperty verbosity net FTrue traps m
case rm of
(Nothing, _) ->
return $ Just $ generateLivenessRefinement
net x traps
(Nothing, _) -> do
cut <- generateLivenessRefinement verbosity net x traps
return $ Just cut
(Just _, _) ->
return Nothing
Just trap -> do
rm <- checkSafetyProperty' verbosity net False FTrue (trap:traps)
case rm of
(Nothing, _) ->
return $ Just $ generateLivenessRefinement
net x (trap:traps)
(Nothing, _) -> do
cut <- generateLivenessRefinement verbosity net x traps
return $ Just cut
(Just m', _) ->
findLivenessRefinementByEmptyTraps verbosity net m' x (trap:traps)
generateLivenessRefinement :: PetriNet -> FiringVector -> [Trap] -> Cut
generateLivenessRefinement net x traps =
(map (filter (\t -> value x t > 0) . mpre net) traps,
nubOrd (concatMap (filter (\t -> value x t == 0) . mpost net) traps))
generateLivenessRefinement :: Int -> PetriNet -> FiringVector -> [Trap] -> IO Cut
generateLivenessRefinement verbosity net x traps = do
let ts = map (filter (\t -> val x t > 0) . mpre net) traps
let u = nubOrd (concatMap (filter (\t -> val x t == 0) . mpost net) traps)
let cut = (ts,u)
verbosePut verbosity 3 $ "- cut: " ++ show cut
return cut
checkStructuralProperty :: Int -> PetriNet -> Structure -> IO PropResult
checkStructuralProperty _ net struct =
......
......@@ -67,7 +67,7 @@ data PetriNet = PetriNet {
}
initial :: PetriNet -> Place -> Integer
initial net = value (initialMarking net)
initial net = val (initialMarking net)
initials :: PetriNet -> [Place]
initials = elems . initialMarking
......@@ -108,7 +108,7 @@ renamePetriNetPlacesAndTransitions f net =
adjacencyP net,
adjacencyT = mapAdjacency (renameTransition f) (renamePlace f) $
adjacencyT net,
initialMarking = vmap (renamePlace f) $ initialMarking net,
initialMarking = emap (renamePlace f) $ initialMarking net,
ghostTransitions = map (renameTransition f) $ ghostTransitions net
}
where mapAdjacency f g m = M.mapKeys f (M.map (mapContext g) m)
......
{-# LANGUAGE TypeSynonymInstances, FlexibleInstances #-}
module Solver
(prime,checkSat,ModelReader,val,vals,positiveVal,zeroVal,
sumVal, getNames,makeVarMap,makeVarMapWith,mval,
IntConstraint,BoolConstraint,IntResult,BoolResult,
Model,ConstraintProblem,
SIMap,SBMap,IMap,BMap,VarMap)
(prime,checkSat,val,vals,positiveVal,zeroVal,
getNames,
ConstraintProblem)
where
import Data.SBV
import qualified Data.Map as M
import Control.Monad.Reader
import Util
type Model a = M.Map String a
type VarMap a = M.Map a String
type SIMap a = M.Map a SInteger
type SBMap a = M.Map a SBool
type IMap a = M.Map a Integer
type BMap a = M.Map a Bool
getNames :: VarMap a -> [String]
getNames = M.elems
type ModelReader a b = Reader (Model a) b
type IntConstraint = ModelReader SInteger SBool
type BoolConstraint = ModelReader SBool SBool
type IntResult a = ModelReader Integer a
type BoolResult a = ModelReader Bool a
type ConstraintProblem a b =
(String, String, [String], (String -> SBV a) -> SBool, (String -> a) -> b)
val :: (Ord a) => M.Map a b -> a -> b
val = (M.!)
mval :: (Ord a) => M.Map a b -> [a] -> [b]
mval = map . val
zeroVal :: (Ord a) => M.Map a SInteger -> a -> SBool
zeroVal m x = val m x .== 0
positiveVal :: (Ord a) => M.Map a SInteger -> a -> SBool
positiveVal m x = val m x .> 0
sumVal :: (Ord a, Num b) => M.Map a b -> b
sumVal = sum . vals
vals :: (Ord a) => M.Map a b -> [b]
vals = M.elems
makeVarMap :: (Show a, Ord a) => [a] -> VarMap a
makeVarMap = makeVarMapWith id
makeVarMapWith :: (Show a, Ord a) => (String -> String) -> [a] -> VarMap a
makeVarMapWith f xs = M.fromList $ xs `zip` map (f . show) xs
rebuildModel :: SymWord a => [String] -> Either String (Bool, [a]) ->
Maybe (Model a)
rebuildModel _ (Left _) = Nothing
......
......@@ -4,8 +4,8 @@ where
import Data.SBV
import Util
import Property
import Solver
evaluateTerm :: (Ord a) => Term a -> SIMap a -> SInteger
evaluateTerm (Var x) m = val m x
......
......@@ -48,7 +48,7 @@ checkClosed net x p' y =
let pVal = positiveVal p' p
postVal = bAnd $ map checkTransition
[(t,t') | t <- pre net p, t' <- post net p,
value x t > 0, value x t' > 0 ]
val x t > 0, val x t' > 0 ]
in pVal ==> postVal
checkTransition (t,t') = positiveVal y t ==> positiveVal y t'
......@@ -91,7 +91,7 @@ checkSComponentSat net x =
-- TODO: use strongly connected components and min cuts
cutFromAssignment :: FiringVector -> IMap Transition -> IMap Transition -> Cut
cutFromAssignment x t' y =
let (ts, u) = partition (\t -> value x t > 0) $ M.keys $ M.filter (> 0) t'
let (ts, u) = partition (\t -> val x t > 0) $ M.keys $ M.filter (> 0) t'
(t1, t2) = partition (\t -> val y t > 0) ts
in ([t1,t2], u)
......@@ -13,7 +13,7 @@ subnetTrapConstraints :: PetriNet -> Marking -> FiringVector ->
SBMap Place -> SBool
subnetTrapConstraints net m x b =
bAnd $ map trapConstraint $ elems x
where placeConstraints = mval b . filter (\p -> value m p == 0)
where placeConstraints = mval b . filter (\p -> val m p == 0)
trapConstraint t =
bOr (placeConstraints (pre net t)) ==>
bOr (placeConstraints (post net t))
......@@ -30,7 +30,7 @@ checkSubnetEmptyTrap net m x b =
checkSubnetEmptyTrapSat :: PetriNet -> Marking -> FiringVector ->
ConstraintProblem Bool Trap
checkSubnetEmptyTrapSat net m x =
let b = makeVarMap $ filter (\p -> value m p == 0) $ mpost net $ elems x
let b = makeVarMap $ filter (\p -> val m p == 0) $ mpost net $ elems x
in ("subnet empty trap constraints", "trap",
getNames b,
\fm -> checkSubnetEmptyTrap net m x (fmap fm b),
......
module Util
(verbosePut,Vector,value,elems,items,buildVector,makeVector,vmap,
nubOrd,nubOrdBy,prime)
(verbosePut,elems,items,emap,
nubOrd,nubOrdBy,prime,val,vals,mval,zeroVal,positiveVal,sumVal,
makeVarMap,makeVarMapWith,buildVector,makeVector,getNames,
Vector,Model,VarMap,SIMap,SBMap,IMap,BMap)
where
import Data.SBV
import qualified Data.Map as M
import Control.Monad
import Data.List
import Data.Ord
import Data.Function
verbosePut :: Int -> Int -> String -> IO ()
verbosePut verbosity level str =
when (verbosity >= level) (putStrLn str)
{-
- Various maps and functions on them
-}
prime :: String -> String
prime = ('\'':)
type Vector a = M.Map a Integer
type Model a = M.Map String a
type VarMap a = M.Map a String
type SIMap a = M.Map a SInteger
type SBMap a = M.Map a SBool
type IMap a = M.Map a Integer
type BMap a = M.Map a Bool
val :: (Ord a) => M.Map a b -> a -> b
val = (M.!)
mval :: (Ord a) => M.Map a b -> [a] -> [b]
mval = map . val
zeroVal :: (Ord a) => M.Map a SInteger -> a -> SBool
zeroVal m x = val m x .== 0
positiveVal :: (Ord a) => M.Map a SInteger -> a -> SBool
positiveVal m x = val m x .> 0
sumVal :: (Ord a, Num b) => M.Map a b -> b
sumVal = sum . vals
newtype Vector a = Vector { getVector :: M.Map a Integer }
vals :: (Ord a) => M.Map a b -> [b]
vals = M.elems
instance (Show a) => Show (Vector a) where
show (Vector v) =
"[" ++ intercalate "," (map showEntry (M.toList v)) ++ "]"
where showEntry (i,x) =
show i ++ (if x /= 1 then "(" ++ show x ++ ")" else "")
elems :: (Ord a) => M.Map a b -> [a]
elems = M.keys
vmap :: (Ord a, Ord b) => (a -> b) -> Vector a -> Vector b
vmap f (Vector m) = Vector $ M.mapKeys f m
items :: M.Map a b -> [(a,b)]
items = M.toList
value :: (Ord a) => Vector a -> a -> Integer
value v x = M.findWithDefault 0 x (getVector v)
makeVarMap :: (Show a, Ord a) => [a] -> VarMap a
makeVarMap = makeVarMapWith id
elems :: (Ord a) => Vector a -> [a]
elems = M.keys . getVector
makeVarMapWith :: (Show a, Ord a) => (String -> String) -> [a] -> VarMap a
makeVarMapWith f xs = M.fromList $ xs `zip` map (f . show) xs
items :: Vector a -> [(a,Integer)]
items = M.toList . getVector
getNames :: VarMap a -> [String]
getNames = M.elems
--instance (Show a) => Show (Vector a) where
-- show (Vector v) =
-- "[" ++ intercalate "," (map showEntry (M.toList v)) ++ "]"
-- where showEntry (i,x) =
-- show i ++ (if x /= 1 then "(" ++ show x ++ ")" else "")
emap :: (Ord a, Ord b) => (a -> b) -> M.Map a c -> M.Map b c
emap = M.mapKeys
buildVector :: (Ord a) => [(a, Integer)] -> Vector a
buildVector = makeVector . M.fromList
buildVector = M.fromList
makeVector :: (Ord a) => M.Map a Integer -> Vector a
makeVector = Vector . M.filter (/=0)
makeVector = M.filter (/=0)
{-
- List functions
-}
nubOrd :: (Ord a) => [a] -> [a]
nubOrd = nubOrdBy id
......@@ -48,5 +82,15 @@ nubOrd = nubOrdBy id
nubOrdBy :: (Ord b) => (a -> b) -> [a] -> [a]
nubOrdBy f = map head . groupBy ((==) `on` f) . sortBy (comparing f)
{-
- TODO: IO wrapper with options
-}
verbosePut :: Int -> Int -> String -> IO ()
verbosePut verbosity level str =
when (verbosity >= level) (putStrLn str)
prime :: String -> String
prime = ('\'':)
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