type State = int * bool list * int list * string list;
type Model = string list * State list;

exception badPredicate;
exception badFormula;

(* ---- datatypes definitions BEGIN ---- *)

datatype 'L formula =
	EMPTY | TRUE | FALSE
	| PRED of 'L
	| NOT of 'L formula
	| AND of 'L formula * 'L formula
	| AX of 'L formula
	| EX of 'L formula 
	| AU of 'L formula * 'L formula
	| EU of 'L formula * 'L formula ;

(* ---- datatypes definitions END ---- *)


(* ---- helper functions BEGIN ---- *)

(* returns ~1 if index not found *)

fun memberIndex m nil = ~1
  | memberIndex m (s::t) = if (m=s) then 0 else
      let val i = (memberIndex m t)
      in
          if i = ~1 
            then ~1
          else
            i+1
      end;


(* returns true if member of list, false if not *)
fun member x nil = false
  | member x (s::t) = (x=s) orelse member x t;

(* returns if state n has been visited *)
fun isMarked m n = Array.sub(m,n);

(* adds visited mark and returns new marked array *)
fun addMark (n,mArray) = ( 
			  Array.update(mArray,n,true);
			  mArray
			  );

(* initializes marked array of length n with all entries set to false *)
fun mark_init n = Array.array(n,false);

(* ---- helper functions END ---- *)



(* ----- guts of program BEGIN -------- *)

(* if formula holds for given model at state n, returns true *)
fun mCheck (apList:string list, stList:State list, mArray) EMPTY n = true
  | mCheck (apList:string list, stList:State list,mArray) TRUE n = true
  | mCheck (apList:string list, stList:State list,mArray) FALSE n = false
  | mCheck (apList:string list,  stList:State list,mArray) (PRED p) n =
        if (member p apList) then
          let val s = List.nth (stList,n);
              val tmpAP = memberIndex p apList;
          in
              List.nth((#2 s),tmpAP)
          end
          else raise badPredicate
  | mCheck (apList:string list, stList:State list,mArray) (NOT f) n =
        not( mCheck(apList:string list, stList:State list,mArray) f n)
  | mCheck (apList:string list, stList:State list,mArray) (AND(f1,f2)) n =
        mCheck(apList:string list, stList:State list,mArray) f1 n andalso mCheck(apList:string list, stList:State list,mArray) f2 n

  | mCheck (apList:string list, stList:State list,mArray) (AX f) n =
        let val s = List.nth(stList,n);
            val tls = #3 s;
        in
            List.all (mCheck (apList:string list, stList:State list,mArray) f ) tls
        end
  | mCheck (apList:string list, stList:State list,mArray) (EX f) n =
        let val s = List.nth(stList,n);
            val tls = #3 s;
        in
            List.exists (mCheck(apList:string list, stList:State list,mArray) f) tls
        end
  | mCheck (apList,stList,mArray) (AU(f1,f2)) n =
        let val mArray2 = mark_init(List.length(stList));
            val notMarked = List.filter (not o isMarked mArray2) (map #1 stList);
        in
            List.all (fwdAU(apList,stList,mArray2) (AU(f1,f2))) notMarked
        end
  | mCheck (apList:string list, stList:State list,mArray) (EU(f1,f2)) n =
        let val mArray2 = mark_init(List.length(stList));
            val notMarked = List.filter (not o isMarked mArray2) (map #1 stList);
        in
            List.exists (fwdEU(apList,stList,mArray2) (EU(f1,f2))) notMarked
        end

  and fwdAU (apList:string list, stList:State list,mArray) (AU(f1,f2)) n =
        if (isMarked mArray n) then false
	else 
	    let val newarr = addMark(n,mArray);
            in
                if (mCheck(apList,stList,newarr) f2 n) then true
		else
		    let val f1pos = mCheck(apList,stList,newarr) f1 n;
                    in
		        if (not f1pos) then false
			else (* f1^~f2 => search successors of s *)
			    let val s = List.nth(stList,n);
			        val tls = #3 s;
                            in
			        List.all(fwdAU(apList,stList,newarr) (AU(f1,f2))) tls
			    end
		    end
            end
    | fwdAU (apList:string list, stList:State list,mArray) f n = raise badFormula

  and fwdEU(apList:string list, stList:State list,mArray) (EU(f1,f2)) n =
        if (isMarked mArray n) then false
	else
	    let val newarr = addMark(n,mArray);
	    in
	        if (mCheck(apList,stList,newarr) f2 n) then true
                else
                    let val f1pos = mCheck(apList,stList,newarr) f1 n;
                    in
                        if (not f1pos) then false
                        else (* f1^~f2 => search successors of s *)
                            let val s = List.nth(stList,n);
                                val tls = #3 s;
                            in
                                List.exists (fwdEU(apList,stList,newarr) (EU(f1,f2))) tls
                            end
                    end
            end

    | fwdEU(apList:string list, stList:State list,mArray) f n = raise badFormula 
	

(* ----- END   guts of program -------- *)




(* ---- highest level function BEGIN ---- *)

(* tests formula against model m with start state s *)
fun mTest (m:Model) f s =
        let val apList  = #1 m;
            val stList  = #2 m;
            val mArray = mark_init(length(stList));
        in
            mCheck (apList,stList,mArray) f s
        end;

(* ---- highest level function END ---- *)