content: {- |
  Module      :  ./Temporal/NuSmvLtl.hs
  Copyright   :  (c) Klaus Hartke, Uni Bremen 2008
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  Christian.Maeder@dfki.de
  Stability   :  experimental
  Portability :  portable
  
  -}
  
  module NuSmvLtl where
  
  
  {- ----------------------------------------------------------------------------
  LTL Specifications
  ---------------------------------------------------------------------------- -}
  
  --
  {- LTL specifications are introduced by the keyword LTLSPEC. The syntax
  of LTL formulas recognized by NuSMV is as follows: -}
  --
  
  data Formula a = Var a
                 | Not (Formula a)                   -- logical not
                 | And (Formula a) (Formula a)       -- logical and
                 | Or (Formula a) (Formula a)       -- logical or
                 | Xor (Formula a) (Formula a)       -- logical exlusive or
                 | Impl (Formula a) (Formula a)       -- logical implies
                 | Equiv (Formula a) (Formula a)       {- logical equivalence
                 Future -}
                 | X (Formula a)                   -- next state
                 | G (Formula a)                   -- globally
                 | F (Formula a)                   -- finally
                 | U (Formula a) (Formula a)       -- until
                 | V (Formula a) (Formula a)       {- releases
                 Past -}
                 | Y (Formula a)                   -- previous state
                 | Z (Formula a)                   -- not previous state not
                 | H (Formula a)                   -- historically
                 | O (Formula a)                   -- once
                 | S (Formula a) (Formula a)       -- since
                 | T (Formula a) (Formula a)       -- triggered
  
  
  instance (Show a) => Show (Formula a) where
    show phi = "LTLSPEC " ++ show' phi True ++ ";" where
      show' (Var x) outer = show x
      show' (Not phi) outer = "! " ++ show' phi False
      show' (And phi psi) True = show' phi False ++ " & " ++ show' psi False
      show' (Or phi psi) True = show' phi False ++ " | " ++ show' psi False
      show' (Xor phi psi) True = show' phi False ++ " xor " ++ show' psi False
      show' (Impl phi psi) True = show' phi False ++ " -> " ++ show' psi False
      show' (Equiv phi psi) True = show' phi False ++ " <-> " ++ show' psi False
      show' (X phi) outer = "X " ++ show' phi False
      show' (G phi) outer = "G " ++ show' phi False
      show' (F phi) outer = "F " ++ show' phi False
      show' (U phi psi) True = show' phi False ++ " U " ++ show' psi False
      show' (V phi psi) True = show' phi False ++ " V " ++ show' psi False
      show' (Y phi) outer = "Y " ++ show' phi False
      show' (Z phi) outer = "Z " ++ show' phi False
      show' (H phi) outer = "H " ++ show' phi False
      show' (O phi) outer = "O " ++ show' phi False
      show' (S phi psi) True = show' phi False ++ " S " ++ show' psi False
      show' (T phi psi) True = show' phi False ++ " T " ++ show' psi False
      show' phi False = "(" ++ show' phi True ++ ")"
  
  
  -- ----------------------------------------------------------------------------
  