Commit a6f74eb6 authored by Philipp Meyer's avatar Philipp Meyer

Made output compatible with sara

parent 1ec6cad1
......@@ -222,7 +222,8 @@ transformNet (net, props) TerminationByReachability =
(transitions net)
prop = Property "termination by reachability" Safety $
foldl (:&:) (Atom (LinIneq (Var "'sigma") Ge (Const 1)))
(map (\p -> Atom (LinIneq (Var (prime p)) Ge (Var p)))
(map (\p -> Atom (LinIneq
(Var (prime p) :-: Var p) Ge (Const 0)))
(places net))
-- TODO: map existing liveness properties
in (makePetriNetWithTrans (name net) ps ts is, prop : props)
......
......@@ -41,7 +41,8 @@ printProperty :: String -> PetriNet -> Property -> String
printProperty filename net (Property propname Safety f) =
"PROBLEM " ++ validateId propname ++ ":\n" ++
"GOAL REACHABILITY;\n" ++
"FILE " ++ filename ++ " TYPE LOLA;\n" ++
"FILE " ++ reverse (takeWhile (/='/') (reverse filename)) ++
" TYPE LOLA;\n" ++
"INITIAL " ++ intercalate ","
(map (\(p,i) -> p ++ ":" ++ show i) (initials net)) ++ ";\n" ++
"FINAL COVER;\n" ++
......
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