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 7b966440 authored by Philipp Meyer's avatar Philipp Meyer
Browse files

Adding formula after simplification

parent 159de6f5
......@@ -9,6 +9,7 @@ import Data.List (partition)
import Data.Maybe
import qualified Data.ByteString.Lazy as L
import Control.Monad.Reader
import qualified Data.Set as S
import Util
import Options
......@@ -291,7 +292,7 @@ getLivenessInvariant :: PetriNet -> Formula Transition -> [Cut] -> OptIO (Maybe
getLivenessInvariant net f cuts = do
dnfCuts <- generateCuts net f cuts
verbosePut 2 $ "Number of disjuncts: " ++ show (length dnfCuts)
rs <- mapM (checkSat . checkLivenessInvariantSat net) dnfCuts
rs <- parallelIO (map (checkSat . checkLivenessInvariantSat net f) dnfCuts)
let added = map (Just . cutToLivenessInvariant) cuts
return $ sequence (rs ++ added)
......
......@@ -13,6 +13,7 @@ import qualified Data.Set as S
import Util
import Solver
import Solver.Simplifier
import Property
import PetriNet
data LivenessInvariant =
......@@ -82,9 +83,12 @@ checkLivenessInvariant net (comp0, comps) m =
addComp (n, _) = val m n
checkNonNegativity x = val m x .>= 0
checkLivenessInvariantSat :: PetriNet -> SimpleCut -> ConstraintProblem Integer LivenessInvariant
checkLivenessInvariantSat net cut =
let namedCut = nameCut cut
checkLivenessInvariantSat :: PetriNet -> Formula Transition -> SimpleCut -> ConstraintProblem Integer LivenessInvariant
checkLivenessInvariantSat net f (c0, cs) =
-- TODO: use own variables for formula cut
let (f0, fs) = formulaToCut f
cut = (c0 `S.union` f0, simplifyPositiveCut (cs ++ fs))
namedCut = nameCut cut
names = cutNames net namedCut
myVarMap fvm = M.fromList $ names `zip` fmap fvm names
in ("liveness invariant constraints", "liveness invariant",
......
......@@ -3,6 +3,8 @@ module Solver.Simplifier (
,SimpleCut
,generateCuts
,greedySimplify
,formulaToCut
,simplifyPositiveCut
) where
import Data.SBV
......@@ -53,7 +55,7 @@ checkSubsumptionSat c0 cs =
cutTransitions :: SimpleCut -> S.Set Transition
cutTransitions (c0, cs) = S.unions (c0:cs)
type SimpConfig = ([[SimpleCut] -> OptIO [SimpleCut]], SimpleCut, SimpleCut, Int)
type SimpConfig = ([[SimpleCut] -> OptIO [SimpleCut]], SimpleCut, Int)
simpWithoutFormula :: PetriNet -> Formula Transition -> SimpConfig
simpWithoutFormula net f =
......@@ -65,7 +67,6 @@ simpWithoutFormula net f =
, simplifyBySubsumption
]
, (S.empty, [])
, second (S.fromList (transitions net) :) (formulaToCut f)
, 2
)
......@@ -80,20 +81,18 @@ simpWithFormula net f =
, simplifyBySubsumption
]
, second (S.fromList (transitions net) :) (formulaToCut f)
, (S.empty, [])
, 2
)
applySimpConfig :: SimpConfig -> [Cut] -> OptIO [SimpleCut]
applySimpConfig (simpFunctions, initialCut, afterCut, otfIndex) cuts = do
applySimpConfig (simpFunctions, initialCut, otfIndex) cuts = do
simp <- opt optSimpFormula
let (otfSimps, afterSimps) = splitAt otfIndex $ take simp simpFunctions
let simpFunction = foldl (>=>) return afterSimps
let otfFunction = foldl (>=>) return otfSimps
let cnfCuts = map cutToSimpleDNFCuts cuts
dnfCuts <- foldM (combine otfFunction) [initialCut] cnfCuts
simpCuts <- simpFunction dnfCuts
combine otfFunction [afterCut] simpCuts
simpFunction dnfCuts
where
combine simpFunction cs1 cs2 =
simpFunction [ (c1c0 `S.union` c2c0, c1cs ++ c2cs)
......
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