Commit 93273f58 authored by Stefan Jaax's avatar Stefan Jaax

Change formula format

parent 4df299f3
......@@ -27,13 +27,13 @@ languageDef =
Token.commentStart = "/*",
Token.commentEnd = "*/",
Token.commentLine = "//",
Token.identStart = letter <|> char '_',
Token.identStart = alphaNum <|> letter <|> char '_',
Token.identLetter = alphaNum <|> char '_',
Token.reservedNames = ["true", "false", "EXISTS", "FORALL"],
Token.reservedOpNames = ["->", "<", "<=", "=", "!=", ">=", ">",
"+", "-", "*", "&&", "||", "!", ":"]
}
lexer :: Token.TokenParser ()
lexer = Token.makeTokenParser languageDef
......@@ -71,7 +71,7 @@ numberOption :: Parser Integer
numberOption = option 1 (brackets natural)
ident :: Parser String
ident = (identifier <|> stringLiteral) <?> "identifier"
ident = (char 'C' *> brackets (identifier <|> stringLiteral)) <?> "identifier"
identList :: Parser [String]
identList = singleOrList ident
......@@ -152,13 +152,13 @@ instance FromJSON (QuantFormula String) where
instance ToJSON (QuantFormula String) where
toJSON x = String ""
data RecordTransition = RecordTransition {
data RecordTransition = RecordTransition {
name :: String,
pre :: [String],
post :: [String]
} deriving (Show)
data RecordPP = RecordPP {
data RecordPP = RecordPP {
title :: String,
states :: [String],
transitions :: [RecordTransition],
......@@ -172,20 +172,18 @@ $(deriveJSON defaultOptions ''RecordTransition)
$(deriveJSON defaultOptions ''RecordPP)
recordPP2PopulationProtocol :: RecordPP -> PopulationProtocol
recordPP2PopulationProtocol r =
recordPP2PopulationProtocol r =
makePopulationProtocolFromStrings (title r) (states r) (map name (transitions r)) (initialStates r) (trueStates r) falseStates p arcs where
falseStates = [q | q <- states r, not (S.member q (S.fromList (trueStates r)))]
arcs = [(q, name t, 1) | t <- transitions r, q <- pre t] ++
arcs = [(q, name t, 1) | t <- transitions r, q <- pre t] ++
[(name t, q, 1) | t <- transitions r, q <- post t]
p = case predicate r of Nothing -> ExQuantFormula [] FTrue
p = case predicate r of Nothing -> ExQuantFormula [] FTrue
(Just p') -> p'
parseContent :: Parser PopulationProtocol
parseContent = do
parseContent = do
str <- manyTill anyChar eof
let r = eitherDecode (BS.pack str)
case r of
(Left e) -> fail e
(Right pp) -> return (recordPP2PopulationProtocol pp)
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