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

Commit ad3b64e6 authored by Philipp Meyer's avatar Philipp Meyer

Remove petri net only code and rename terminology for population protocols

parent 3cc46d66
This diff is collapsed.
{-# LANGUAGE TupleSections #-}
module Options
(InputFormat(..),OutputFormat(..),NetTransformation(..),RefinementType(..),
(InputFormat(..),OutputFormat(..),RefinementType(..),
ImplicitProperty(..),Options(..),startOptions,options,parseArgs,
usageInformation)
where
......@@ -10,32 +10,22 @@ import Control.Applicative ((<$>))
import System.Console.GetOpt
import System.Environment (getArgs)
data InputFormat = PNET | LOLA | TPN | MIST deriving (Show,Read)
data OutputFormat = OutLOLA | OutSARA | OutSPEC | OutDOT deriving (Read)
data InputFormat = InPP deriving (Read)
data OutputFormat = OutDOT deriving (Read)
instance Show InputFormat where
show InPP = "PP"
instance Show OutputFormat where
show OutLOLA = "LOLA"
show OutSARA = "SARA"
show OutSPEC = "SPEC"
show OutDOT = "DOT"
data NetTransformation = TerminationByReachability
| ValidateIdentifiers
data ImplicitProperty = Termination
| DeadlockFree | DeadlockFreeUnlessFinal
| FinalStateUnreachable
| ProperTermination
| Safe | Bounded Integer
| StructFreeChoice
| StructParallel
| StructFinalPlace
| StructCommunicationFree
| TerminalMarkingsUniqueConsensus
data ImplicitProperty = TerminalMarkingsUniqueConsensus
| TerminalMarkingReachable
deriving (Show,Read)
data RefinementType = TrapRefinement | SComponentRefinement | SComponentWithCutRefinement
data RefinementType = TrapRefinement
| SiphonRefinement
| UTrapRefinement
| USiphonRefinement
deriving (Show,Read)
data Options = Options { inputFormat :: InputFormat
......@@ -43,11 +33,8 @@ data Options = Options { inputFormat :: InputFormat
, optShowHelp :: Bool
, optShowVersion :: Bool
, optProperties :: [ImplicitProperty]
, optTransformations :: [NetTransformation]
, optSimpMethod :: Int
, optRefinementType :: Maybe RefinementType
, optRefinementType :: Maybe [RefinementType]
, optMinimizeRefinement :: Int
, optAuto :: Bool
, optSMTAuto :: Bool
, optInvariant :: Bool
, optBoolConst :: Bool
......@@ -58,138 +45,41 @@ data Options = Options { inputFormat :: InputFormat
}
startOptions :: Options
startOptions = Options { inputFormat = PNET
startOptions = Options { inputFormat = InPP
, optVerbosity = 1
, optShowHelp = False
, optShowVersion = False
, optProperties = []
, optTransformations = []
, optSimpMethod = 1
, optRefinementType = Just SComponentWithCutRefinement
, optRefinementType = Just [TrapRefinement, SiphonRefinement, UTrapRefinement, USiphonRefinement]
, optMinimizeRefinement = 0
, optAuto = False
, optSMTAuto = True
, optInvariant = False
, optBoolConst = False
, optOutput = Nothing
, outputFormat = OutLOLA
, outputFormat = OutDOT
, optUseProperties = True
, optPrintStructure = False
}
options :: [ OptDescr (Options -> Either String Options) ]
options =
[ Option "" ["pnet"]
(NoArg (\opt -> Right opt { inputFormat = PNET }))
"Use the pnet input format"
, Option "" ["lola"]
(NoArg (\opt -> Right opt { inputFormat = LOLA }))
"Use the lola input format"
, Option "" ["tpn"]
(NoArg (\opt -> Right opt { inputFormat = TPN }))
"Use the tpn input format"
, Option "" ["spec"]
(NoArg (\opt -> Right opt { inputFormat = MIST }))
"Use the mist input format"
[ Option "" ["pp"]
(NoArg (\opt -> Right opt { inputFormat = InPP }))
"Use the population protocol input format"
, Option "" ["structure"]
(NoArg (\opt -> Right opt { optPrintStructure = True }))
"Print structural information"
, Option "" ["validate-identifiers"]
(NoArg (\opt -> Right opt {
optTransformations = ValidateIdentifiers : optTransformations opt
}))
"Make identifiers valid for lola"
, Option "" ["termination-by-reachability"]
(NoArg (\opt -> Right opt {
optTransformations = TerminationByReachability : optTransformations opt
}))
"Prove termination by reducing it to reachability"
, Option "" ["termination"]
(NoArg (\opt -> Right opt {
optProperties = Termination : optProperties opt
}))
"Prove that the net is terminating"
, Option "" ["proper-termination"]
(NoArg (\opt -> Right opt {
optProperties = ProperTermination : optProperties opt
}))
"Prove termination in the final marking"
, Option "" ["deadlock-free"]
(NoArg (\opt -> Right opt {
optProperties = DeadlockFree : optProperties opt
}))
"Prove that the net is deadlock-free"
, Option "" ["deadlock-free-unless-final"]
(NoArg (\opt -> Right opt {
optProperties = DeadlockFreeUnlessFinal : optProperties opt
}))
("Prove that the net is deadlock-free\n" ++
" unless it is in the final marking")
, Option "" ["final-state-unreachable"]
(NoArg (\opt -> Right opt {
optProperties = FinalStateUnreachable : optProperties opt
}))
"Prove that the final state is unreachable"
, Option "" ["safe"]
(NoArg (\opt -> Right opt {
optProperties = Safe : optProperties opt
}))
"Prove that the net is safe, i.e. 1-bounded"
, Option "" ["bounded"]
(ReqArg (\arg opt -> case reads arg of
[(k, "")] -> Right opt {
optProperties = Bounded k : optProperties opt }
_ -> Left ("invalid argument for k-bounded option: " ++ arg)
)
"K")
"Prove that the net is K-bounded"
, Option "" ["free-choice"]
(NoArg (\opt -> Right opt {
optProperties = StructFreeChoice : optProperties opt
}))
"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 "" ["communication-free"]
(NoArg (\opt -> Right opt {
optProperties = StructCommunicationFree : optProperties opt
}))
"Prove that the net is communication-free"
, Option "" ["terminal-markings-unique-consensus"]
(NoArg (\opt -> Right opt {
optProperties = TerminalMarkingsUniqueConsensus : optProperties opt
optProperties = optProperties opt ++ [TerminalMarkingsUniqueConsensus]
}))
"Prove that terminal markings have a unique consensus"
, Option "" ["terminal-marking-reachable"]
(NoArg (\opt -> Right opt {
optProperties = TerminalMarkingReachable : optProperties opt
optProperties = optProperties opt ++ [TerminalMarkingReachable]
}))
"Prove that a terminal marking is reachable"
......@@ -203,66 +93,35 @@ options =
" for transition invariant")
, Option "r" ["refinement"]
(ReqArg (\arg opt -> case reads arg :: [(Int, String)] of
[(0, "")] -> Right opt { optRefinementType = Nothing }
[(1, "")] -> Right opt { optRefinementType = Just SComponentWithCutRefinement }
[(2, "")] -> Right opt { optRefinementType = Just SComponentRefinement }
[(3, "")] -> Right opt { optRefinementType = Just TrapRefinement }
_ -> Left ("invalid argument for refinement method: " ++ arg)
(ReqArg (\arg opt ->
let addRef ref =
Right opt { optRefinementType =
case optRefinementType opt of
Nothing -> Just [ref]
Just(refs) -> Just (refs ++ [ref])
}
in case arg of
"trap" -> addRef TrapRefinement
"siphon" -> addRef SiphonRefinement
"utrap" -> addRef UTrapRefinement
"usiphon" -> addRef USiphonRefinement
_ -> Left ("invalid argument for refinement method: " ++ arg)
)
"METHOD")
("Refine with METHOD (0=none, 1=SCompCut+Traps,\n" ++
" 2=SComp+Traps, 3=Traps)")
("Refine with METHOD (trap, siphon, utrap, usiphon)")
, Option "o" ["output"]
(ReqArg (\arg opt -> Right opt {
optOutput = Just arg
})
"FILE")
"Write net and properties to FILE"
, Option "" ["out-lola"]
(NoArg (\opt -> Right opt { outputFormat = OutLOLA }))
"Use the lola output format"
, Option "" ["out-sara"]
(NoArg (\opt -> Right opt { outputFormat = OutSARA }))
"Use the sara output format"
, Option "" ["out-spec"]
(NoArg (\opt -> Right opt { outputFormat = OutSPEC }))
"Use the spec output format"
"Write population protocol to FILE"
, Option "" ["out-dot"]
(NoArg (\opt -> Right opt { outputFormat = OutDOT }))
"Use the dot output format"
, Option "" ["no-given-properties"]
(NoArg (\opt -> Right opt {
optUseProperties = False
}))
"Do not use the properties given in the input file"
, Option "s" ["simp"]
(ReqArg (\arg opt -> case reads arg of
[(i, "")] -> Right opt { optSimpMethod = i }
_ -> Left ("invalid argument for simplification method: " ++ arg)
)
"METHOD")
"Simply formula with method METHOD (0-2)"
, Option "" ["simp-1"]
(NoArg (\opt -> Right opt {
optSimpMethod = 1
}))
"Use simplification level 1 for invariant generation"
, Option "" ["simp-2"]
(NoArg (\opt -> Right opt {
optSimpMethod = 2
}))
"Use simplification level 2 for invariant generation"
, Option "m" ["minimize"]
(ReqArg (\arg opt -> case reads arg of
[(i, "")] -> Right opt { optMinimizeRefinement = i }
......@@ -271,10 +130,6 @@ options =
"METHOD")
"Minimize size of refinement structure by method METHOD (1-4)"
, Option "" ["auto"]
(NoArg (\opt -> Right opt { optAuto = True }))
"Automatically find best refinement, minimization and simplification method"
, Option "" ["smt-disable-auto-config"]
(NoArg (\opt -> Right opt { optSMTAuto = False }))
"Disable automatic configuration of the SMT solver"
......@@ -305,4 +160,4 @@ parseArgs = do
(_, _, errs) -> return $ Left $ concat errs
usageInformation :: String
usageInformation = usageInfo "SLAPnet" options
usageInformation = usageInfo "VerPol" options
module Parser.LOLA
(module Parser.LOLAFormula,
parseContent)
where
import Control.Applicative ((*>),(<*))
import Text.Parsec
import Text.Parsec.Language (LanguageDef, emptyDef)
import qualified Text.Parsec.Token as Token
import Parser
import Parser.LOLAFormula
import PetriNet (PetriNet,makePetriNetWithTransFromStrings)
import Property
languageDef :: LanguageDef ()
languageDef =
emptyDef {
Token.commentStart = "{",
Token.commentEnd = "}",
Token.commentLine = "",
Token.identStart = noneOf ",;:(){}\t \n\r",
Token.identLetter = noneOf ",;:(){}\t \n\r",
Token.reservedNames = ["PLACE", "MARKING", "SAFE",
"TRANSITION", "CONSUME", "PRODUCE",
"STRONG", "WEAK", "FAIR"],
Token.reservedOpNames = []
}
lexer :: Token.TokenParser ()
lexer = Token.makeTokenParser languageDef
identifier :: Parser String
identifier = Token.identifier lexer -- parses an identifier
reserved :: String -> Parser ()
reserved = Token.reserved lexer -- parses a reserved name
integer :: Parser Integer
integer = Token.integer lexer -- parses an integer
colon :: Parser String
colon = Token.colon lexer -- parses a colon
semi :: Parser String
semi = Token.semi lexer -- parses a semicolon
commaSep1 :: Parser a -> Parser [a]
commaSep1 = Token.commaSep1 lexer -- parses a comma separated list
whiteSpace :: Parser ()
whiteSpace = Token.whiteSpace lexer -- parses whitespace
ident :: Parser String
ident = (identifier <|> fmap show integer) <?> "identifier"
net :: Parser PetriNet
net = do
reserved "PLACE"
ps <- placeLists
reserved "MARKING"
initial <- option [] markingList
_ <- semi
ts <- many1 transition
return $ makePetriNetWithTransFromStrings "" ps ts initial [] [] [] [] []
placeLists :: Parser [String]
placeLists =
fmap concat (many1 (do
_ <- optionMaybe (reserved "SAFE" *> option 1 integer <* colon)
ps <- placeList
_ <- semi
return ps
))
placeList :: Parser [String]
placeList = commaSep1 ident
markingList :: Parser [(String, Integer)]
markingList = commaSep1 marking
marking :: Parser (String, Integer)
marking = do
s <- ident
i <- option 1 (colon *> integer)
return (s, i)
transition :: Parser (String, ([(String, Integer)], [(String, Integer)]))
transition = do
reserved "TRANSITION"
t <- ident
_ <- optionMaybe ((reserved "STRONG" <|> reserved "WEAK") <*
reserved "FAIR")
reserved "CONSUME"
input <- option [] arcList
_ <- semi
reserved "PRODUCE"
output <- option [] arcList
_ <- semi
return (t, (input, output))
arcList :: Parser [(String, Integer)]
arcList = commaSep1 arc
arc :: Parser (String, Integer)
arc = do
x <- ident
w <- option 1 (colon *> integer)
return (x, w)
parseContent :: Parser (PetriNet,[Property])
parseContent = do
whiteSpace
n <- net
eof
return (n, [])
module Parser.LOLAFormula
(parseFormula)
where
import Control.Applicative ((*>),(<$>))
import Data.Functor.Identity
import Text.Parsec
import Text.Parsec.Expr
import Text.Parsec.Language (LanguageDef, emptyDef)
import qualified Text.Parsec.Token as Token
import Parser
import Property
languageDef :: LanguageDef ()
languageDef =
emptyDef {
Token.commentStart = "{",
Token.commentEnd = "}",
Token.commentLine = "",
Token.identStart = noneOf ",;:(){}\t \n\r0123456789-",
Token.identLetter = noneOf ",;:(){}\t \n\r",
Token.reservedNames = ["FORMULA", "TRUE", "FALSE",
"NOT", "AND", "OR"],
Token.reservedOpNames = ["<", "<=", "=", "!=", ">=", ">",
"+", "-", "*"]
}
lexer :: Token.TokenParser ()
lexer = Token.makeTokenParser languageDef
identifier :: Parser String
identifier = Token.identifier lexer -- parses an identifier
reserved :: String -> Parser ()
reserved = Token.reserved lexer -- parses a reserved name
reservedOp :: String -> Parser ()
reservedOp = Token.reservedOp lexer -- parses an operator
parens :: Parser a -> Parser a
parens = Token.parens lexer -- parses p surrounded by parenthesis
integer :: Parser Integer
integer = Token.integer lexer -- parses an integer
whiteSpace :: Parser ()
whiteSpace = Token.whiteSpace lexer -- parses whitespace
binary :: String -> (a -> a -> a) -> Assoc -> Operator String () Identity a
binary name fun = Infix ( reservedOp name *> return fun )
prefix :: String -> (a -> a) -> Operator String () Identity a
prefix name fun = Prefix ( reservedOp name *> return fun )
termOperatorTable :: [[Operator String () Identity (Term String)]]
termOperatorTable =
[ [ prefix "-" Minus ]
, [ binary "*" (:*:) AssocLeft ]
, [ binary "+" (:+:) AssocLeft, binary "-" (:-:) AssocLeft ]
]
termAtom :: Parser (Term String)
termAtom = (Var <$> identifier)
<|> (Const <$> integer)
<|> parens term
<?> "basic term"
term :: Parser (Term String)
term = buildExpressionParser termOperatorTable termAtom <?> "term"
parseOp :: Parser Op
parseOp = (reservedOp "<" *> return Lt) <|>
(reservedOp "<=" *> return Le) <|>
(reservedOp "=" *> return Eq) <|>
(reservedOp "!=" *> return Ne) <|>
(reservedOp ">" *> return Gt) <|>
(reservedOp ">=" *> return Ge)
linIneq :: Parser (Formula String)
linIneq = do
lhs <- term
op <- parseOp
rhs <- term
return (LinearInequation lhs op rhs)
binaryName :: String -> (a -> a -> a) -> Assoc -> Operator String () Identity a
binaryName name fun = Infix ( reserved name *> return fun )
prefixName :: String -> (a -> a) -> Operator String () Identity a
prefixName name fun = Prefix ( reserved name *> return fun )
formOperatorTable :: [[Operator String () Identity (Formula String)]]
formOperatorTable =
[ [ prefixName "NOT" Neg ]
, [ binaryName "AND" (:&:) AssocRight ]
, [ binaryName "OR" (:|:) AssocRight ]
]
formAtom :: Parser (Formula String)
formAtom = try linIneq
<|> (reserved "TRUE" *> return FTrue)
<|> (reserved "FALSE" *> return FFalse)
<|> parens formula
<?> "basic formula"
formula :: Parser (Formula String)
formula = buildExpressionParser formOperatorTable formAtom <?> "formula"
parseFormula :: Parser (Formula String)
parseFormula = do
whiteSpace
reserved "FORMULA"
f <- formula
eof
return f
module Parser.MIST
(parseContent)
where
import Control.Applicative ((<$>),(*>),(<*),(<*>))
import Control.Monad (when)
import Data.List (sortBy, groupBy)
import Data.Function (on)
import Data.Ord (comparing)
import Text.Parsec
import Text.Parsec.Language (LanguageDef, emptyDef)
import qualified Text.Parsec.Token as Token
import Parser
import PetriNet (PetriNet,makePetriNetWithTransFromStrings,Place(..))
import Property
languageDef :: LanguageDef ()
languageDef =
emptyDef {
Token.commentStart = "",
Token.commentEnd = "",
Token.commentLine = "#",
Token.identStart = letter <|> char '_',
Token.identLetter = alphaNum <|> oneOf "'_",
Token.reservedNames = ["vars", "rules", "init",
"target", "invariants"],
Token.reservedOpNames = ["->", "+", "-", "=", ">="]
}
lexer :: Token.TokenParser ()
lexer = Token.makeTokenParser languageDef
identifier :: Parser String
identifier = Token.identifier lexer -- parses an identifier
reserved :: String -> Parser ()
reserved = Token.reserved lexer -- parses a reserved name
reservedOp :: String -> Parser ()
reservedOp = Token.reservedOp lexer -- parses an operator
integer :: Parser Integer
integer = Token.integer lexer -- parses an integer
semi :: Parser String
semi = Token.semi lexer -- parses a semicolon
commaSep :: Parser a -> Parser [a]
commaSep = Token.commaSep lexer -- parses a comma separated list
commaSep1 :: Parser a -> Parser [a]
commaSep1 = Token.commaSep1 lexer -- parses a comma separated list
whiteSpace :: Parser ()
whiteSpace = Token.whiteSpace lexer -- parses whitespace
net :: Parser PetriNet
net = do
reserved "vars"
ps <- many1 identifier
reserved "rules"
ts <- transitions
reserved "init"
(is,initTrans) <- initial
return $ makePetriNetWithTransFromStrings "" ps (initTrans ++ ts) is
(map fst initTrans) [] [] [] []
prop :: Parser Property
prop = do
reserved "target"
ineqs <- many1 (commaSep1 ineq)
_ <- optionMaybe (reserved "invariants" *> invariants)
return $ Property "" $ Safety $
foldl1 (:|:) $ map (foldl1 (:&:)) ineqs
ineq :: Parser (Formula Place)
ineq = do
x <- identifier
reservedOp ">="
c <- integer