Commit b6cb1c4e authored by Philipp Meyer's avatar Philipp Meyer

Added option to check if net is communication-free

parent 08fdf8e0
......@@ -43,6 +43,7 @@ data ImplicitProperty = Termination
| StructFreeChoice
| StructParallel
| StructFinalPlace
| StructCommunicationFree
deriving (Show,Read)
data Options = Options { inputFormat :: InputFormat
......@@ -162,6 +163,12 @@ options =
}))
"Prove that there is only one needed final place"
, Option "" ["communication-free"]
(NoArg (\opt -> Right opt {
optProperties = StructCommunicationFree : optProperties opt
}))
"Prove that the net is communication-free"
, Option "n" ["no-refinement"]
(NoArg (\opt -> Right opt { optRefine = False }))
"Don't use refinement"
......@@ -354,6 +361,8 @@ makeImplicitProperty _ StructParallel =
Property "parallel" $ Structural Parallel
makeImplicitProperty _ StructFinalPlace =
Property "final place" $ Structural FinalPlace
makeImplicitProperty _ StructCommunicationFree =
Property "communication free" $ Structural CommunicationFree
checkProperty :: Int -> PetriNet -> Bool -> Property -> IO PropResult
checkProperty verbosity net refine p = do
......
......@@ -7,12 +7,14 @@ where
import PetriNet
import Data.List (intersect,sort)
data Structure = FreeChoice | Parallel | FinalPlace
-- TODO: use formulas instead of hard-coded properties
data Structure = FreeChoice | Parallel | FinalPlace | CommunicationFree
instance Show Structure where
show FreeChoice = "free choice"
show Parallel = "parallel"
show FinalPlace = "final place"
show CommunicationFree = "communication free"
checkStructure :: PetriNet -> Structure -> Bool
checkStructure net FreeChoice =
......@@ -22,11 +24,13 @@ checkStructure net FreeChoice =
spost = sort $ post net s
in null (ppost `intersect` spost) || ppost == spost
checkStructure net Parallel =
any (checkParallelT net) (transitions net)
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)
length (filter finalPlace (places net)) == 1
where finalPlace p = null (post net p) &&
all (\t -> length (post net t) == 1) (pre net p)
checkStructure net CommunicationFree =
all (\t -> length (pre net t) == 1) (transitions net)
checkParallelT :: PetriNet -> String -> Bool
checkParallelT net t =
......
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