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

Commit ee45be29 authored by Philipp Meyer's avatar Philipp Meyer

Added transformation to validate identifiers for lola

parent 4f283fdf
......@@ -8,6 +8,7 @@ import System.IO
import System.Console.GetOpt
import Control.Monad
import Control.Applicative ((<$>))
import Control.Arrow (first)
import Data.List (partition)
import Parser
......@@ -25,7 +26,8 @@ import Solver.SComponent
data InputFormat = PNET | LOLA | TPN deriving (Show,Read)
data NetTransformation = TerminationToReachability
data NetTransformation = TerminationByReachability
| ValidateIdentifiers
data ImplicitProperty = Termination
| NoDeadlock | NoDeadlockUnlessFinal
......@@ -68,9 +70,15 @@ options =
(NoArg (\opt -> Right opt { inputFormat = TPN }))
"Use the tpn input format"
, 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 = TerminationToReachability : optTransformations opt
optTransformations = TerminationByReachability : optTransformations opt
}))
"Prove termination by reducing it to reachability"
......@@ -191,20 +199,19 @@ placeOp op (p,w) = Atom $ LinIneq (Var p) op (Const w)
transformNet :: (PetriNet, [Property]) -> NetTransformation ->
(PetriNet, [Property])
transformNet (net, props) TerminationToReachability =
transformNet (net, props) TerminationByReachability =
let prime = ('\'':)
primeFst (p,x) = (prime p, x)
ps = ["'sigma", "'m1", "'m2"] ++
places net ++ map prime (places net)
is = [("'m1", 1)] ++
initials net ++ map primeFst (initials net)
initials net ++ map (first prime) (initials net)
ts = ("'switch", [("'m1",1)], [("'m2",1)]) :
concatMap (\t ->
let (preT, postT) = context net t
pre' = [("'m1",1)] ++ preT ++ map primeFst preT
post' = [("'m1",1)] ++ postT ++ map primeFst postT
pre'' = ("'m2",1) : map primeFst preT
post'' = [("'m2",1), ("'sigma",1)] ++ map primeFst postT
pre' = [("'m1",1)] ++ preT ++ map (first prime) preT
post' = [("'m1",1)] ++ postT ++ map (first prime) postT
pre'' = ("'m2",1) : map (first prime) preT
post'' = [("'m2",1), ("'sigma",1)] ++ map (first prime) postT
in [(t, pre', post'), (prime t, pre'', post'')]
)
(transitions net)
......@@ -212,7 +219,17 @@ transformNet (net, props) TerminationToReachability =
foldl (:&:) (Atom (LinIneq (Var "'sigma") Ge (Const 1)))
(map (\p -> Atom (LinIneq (Var (prime p)) Ge (Var p)))
(places net))
-- TODO: map existing liveness properties
in (makePetriNetWithTrans (name net) ps ts is, prop : props)
transformNet (net, props) ValidateIdentifiers =
let validate = map (\c -> if c `elem` ",;:(){}\t \n\r" then '_' else c)
ps = map validate $ places net
ts = map validate $ transitions net
is = map (first validate) $ initials net
as = map (\(a,b,x) -> (validate a, validate b, x)) $ arcs net
net' = makePetriNet (name net) ps ts as is
props' = map (rename validate) props
in (net', props')
makeImplicitProperty :: PetriNet -> ImplicitProperty -> Property
makeImplicitProperty _ Termination =
......
......@@ -2,7 +2,7 @@
module PetriNet
(PetriNet,name,showNetName,places,transitions,initial,
pre,lpre,post,lpost,initials,context,
pre,lpre,post,lpost,initials,context,arcs,
makePetriNet,makePetriNetWithTrans)
where
......@@ -19,6 +19,10 @@ data PetriNet = PetriNet {
initial :: PetriNet -> String -> Integer
initial net p = M.findWithDefault 0 p (initMap net)
arcs :: PetriNet -> [(String, String, Integer)]
arcs net = concatMap (\(a,(_,bs)) -> map (\(b,w) -> (a,b,w)) bs)
(M.toList (adjacency net))
context :: PetriNet -> String -> ([(String, Integer)], [(String, Integer)])
context net x = M.findWithDefault ([],[]) x (adjacency net)
......
......@@ -3,6 +3,7 @@
module Property
(Property(..),
showPropertyName,
rename,
PropertyType(..),
Formula(..),
LinearInequation(..),
......@@ -25,6 +26,14 @@ instance Show Term where
show (t :-: u) = "(" ++ show t ++ " - " ++ show u ++ ")"
show (t :*: u) = show t ++ " * " ++ show u
renameTerm :: (String -> String) -> Term -> Term
renameTerm f (Var x) = Var (f x)
renameTerm _ (Const c) = Const c
renameTerm f (Minus t) = Minus (renameTerm f t)
renameTerm f (t :+: u) = renameTerm f t :+: renameTerm f u
renameTerm f (t :-: u) = renameTerm f t :-: renameTerm f u
renameTerm f (t :*: u) = renameTerm f t :*: renameTerm f u
data Op = Gt | Ge | Eq | Ne | Le | Lt
instance Show Op where
......@@ -41,6 +50,10 @@ data LinearInequation = LinIneq Term Op Term
instance Show LinearInequation where
show (LinIneq lhs op rhs) = show lhs ++ " " ++ show op ++ " " ++ show rhs
renameLinIneq :: (String -> String) -> LinearInequation -> LinearInequation
renameLinIneq f (LinIneq lhs op rhs) =
LinIneq (renameTerm f lhs) op (renameTerm f rhs)
data Formula = FTrue | FFalse
| Atom LinearInequation
| Neg Formula
......@@ -58,6 +71,14 @@ instance Show Formula where
show (p :&: q) = "(" ++ show p ++ " ∧ " ++ show q ++ ")"
show (p :|: q) = "(" ++ show p ++ " ∨ " ++ show q ++ ")"
renameFormula :: (String -> String) -> Formula -> Formula
renameFormula _ FTrue = FTrue
renameFormula _ FFalse = FFalse
renameFormula f (Atom a) = Atom (renameLinIneq f a)
renameFormula f (Neg p) = Neg (renameFormula f p)
renameFormula f (p :&: q) = renameFormula f p :&: renameFormula f q
renameFormula f (p :|: q) = renameFormula f p :|: renameFormula f q
data PropertyType = Safety | Liveness
instance Show PropertyType where
......@@ -74,6 +95,9 @@ instance Show Property where
show p =
showPropertyName p ++ " { " ++ show (pformula p) ++ " }"
rename :: (String -> String) -> Property -> Property
rename f (Property pn pt pf) = Property pn pt (renameFormula f pf)
showPropertyName :: Property -> String
showPropertyName p = show (ptype p) ++ " property" ++
(if null (pname p) then "" else " " ++ show (pname p))
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