Commit 920b4175 authored by Philipp J. Meyer's avatar Philipp J. Meyer
Browse files

optimized generation of triplets

parent 3cc44ea2
......@@ -530,20 +530,7 @@ refineNonConsensusTerminalMarkingProperty net traps siphons c@(m0, m, x) = do
checkTerminalMarkingReachableProperty :: PetriNet -> OptIO PropResult
checkTerminalMarkingReachableProperty net = do
let triplets = generateTriplets net
let trivialTriplets = filter trivialTriplet triplets
let nonTrivialTriplets = filter (not . trivialTriplet) triplets
let emptyTriplets = filter emptyTriplet triplets
let nonTrivialNonEmptyTriplets = filter (not . emptyTriplet) nonTrivialTriplets
-- 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
let nonTrivialTriplets = filter (not . trivialTriplet) $ generateTriplets net
checkTerminalMarkingReachableProperty' net nonTrivialTriplets 1 $ genericLength $ transitions net
checkTerminalMarkingReachableProperty' :: PetriNet -> [Triplet] -> Integer -> Integer -> OptIO PropResult
......
......@@ -10,7 +10,6 @@ import qualified Data.Map as M
type Triplet = (Transition, Transition, [Transition])
-- TODO: optimize
generateTriplets :: PetriNet -> [Triplet]
generateTriplets net =
let
......@@ -27,7 +26,7 @@ generateTriplets net =
(tPre, tPost) = prePostMultisets M.! t
stSet = M.unionWith (+) sPre (M.differenceWith multiSetDifference tPre sPost)
in
[t' | t' <- transitions net, t' /= s, checkTriple stSet t']
[t' | t' <- mpost net (M.keys stSet), t' /= s, checkTriple stSet t']
checkTriple stMultiset t' =
let
(tPre, _) = prePostMultisets M.! t'
......@@ -35,7 +34,7 @@ generateTriplets net =
in
M.null differenceMultiset
in
[(s, t, findT' s t) | s <- transitions net, t <- transitions net, s /= t]
[(s, t, findT' s t) | s <- transitions net, t <- mpost net (post net s), s /= t]
trivialTriplet :: Triplet -> Bool
trivialTriplet (_, t, ts) = elem t ts
......
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