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

Commit 0bbb82c8 authored by Philipp J. Meyer's avatar Philipp J. Meyer
Browse files

working constraints for terminal marking reachable

parent ae3faf35
......@@ -5,7 +5,7 @@ import System.IO
import Control.Monad
import Control.Concurrent.ParallelIO
import Control.Arrow (first)
import Data.List (partition,minimumBy)
import Data.List (partition,minimumBy,genericLength)
import Data.Ord (comparing)
import Data.Maybe
import qualified Data.ByteString.Lazy as L
......@@ -535,18 +535,27 @@ checkTerminalMarkingReachableProperty net = do
let nonTrivialTriplets = filter (not . trivialTriplet) triplets
let emptyTriplets = filter emptyTriplet triplets
let nonTrivialNonEmptyTriplets = filter (not . emptyTriplet) nonTrivialTriplets
liftIO $ putStrLn $ "All triplets (" ++ show (length triplets) ++ "):"
liftIO $ putStrLn $ unlines $ map show triplets
liftIO $ putStrLn $ "Trivial triplets (" ++ show (length trivialTriplets) ++ "):"
liftIO $ putStrLn $ unlines $ map show trivialTriplets
liftIO $ putStrLn $ "Empty triplets (" ++ show (length emptyTriplets) ++ "):"
liftIO $ putStrLn $ unlines $ map show emptyTriplets
liftIO $ putStrLn $ "Non-trivial, non-empty triplets (" ++ show (length nonTrivialNonEmptyTriplets) ++ "):"
liftIO $ putStrLn $ unlines $ map show nonTrivialNonEmptyTriplets
return Satisfied
r <- checkSat $ checkTerminalMarkingReachableSat net nonTrivialTriplets 2
-- TODO optimize triplet computation
-- liftIO $ putStrLn $ "All triplets (" ++ show (length triplets) ++ "):"
-- liftIO $ putStrLn $ unlines $ map show triplets
-- liftIO $ putStrLn $ "Trivial triplets (" ++ show (length trivialTriplets) ++ "):"
-- liftIO $ putStrLn $ unlines $ map show trivialTriplets
-- liftIO $ putStrLn $ "Empty triplets (" ++ show (length emptyTriplets) ++ "):"
-- liftIO $ putStrLn $ unlines $ map show emptyTriplets
-- liftIO $ putStrLn $ "Non-trivial, non-empty triplets (" ++ show (length nonTrivialNonEmptyTriplets) ++ "):"
-- liftIO $ putStrLn $ unlines $ map show nonTrivialNonEmptyTriplets
checkTerminalMarkingReachableProperty' net nonTrivialTriplets 1 $ genericLength $ transitions net
checkTerminalMarkingReachableProperty' :: PetriNet -> [Triplet] -> Integer -> Integer -> OptIO PropResult
checkTerminalMarkingReachableProperty' net triplets k kmax = do
verbosePut 1 $ "Checking terminal marking reachable with at most " ++ show k ++ " partitions"
r <- checkSat $ checkTerminalMarkingReachableSat net triplets k
case r of
Nothing -> return Unknown
Nothing ->
if k < kmax then
checkTerminalMarkingReachableProperty' net triplets (k + 1) kmax
else
return Unknown
Just inv -> do
invariant <- opt optInvariant
if invariant then
......
......@@ -6,7 +6,7 @@ module Solver.TerminalMarkingReachable
where
import Data.SBV
import Data.List (intercalate)
import Data.List (intercalate,genericReplicate)
import qualified Data.Map as M
import Util
......@@ -17,36 +17,65 @@ import StructuralComputation
type TerminalMarkingReachableInvariant = [BlockInvariant]
data BlockInvariant =
BlockInvariant (Int, [Transition], IVector Place)
BlockInvariant (Integer, [Transition], IVector Place)
instance Invariant BlockInvariant where
invariantSize (BlockInvariant (_, _, yi)) = size yi
invariantSize (BlockInvariant (_, ti, yi)) = if null ti then 0 else size yi
instance Show BlockInvariant where
show (BlockInvariant (i, ti, yi)) =
"T_" ++ show i ++ ": " ++ show ti ++ "; " ++ intercalate " + " (map showWeighted (items yi))
"T_" ++ show i ++ ": " ++ show ti ++
(if null ti then "" else " => " ++ intercalate " + " (map showWeighted (items yi)))
nonNegativityConstraints :: (Ord a, Show a) => SIMap a -> SBool
nonNegativityConstraints m =
bAnd $ map checkVal $ vals m
where checkVal x = x .>= 0
checkTerminalMarkingReachable :: PetriNet -> [Triplet] -> Int -> [SIMap Place] -> SIMap Transition -> SBool
checkTerminalMarkingReachable net triplets k ys b =
bAnd (map nonNegativityConstraints ys)
-- farkas lemma constraints
-- triplet constraints
-- block constraints
checkNonNegativityConstraints :: (Ord a, Show a) => [SIMap a] -> SBool
checkNonNegativityConstraints xs =
bAnd $ map nonNegativityConstraints xs
checkTerminalMarkingReachableSat :: PetriNet -> [Triplet] -> Int -> ConstraintProblem Integer TerminalMarkingReachableInvariant
blockTerminationConstraints :: PetriNet -> Integer -> SIMap Transition -> SIMap Place -> SBool
blockTerminationConstraints net i b y =
bAnd $ map checkTransition $ transitions net
where checkTransition t =
let incoming = map addPlace $ lpre net t
outgoing = map addPlace $ lpost net t
in (val b t .== literal i) ==> (sum outgoing - sum incoming .< 0)
addPlace (p, w) = literal w * val y p
terminationConstraints :: PetriNet -> Integer -> SIMap Transition -> [SIMap Place] -> SBool
terminationConstraints net k b ys =
bAnd $ [blockTerminationConstraints net i b y | (i,y) <- zip [1..] ys]
blockConstraints :: PetriNet -> Integer -> SIMap Transition -> SBool
blockConstraints net k b =
bAnd $ map checkBlock $ transitions net
where checkBlock t = literal 1 .<= val b t &&& val b t .<= literal k
blockOrderConstraints :: PetriNet -> [Triplet] -> Integer -> SIMap Transition -> SBool
blockOrderConstraints net triplets k b =
bAnd $ map checkTriplet triplets
where checkTriplet (s,t,ts) = (val b s .> val b t) ==> bOr (map (\t' -> val b t' .== val b t) ts)
checkTerminalMarkingReachable :: PetriNet -> [Triplet] -> Integer -> SIMap Transition -> [SIMap Place] -> SBool
checkTerminalMarkingReachable net triplets k b ys =
blockConstraints net k b &&&
terminationConstraints net k b ys &&&
blockOrderConstraints net triplets k b &&&
checkNonNegativityConstraints ys
checkTerminalMarkingReachableSat :: PetriNet -> [Triplet] -> Integer -> ConstraintProblem Integer TerminalMarkingReachableInvariant
checkTerminalMarkingReachableSat net triplets k =
let makeYName i = (++) (replicate i '\'')
let makeYName i = (++) (genericReplicate i '\'')
ys = [makeVarMapWith (makeYName i) $ places net | i <- [1..k]]
b = makeVarMap $ transitions net
in ("terminal marking reachable", "invariant",
concat (map getNames ys) ++ getNames b,
\fm -> checkTerminalMarkingReachable net triplets k (map (fmap fm) ys) (fmap fm b),
\fm -> invariantFromAssignment (map (fmap fm) ys) (fmap fm b))
\fm -> checkTerminalMarkingReachable net triplets k (fmap fm b) (map (fmap fm) ys),
\fm -> invariantFromAssignment net k (fmap fm b) (map (fmap fm) ys))
invariantFromAssignment :: [IMap Place] -> IMap Transition -> TerminalMarkingReachableInvariant
invariantFromAssignment ys b = [BlockInvariant (1, [], buildVector [])]
invariantFromAssignment :: PetriNet -> Integer -> IMap Transition -> [IMap Place] -> TerminalMarkingReachableInvariant
invariantFromAssignment net k b ys =
[BlockInvariant (i, M.keys (M.filter (== i) b), makeVector y) | (i,y) <- zip [1..] ys]
......@@ -10,6 +10,7 @@ import qualified Data.Map as M
type Triplet = (Transition, Transition, [Transition])
-- TODO: optimize
generateTriplets :: PetriNet -> [Triplet]
generateTriplets net =
let
......
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