NuSmvLtl.hs revision f1edf379717f0ddb7607585a027cf6f03a6fce68
c9c1befa9e28187945c4a6b613e2ff2ce596a404Ewaryst SchulzModule : $Header$
e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerCopyright : (c) Klaus Hartke, Uni Bremen 2008
c9c1befa9e28187945c4a6b613e2ff2ce596a404Ewaryst SchulzLicense : GPLv2 or higher, see LICENSE.txt
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuMaintainer : Christian.Maeder@dfki.de
c9c1befa9e28187945c4a6b613e2ff2ce596a404Ewaryst SchulzStability : experimental
c9c1befa9e28187945c4a6b613e2ff2ce596a404Ewaryst SchulzPortability : portable
c9c1befa9e28187945c4a6b613e2ff2ce596a404Ewaryst Schulzmodule NuSmvLtl where
c9c1befa9e28187945c4a6b613e2ff2ce596a404Ewaryst Schulz{------------------------------------------------------------------------------}
642e53cf4725fbe1f2c956db3a7cf1846141bdffEwaryst Schulz{- LTL Specifications -}
c9c1befa9e28187945c4a6b613e2ff2ce596a404Ewaryst Schulz{------------------------------------------------------------------------------}
c9c1befa9e28187945c4a6b613e2ff2ce596a404Ewaryst Schulz-- LTL specifications are introduced by the keyword LTLSPEC. The syntax
c9c1befa9e28187945c4a6b613e2ff2ce596a404Ewaryst Schulz-- of LTL formulas recognized by NuSMV is as follows:
c9c1befa9e28187945c4a6b613e2ff2ce596a404Ewaryst Schulzdata Formula a = Var a
c9c1befa9e28187945c4a6b613e2ff2ce596a404Ewaryst Schulz | Not (Formula a) -- logical not
c9c1befa9e28187945c4a6b613e2ff2ce596a404Ewaryst Schulz | And (Formula a) (Formula a) -- logical and
c9c1befa9e28187945c4a6b613e2ff2ce596a404Ewaryst Schulz | Or (Formula a) (Formula a) -- logical or
c9c1befa9e28187945c4a6b613e2ff2ce596a404Ewaryst Schulz | Xor (Formula a) (Formula a) -- logical exlusive or
c7aec1a837c5dad9130b071a11a1a40e6ec387ffEwaryst Schulz | Impl (Formula a) (Formula a) -- logical implies
642e53cf4725fbe1f2c956db3a7cf1846141bdffEwaryst Schulz | Equiv (Formula a) (Formula a) -- logical equivalence
e17e2ac99326bc2f74b284aae94337b18320e31cEwaryst Schulz | X (Formula a) -- next state
e17e2ac99326bc2f74b284aae94337b18320e31cEwaryst Schulz | G (Formula a) -- globally
c9c1befa9e28187945c4a6b613e2ff2ce596a404Ewaryst Schulz | F (Formula a) -- finally
70a7281955f0c5e8ab0181166731a5c801ed6cc8Ewaryst Schulz | U (Formula a) (Formula a) -- until
c9c1befa9e28187945c4a6b613e2ff2ce596a404Ewaryst Schulz | V (Formula a) (Formula a) -- releases
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder | Y (Formula a) -- previous state
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder | Z (Formula a) -- not previous state not
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder | H (Formula a) -- historically
e17e2ac99326bc2f74b284aae94337b18320e31cEwaryst Schulz | O (Formula a) -- once
c9c1befa9e28187945c4a6b613e2ff2ce596a404Ewaryst Schulz | S (Formula a) (Formula a) -- since
5dad1d101f19a24ec783767c720a9b36640a1222Ewaryst Schulz | T (Formula a) (Formula a) -- triggered
0f3be7e6cc28f85641a6405c80ac19bc14843e09Ewaryst Schulzinstance (Show a) => Show (Formula a) where
3953a89b6dbc66b52dc447ab89ac765dccb3ec74Ewaryst Schulz show phi = "LTLSPEC " ++ show' phi True ++ ";" where
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder show' (Var x) outer = show x
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder show' (Not phi) outer = "! " ++ show' phi False
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder show' (And phi psi) True = show' phi False ++ " & " ++ show' psi False
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder show' (Or phi psi) True = show' phi False ++ " | " ++ show' psi False
0f3be7e6cc28f85641a6405c80ac19bc14843e09Ewaryst Schulz show' (Xor phi psi) True = show' phi False ++ " xor " ++ show' psi False
c9c1befa9e28187945c4a6b613e2ff2ce596a404Ewaryst Schulz show' (Impl phi psi) True = show' phi False ++ " -> " ++ show' psi False
ec266401925dd5b6ba498665c02a127c3da0b8a8Ewaryst Schulz show' (Equiv phi psi) True = show' phi False ++ " <-> " ++ show' psi False
ec266401925dd5b6ba498665c02a127c3da0b8a8Ewaryst Schulz show' (X phi) outer = "X " ++ show' phi False
70a7281955f0c5e8ab0181166731a5c801ed6cc8Ewaryst Schulz show' (G phi) outer = "G " ++ show' phi False
2229aec70b494e2215b8eae14e29bd27e79aa3a7Ewaryst Schulz show' (F phi) outer = "F " ++ show' phi False
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder show' (U phi psi) True = show' phi False ++ " U " ++ show' psi False
2229aec70b494e2215b8eae14e29bd27e79aa3a7Ewaryst Schulz show' (V phi psi) True = show' phi False ++ " V " ++ show' psi False
70a7281955f0c5e8ab0181166731a5c801ed6cc8Ewaryst Schulz show' (Y phi) outer = "Y " ++ show' phi False
70a7281955f0c5e8ab0181166731a5c801ed6cc8Ewaryst Schulz show' (Z phi) outer = "Z " ++ show' phi False
70a7281955f0c5e8ab0181166731a5c801ed6cc8Ewaryst Schulz show' (H phi) outer = "H " ++ show' phi False
70a7281955f0c5e8ab0181166731a5c801ed6cc8Ewaryst Schulz show' (O phi) outer = "O " ++ show' phi False
70a7281955f0c5e8ab0181166731a5c801ed6cc8Ewaryst Schulz show' (S phi psi) True = show' phi False ++ " S " ++ show' psi False
70a7281955f0c5e8ab0181166731a5c801ed6cc8Ewaryst Schulz show' (T phi psi) True = show' phi False ++ " T " ++ show' psi False
70a7281955f0c5e8ab0181166731a5c801ed6cc8Ewaryst Schulz show' phi False = "(" ++ show' phi True ++ ")"
70a7281955f0c5e8ab0181166731a5c801ed6cc8Ewaryst Schulz{------------------------------------------------------------------------------}