Theory PromelaLTLConv

theory PromelaLTLConv
subsection ‹Proposition types and conversion›

text ‹LTL formulae and propositions are also generated by an SML parser.
Hence we have the same setup as for Promela itself: Mirror the data structures and
(sometimes) map them to new ones.›

text ‹This theory is intended purely to be used by frontend code to convert
from propc› to expr›. The other theories work on @{typ expr} directly.

While we could of course convert directly, that would introduce yet a semantic level.›

datatype binOp = Eq | Le | LEq | Gr | GEq

datatype ident = Ident "String.literal" "integer option"

datatype propc = CProp ident
               | BProp binOp ident ident
               | BExpProp binOp ident integer

fun identConv :: "ident  varRef" where
  "identConv (Ident name None) = VarRef True name None"
| "identConv (Ident name (Some i)) = VarRef True name (Some (ExprConst i))"

definition ident2expr :: "ident  expr" where
  "ident2expr = ExprVarRef  identConv"

primrec binOpConv :: "binOp  PromelaDatastructures.binOp" where
  "binOpConv Eq = BinOpEq"
| "binOpConv Le = BinOpLe"
| "binOpConv LEq = BinOpLEq"
| "binOpConv Gr = BinOpGr"
| "binOpConv GEq = BinOpGEq"

primrec propc2expr :: "propc  expr" where
  "propc2expr (CProp ident) = 
     ExprBinOp BinOpEq (ident2expr ident) (ExprConst 1)"
| "propc2expr (BProp bop il ir) = 
     ExprBinOp (binOpConv bop) (ident2expr il) (ident2expr ir)"
| "propc2expr (BExpProp bop il ir) = 
     ExprBinOp (binOpConv bop) (ident2expr il) (ExprConst ir)"

definition ltl_conv :: "propc ltlc  expr ltlc" where
  "ltl_conv = map_ltlc propc2expr"

definition printPropc 
  :: "(integer  char list)  propc  char list"
  "printPropc f p = printExpr f (propc2expr p)" 

text ‹The semantics of a @{typ propc} is given just for reference.›
definition evalPropc :: "gState  propc  bool" where
  "evalPropc g p  exprArith g emptyProc (propc2expr p)  0"