Commit 924e4ace authored by Joshua Moerman's avatar Joshua Moerman
Browse files

Removed simplification of the formulas

parent d8ce85ec
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
import NuSMV
import Control.Monad (when)
main = loop where
loop = do
l <- getLine
let l2 = case l of
[] -> []
'#':str -> '#':str
ltl -> unlines ["#original: "++ltl, simpl ltl]
putStrLn l2
'#':str -> []
ltl -> "LTLSPEC " ++ simpl ltl
when (not $ null l2) $ putStrLn l2
loop
......@@ -74,5 +74,5 @@ showIO False (Input str) = "input != " ++ str
showIO True (Output str) = "output = " ++ str
showIO False (Output str) = "output != " ++ str
toNuSMV = prettyPrint showIO . simplify . convert . toIO . L.simplify
toNuSMV = prettyPrint showIO . convert . toIO
simpl str = either show (toNuSMV) (parse L.parseLTL "" str)
Supports Markdown
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