Notice to GitKraken users: A vulnerability has been found in the SSH key generation of GitKraken versions 7.6.0 to 8.0.0 (https://www.gitkraken.com/blog/weak-ssh-key-fix). If you use GitKraken and have generated a SSH key using one of these versions, please remove it both from your local workstation and from your LRZ GitLab profile.

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

Commit 6bcaca38 authored by Philipp Meyer's avatar Philipp Meyer
Browse files

Testing weaker refinement constraints

parent 325db648
......@@ -360,7 +360,7 @@ findLivenessRefinementByEmptyTraps net m x traps = do
rm <- refineSafetyProperty net FTrue traps m
case rm of
(Nothing, _) -> do
cut <- generateLivenessRefinement net traps
cut <- generateLivenessRefinement net x traps
return $ Just cut
(Just _, _) ->
return Nothing
......@@ -370,14 +370,14 @@ findLivenessRefinementByEmptyTraps net m x traps = do
checkSafetyProperty' net FTrue traps'
case rm of
(Nothing, _) -> do
cut <- generateLivenessRefinement net traps'
cut <- generateLivenessRefinement net x traps'
return $ Just cut
(Just m', _) ->
findLivenessRefinementByEmptyTraps net m' x traps'
generateLivenessRefinement :: PetriNet -> [Trap] -> OptIO Cut
generateLivenessRefinement net traps = do
let cut = constructCut net traps
generateLivenessRefinement :: PetriNet -> FiringVector -> [Trap] -> OptIO Cut
generateLivenessRefinement net x traps = do
let cut = constructCut net x traps
verbosePut 3 $ "- cut: " ++ show cut
return cut
......
......@@ -99,12 +99,18 @@ instance Show PetriNet where
show l ++ " -> " ++ show s ++ " -> " ++ show r
-- TODO: better cuts, scc, min cut?
constructCut:: PetriNet -> [Trap] -> Cut
constructCut net traps = (trapComponents, trapOutputs)
{-
constructCut:: PetriNet -> FiringVector -> [Trap] -> Cut
constructCut net _ traps = (trapComponents, trapOutputs)
where trapComponent trap = (sort trap, sort (mpre net trap) \\ trapOutputs)
trapComponents = listSet $ map trapComponent traps
trapOutput trap = mpost net trap \\ mpre net trap
trapOutputs = listSet $ concatMap trapOutput traps
-}
constructCut:: PetriNet -> FiringVector -> [Trap] -> Cut
constructCut net x _ = (map (\t -> ([],[t])) tPositive, tNegative)
where tPositive = elems x
tNegative = transitions net \\ tPositive
renamePlace :: (String -> String) -> Place -> Place
renamePlace f (Place p) = Place (f p)
......
......@@ -101,5 +101,5 @@ cutFromAssignment net x p' t' y =
s1 = filter (\p -> val p' p > 0) $ mpre net t1
s2 = filter (\p -> val p' p > 0) $ mpre net t2
size = fromIntegral $ M.size $ M.filter (> 0) p'
in (constructCut net [s1,s2], size)
in (constructCut net x [s1,s2], size)
module Solver.TransitionInvariant
(checkTransitionInvariantSat
,checkTransitionInvariant
,tInvariantConstraints
,nonnegativityConstraints)
(checkTransitionInvariantSat)
where
import Data.SBV
......@@ -35,16 +32,12 @@ checkCuts cuts x = bAnd $ map checkCut cuts
cPost = map (positiveVal x) u
in bAnd cPre ==> bOr cPost
checkTransitionInvariant :: PetriNet -> SIMap Transition -> SBool
checkTransitionInvariant net x =
checkTransitionInvariant :: PetriNet -> Formula Transition ->
[Cut] -> SIMap Transition -> SBool
checkTransitionInvariant net f cuts x =
tInvariantConstraints net x &&&
nonnegativityConstraints x &&&
finalInvariantConstraints x
checkTransitionInvariantMethod :: PetriNet -> Formula Transition ->
[Cut] -> SIMap Transition -> SBool
checkTransitionInvariantMethod net f cuts x =
checkTransitionInvariant net x &&&
finalInvariantConstraints x &&&
checkCuts cuts x &&&
evaluateFormula f x
......@@ -54,7 +47,7 @@ checkTransitionInvariantSat net f cuts =
let x = makeVarMap $ transitions net
in ("transition invariant constraints", "transition invariant",
getNames x,
\fm -> checkTransitionInvariantMethod net f cuts (fmap fm x),
\fm -> checkTransitionInvariant net f cuts (fmap fm x),
\fm -> firingVectorFromAssignment (fmap fm x))
firingVectorFromAssignment :: IMap Transition -> FiringVector
......
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