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

Commit 341129ab authored by Philipp Meyer's avatar Philipp Meyer
Browse files

Added option to check if net might have parallel execution

parent a7aacd19
...@@ -22,6 +22,7 @@ import Printer ...@@ -22,6 +22,7 @@ import Printer
import qualified Printer.LOLA as LOLAPrinter import qualified Printer.LOLA as LOLAPrinter
import qualified Printer.SARA as SARAPrinter import qualified Printer.SARA as SARAPrinter
import qualified Printer.SPEC as SPECPrinter import qualified Printer.SPEC as SPECPrinter
import qualified Printer.DOT as DOTPrinter
import Property import Property
import Structure import Structure
import Solver import Solver
...@@ -40,6 +41,8 @@ data ImplicitProperty = Termination ...@@ -40,6 +41,8 @@ data ImplicitProperty = Termination
| ProperTermination | ProperTermination
| Safe | Bounded Integer | Safe | Bounded Integer
| StructFreeChoice | StructFreeChoice
| StructParallel
| StructFinalPlace
deriving (Show,Read) deriving (Show,Read)
data Options = Options { inputFormat :: InputFormat data Options = Options { inputFormat :: InputFormat
...@@ -147,6 +150,18 @@ options = ...@@ -147,6 +150,18 @@ options =
})) }))
"Prove that the net is free-choice" "Prove that the net is free-choice"
, Option "" ["parallel"]
(NoArg (\opt -> Right opt {
optProperties = StructParallel : optProperties opt
}))
"Prove that the net has non-trivial parallellism"
, Option "" ["final-place"]
(NoArg (\opt -> Right opt {
optProperties = StructFinalPlace : optProperties opt
}))
"Prove that there is only one needed final place"
, Option "n" ["no-refinement"] , Option "n" ["no-refinement"]
(NoArg (\opt -> Right opt { optRefine = False })) (NoArg (\opt -> Right opt { optRefine = False }))
"Don't use refinement" "Don't use refinement"
...@@ -197,16 +212,17 @@ writeFiles :: Int -> String -> PetriNet -> [Property] -> IO () ...@@ -197,16 +212,17 @@ writeFiles :: Int -> String -> PetriNet -> [Property] -> IO ()
writeFiles verbosity basename net props = do writeFiles verbosity basename net props = do
-- TODO: add options for different outputs -- TODO: add options for different outputs
verbosePut verbosity 1 $ "Writing " ++ showNetName net ++ " to " ++ basename verbosePut verbosity 1 $ "Writing " ++ showNetName net ++ " to " ++ basename
L.writeFile basename $ LOLAPrinter.printNet net L.writeFile basename $ DOTPrinter.printNet net
mapM_ (\(p,i) -> do --L.writeFile basename $ LOLAPrinter.printNet net
let file = basename ++ ".task" ++ show i --mapM_ (\(p,i) -> do
verbosePut verbosity 1 $ "Writing " ++ showPropertyName p ++ -- let file = basename ++ ".task" ++ show i
" to " ++ file -- verbosePut verbosity 1 $ "Writing " ++ showPropertyName p ++
L.writeFile file $ LOLAPrinter.printProperty p -- " to " ++ file
) (zip props [(1::Integer)..]) -- L.writeFile file $ LOLAPrinter.printProperty p
verbosePut verbosity 1 $ "Writing properties to " ++ basename ++ ".sara" -- ) (zip props [(1::Integer)..])
L.writeFile (basename ++ ".sara") $ --verbosePut verbosity 1 $ "Writing properties to " ++ basename ++ ".sara"
SARAPrinter.printProperties basename net props --L.writeFile (basename ++ ".sara") $
-- SARAPrinter.printProperties basename net props
--mapM_ (\(p,i) -> do --mapM_ (\(p,i) -> do
-- let file = basename ++ ".target" ++ show i -- let file = basename ++ ".target" ++ show i
-- verbosePut verbosity 1 $ "Writing " ++ showPropertyName p ++ -- verbosePut verbosity 1 $ "Writing " ++ showPropertyName p ++
...@@ -334,6 +350,10 @@ makeImplicitProperty net Safe = ...@@ -334,6 +350,10 @@ makeImplicitProperty net Safe =
in Property "safe" $ pcont bounded in Property "safe" $ pcont bounded
makeImplicitProperty _ StructFreeChoice = makeImplicitProperty _ StructFreeChoice =
Property "free choice" $ Structural FreeChoice Property "free choice" $ Structural FreeChoice
makeImplicitProperty _ StructParallel =
Property "parallel" $ Structural Parallel
makeImplicitProperty _ StructFinalPlace =
Property "final place" $ Structural FinalPlace
checkProperty :: Int -> PetriNet -> Bool -> Property -> IO PropResult checkProperty :: Int -> PetriNet -> Bool -> Property -> IO PropResult
checkProperty verbosity net refine p = do checkProperty verbosity net refine p = do
...@@ -408,7 +428,7 @@ checkLivenessProperty verbosity net refine f strans = do ...@@ -408,7 +428,7 @@ checkLivenessProperty verbosity net refine f strans = do
return Unknown return Unknown
checkStructuralProperty :: Int -> PetriNet -> Structure -> IO PropResult checkStructuralProperty :: Int -> PetriNet -> Structure -> IO PropResult
checkStructuralProperty _ net struct = do checkStructuralProperty _ net struct =
if checkStructure net struct then if checkStructure net struct then
return Satisfied return Satisfied
else else
......
...@@ -12,7 +12,6 @@ import qualified Text.Parsec.Token as Token ...@@ -12,7 +12,6 @@ import qualified Text.Parsec.Token as Token
import Parser import Parser
import PetriNet (PetriNet,makePetriNet) import PetriNet (PetriNet,makePetriNet)
import Property import Property
import Structure
languageDef :: LanguageDef () languageDef :: LanguageDef ()
languageDef = languageDef =
......
module Structure module Structure
(Structure(..), (Structure(..),
checkStructure) checkStructure,
checkParallelT)
where where
import PetriNet import PetriNet
import Data.List (intersect) import Data.List (intersect,sort)
data Structure = FreeChoice data Structure = FreeChoice | Parallel | FinalPlace
instance Show Structure where instance Show Structure where
show FreeChoice = "free choice" show FreeChoice = "free choice"
show Parallel = "parallel"
show FinalPlace = "final place"
checkStructure :: PetriNet -> Structure -> Bool checkStructure :: PetriNet -> Structure -> Bool
checkStructure net FreeChoice = checkStructure net FreeChoice =
all freeChoiceCond [(p,s) | p <- places net, s <- places net] all freeChoiceCond [(p,s) | p <- places net, s <- places net]
where freeChoiceCond (p,s) = where freeChoiceCond (p,s) =
let ppost = post net p let ppost = sort $ post net p
spost = post net s spost = sort $ post net s
in null (ppost `intersect` spost) || ppost == spost in null (ppost `intersect` spost) || ppost == spost
checkStructure net Parallel =
any (checkParallelT net) (transitions net)
checkStructure net FinalPlace =
length (filter finalPlace (places net)) == 1
where finalPlace p = null (post net p) &&
all (\t -> length (post net t) == 1) (pre net p)
checkParallelT :: PetriNet -> String -> Bool
checkParallelT net t =
any postComp [(p,s) | p <- post net t, s <- post net t]
where postComp (p,s) =
let ppost = sort $ post net p
spost = sort $ post net s
in p /= s &&
not (null ppost) && not (null spost) && ppost /= spost &&
any (\u -> length (pre net u) == 1) ppost &&
any (\u -> length (pre net u) == 1) spost
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