(* used in reduction of an extended set of CTL formulae to notation acceptable by original model checker *) 

(* load original model checker *)
use "chkModel.ml";

(* create datatype for extended CTL formulae set *)
datatype 'L extformula = 
	   True
	 | False
	 | Pred of 'L
	 | Not of 'L extformula 
	 | And of 'L extformula * 'L extformula 
	 | Or of 'L extformula * 'L extformula
	 | Imply of 'L extformula * 'L extformula
	 | Ax of 'L extformula 
	 | Ex of 'L extformula 
	 | Au of 'L extformula * 'L extformula 
	 | Eu of 'L extformula * 'L extformula 
	 | Af of 'L extformula
	 | Ef of 'L extformula
	 | Ag of 'L extformula
	 | Eg of 'L extformula;

(* translates extended formulae to that accepted by chkModel.ml *)

fun trans True = TRUE
  | trans False = FALSE
  | trans (Pred p) = (PRED p)
  | trans (Not f) = (NOT (trans f))
  | trans (And(f1,f2)) = (AND((trans f1),(trans f2)))
  | trans (Or(f1,f2)) = (NOT(AND(NOT(trans f1), NOT(trans f2))))
  | trans (Imply(f1,f2)) = (NOT(AND((trans f1), NOT(trans f2))))
  | trans (Ax(f)) = (AX(trans f))
  | trans (Ex(f)) = (EX(trans f))
  | trans (Au(f1, f2)) = (AU((trans f1), (trans f2)))
  | trans (Eu(f1, f2)) = (EU((trans f1), (trans f2)))
  | trans (Af(f)) = (AU(TRUE, (trans f)))
  | trans (Ef(f)) = (EU(TRUE, (trans f)))
  | trans (Eg(f)) = (NOT(AU(TRUE, NOT(trans f))))
  | trans (Ag(f)) = (NOT(EU(TRUE, NOT(trans f))));

(* test an extended formula *)
fun mCheckExt (m:Model) f s =
	let val tf = trans f;
	in
	    mTest m tf s
	end;