From a6f74eb6ab2e5faecc27f129971980a8c36c818e Mon Sep 17 00:00:00 2001 From: Philipp Meyer Date: Wed, 16 Jul 2014 14:50:10 +0200 Subject: [PATCH] Made output compatible with sara --- src/Main.hs | 3 ++- src/Printer/SARA.hs | 3 ++- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/src/Main.hs b/src/Main.hs index 5c86b126..4381630f 100644 --- a/src/Main.hs +++ b/src/Main.hs @@ -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) diff --git a/src/Printer/SARA.hs b/src/Printer/SARA.hs index 6d29e80b..9f4b4790 100644 --- a/src/Printer/SARA.hs +++ b/src/Printer/SARA.hs @@ -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" ++ -- GitLab