(*
------------------------------------------------------------------------------
FUNCTION LIBRARY

Functions to perform mappings, logical operations and member extractions.
------------------------------------------------------------------------------
*)

(* exceptions *)
exception EXC_NOT_FOUND;
exception EXC_INVALID_INDEX;

(* applies a function to a list and returns list of results *)
fun mapList(F, nil) = nil
  | mapList(F, head::tail) = F(head)::mapList(F, tail) ;

(* functions used to appy reductions with *)
fun myOR(x, y) = x orelse y; 
fun myAND(x, y) = x andalso y;

(* applies successively a function to the head and function of tail of a list *)
fun reduce(F, nil, element) = element
  | reduce(F, head::tail, element) = F(head, reduce(F, tail, element)) ;

(* explores the states * elements list recursively to get the elements list for a state *)
fun getList(state, nil) =
    raise EXC_NOT_FOUND
  | getList(state, (state1, list)::tail) =
    if state = state1 then (* found the right state *)
      list (* return the elements list *)
    else
      getList(state, tail); (* recursive call for the next state * list *)

(* explores the states * labels list recursively to add a label for a state *)
fun setList(state, nil, _) =  
  raise EXC_NOT_FOUND
  | setList(state, (state1, label)::tail, newLabel) =
    if state = state1 then (* found the right state *)
      (state1, newLabel)::tail (* end of recursion, return a value catenated to the rest of the list *)
    else
      (state1, label)::setList(state, tail, newLabel); (* recursive call for the next state *)

(* reads a file into a list of strings of one char each *)
fun makeListFromInput(fileName) = 
  if end_of_stream(fileName) then
    nil
  else
    let
      val currentChar = input(fileName, 1);
    in
      if currentChar = ";" then nil (* separate lines with ; *)
      else currentChar::makeListFromInput(fileName) (* recursive call for next char *)
    end;

(* true if element is member of list - not curried like the one in model reader *)
fun isListMember(_, nil) = false
  | isListMember(member, head::tail) =
      if member = head then true
      else
	isListMember(member, tail); (* recursive call for the next element *)

(* returns the index of an element in a list - not curried like the one in model reader *)
fun indexInList(_, nil) = raise EXC_INVALID_INDEX
  | indexInList(element, head::tail) = 
      if element = head then
        1
      else
	1 + indexInList(element, tail); (* recursive call to check the next element *)

(* reverses the order of the elements in a list *)
fun reverseOrder(nil) = nil
  | reverseOrder(head::tail) = reverseOrder(tail)@[head]; (* recursive call *)

(*
------------------------------------------------------------------------------
MODEL READER

modified from getModel.ml

The modified getModel generates a tuple of this type: 

  string list *               list of all atomic predicate names
  int list *                  list of all state numbers
  (int * int list) list *     list of arcs to next states for a state
  (int * int list) list *     list of true atomic predicates for a state
  (int * int list) list *     list of true subformulas indexes for a state

Duplicating the state number between the lists makes the model
easier to handle.
------------------------------------------------------------------------------
*)

fun fileToString fileName = let
  val stream = open_in fileName
  val str = input(stream, can_input stream)
  val _ = close_in stream
in str end;

fun fileToList fileName = let
  fun f fh = if end_of_stream fh then
    let val _ = close_in fh in nil end
    else (input_line fh)::(f fh)
in f(open_in fileName) end;

(* drops leading spaces *)
fun dropSpace nil   = nil
      |   dropSpace(h::t) = if h=" " then dropSpace t else h::t;
val skipSpace = implode o dropSpace o explode;

(* drops trailing new line *)
fun dropNL nil = nil
     |    dropNL(h::t) = if h="\n" then dropNL t else h::dropNL t;
val skipNL = implode o dropNL o explode;

(* drops all null strings from a list of strings *)
fun removeNull nil = nil
   |    removeNull(h::t) = if h="" then removeNull t else h::removeNull t;


(* gets rid of leading spaces, trailing newlines, and blank lines 
   from a list of strings where each string is a line. *)
val stripItDown = removeNull o map (skipNL o skipSpace);


val END = ~1;
val ATOMTOKS = [" ",","];

exception BadInput;

fun white(c) =
   c=" " orelse c="\n" orelse c="\t";

fun digit(c) =
   c >= "0" andalso c <= "9";

(* finds out if something is in a list *)
fun member x  nil  = false
      |   member x(h::t) = (x=h) orelse member x t;

(* returns the index, from zero, of the item if it is in the list.
   Otherwise, return ~1 *)
fun membernth x  nil  = ~1
      |   membernth x (h::t) = if (x=h) then 0 else 
         let val i = (membernth x t) in 
           if i = ~1 then ~1 else
              1 + i
end;

fun finishInt(i,s) = 
     (* return the integer whose first digits have value i and 
        whose remaining digits are found in s, up to the end or 
        the first white space *)
     if s="" then i
     else let val c = hd (explode(s))
          in if digit(c) then finishInt(10*i+ord(c)-ord("0"), substring(s, 1,size s-1))
             else i
          end;

fun getInt(s) = 
     (* get the first digit from string;
        return END if there is no integer *)
     if s="" then END
     else let val c = hd (explode(s))
          in  if digit(c) then finishInt(ord(c)-ord("0"), substring(s, 1,size s-1))
              else getInt(substring(s, 1,size s-1))
          end;

(* chop s into a list of strings separated by any of the chars in toks *)
fun token([], s) = (s, "")
    | token(toks, "") = ("", "")
    | token(toks, s) = 
        if member (substring(s, 0, 1)) toks then ("", substring(s, 1,size s-1))
             else let val (M,N) = token(toks, substring(s, 1,size s-1)) in
            ((substring(s,0,1))^M, N)
end;

     
fun tokenize [] s = [s]
    | tokenize toks "" = []
    | tokenize toks s = 
        let val (M,N) = token(toks, s) in 
           if M="" then (tokenize toks N) else
           M::(tokenize toks N)
end;

(* take list of lists and cats it together into just a list *)
fun flatten nil  = nil
      |   flatten(h::t) = h @ flatten t;

(* val k = map (tokenize[" ",","]) f; *)

(* these functions process a list of lists which represents the tokens
   on the individual lines of the model input file. They each read in a 
   different part of the model *)
fun makeAtomicList ((";"::xs)::xxs:string list list) = (["true"],xxs) (* "true" is true always and should be an atom *)
    | makeAtomicList (([])::xxs:string list list) = makeAtomicList(xxs)
    | makeAtomicList ((x::xs)::xxs:string list list) = 
          let val (M,N) = makeAtomicList( xs::xxs) in
	       (x::M, N)
end;
    
(* form an index list from the bitstring in the input file *)
fun makeAtomTrueList("", lastIndex) = [lastIndex]
    | makeAtomTrueList(y, index) =
        if substring(y,0,1) = "1" then
           index::makeAtomTrueList(substring(y, 1, size y-1), index+1)
        else if substring(y,0,1) = "0" then
           makeAtomTrueList(substring(y, 1, size y-1), index+1)
        else raise BadInput;

(* form an int list list from the successors in the input file-
   This is the structure of the model *)
fun makeNextList (nil) = ([], [])
    | makeNextList (x::xs) = 
        if (hd(explode(x)))= "#" then
            ([], x::xs)
        else let val (M,N) = makeNextList(xs) in 
            ((getInt(x)::M), N)
             end;

fun makeStateList (atoms, nil) = []
    | makeStateList (atoms, x::y::xs) = 
    if (hd(explode(x)))= "#" then
          let
            val state = getInt(x);
            val (trueAtomList) = makeAtomTrueList(y, 1); (* list of true atoms' indexes *)
            val (nextlist, rest) = makeNextList(xs);
          in
	    (state, trueAtomList, nextlist)::makeStateList(atoms, rest) (* recurse to next state *)
	  end
    else raise BadInput
    | makeStateList (atoms, "#END"::xs) = [] (* end recursion *)
    | makeStateList (atoms, _) = raise BadInput; (* catch all other cases *)


fun makeModel (("STATES"::xs)::xxs:string list list) = makeModel(xxs)
     | makeModel (("ARCS"::xs)::xxs) = makeModel(xxs)
     | makeModel (("ATOMIC"::xs)::xxs) = 
            let val (M,N) = makeAtomicList(xs::xxs);
	        val P = makeStateList(M,flatten N);
                val states = mapList(fn((x, _, _))=>(x), P); (* extract the states *)
                val nextStatesList = mapList(fn((x, _, y))=>(x, y), P); (* extract the states-next states list *)
	        val trueAtomList = mapList(fn((x, y, _))=>(x, y), P); (* extract the states-true atoms list *)
	        val trueFormulasList = mapList(fn(x, _, _)=>(x,[]), P); (* construct a states-empty true formulas list *)
             in
		(M, states, nextStatesList, trueAtomList, trueFormulasList) (* output the final model *)
end;

(*
------------------------------------------------------------------------------
FORMULA PARSER

The formula parser constructs a "tree" - a linked list of elements of the
following form:

  (int * string * int * int) list

The first int is the formula number, the string is the name of the
operator and the next two ints are the subformula indexes corresponding 
to the operands.

------------------------------------------------------------------------------
*)

(* exceptions *)
exception EXC_EXPECTED_ATOMIC;
exception EXC_EXPECTED_RPAREN;
exception EXC_EXPECTED_LPAREN;
exception EXC_EXPECTED_OPERATOR;
exception EXC_EXPECTED_OPERAND;

(* separates the first token as a char list from the rest of the list *)
fun getFirstToken(nil) = (nil, nil)  
  | getFirstToken([head]) = (* just one element *)
      if white(head) then (* and white *)
	(nil, nil)
      else
	([head], nil) (* and not white, return it *)
  | getFirstToken(item1::item2::tail) = (* at least two elements *)
      if white(item1) then
        getFirstToken(item2::tail) (* first white, call again *)
      else if (item1 = "~" orelse item1 = "(" orelse item1 = ")" orelse item2 = "(" orelse item2 = ")" orelse white(item2)) then
             ([item1], item2::tail) (* first non white, but separator, or second white - separate and continue *)
           else let 
	     val (elem1, elem2) = getFirstToken(item2::tail); (* first part of a token name, concatenate recursively *)
	   in
	     (item1::elem1, elem2) (* done, extract *)
	   end;

(* separates the input string into a list of tokens *)
fun doTokenize(nil) = nil
  | doTokenize(aString) =
      let
        val (head, tail) = getFirstToken(aString); (* separate the first token *)
      in
	if head=nil then 
	  nil (* got no tokens here! *)
	else
          implode(head)::doTokenize(tail) (* continue recursively, building a list *)
      end;

fun isBinaryOperator(oper) = 
  oper="AND" orelse oper="OR" orelse oper="AU" orelse oper="EU";

fun isUnaryOperator(oper) =
  oper="~"  orelse oper="AX" orelse oper="EX";

(* returns the first operand in a list of tokens and the rest of the list unchanged *)
fun getOperand(nil, _, _) = (* nothing given! *)
    raise EXC_EXPECTED_OPERAND
  | getOperand(")"::tail, 0, _) =
    raise EXC_EXPECTED_OPERAND
  | getOperand(")"::tail, 1, _) =
    ([")"], tail) (* end of subformula here - rparen, so return *)
  | getOperand(")"::tail, n, bool) =
    let
      val (left, right) = getOperand(tail, n-1, bool); (* recursive call for the tail, previous element index *)
    in
      (")"::left, right) (* end of subformula here - rparen *)
    end
  | getOperand("("::tail, n, _) =
    let  
      val (left, right) = getOperand(tail, n+1, false); (* recursive call for the tail, next element index *)
    in
      ("("::left, right) (* begin of subformula here - lparen *)
    end
  | getOperand(head::tail, 0, true) = (* the first case, first level in the tree - bool is true *)
    ([head], tail) (* build a list with the head and also return the tail *)
  | getOperand(head::tail, n, _) =
    let
      val (left, right) = getOperand(tail, n, false); (* recursive call for the tail *)
    in
      (head::left, right) (* concatenate the result *)
    end;

(* separates a formula in operator operand1 operand2 *)
fun separateFormula([a], atomicList) =
  if isListMember(a, atomicList) then (* begins with an atomic *)
    ("", [a], nil)
  else
    (print(a); raise EXC_EXPECTED_ATOMIC)
  | separateFormula("("::operator::tail, _) = (* begins with a lparen *)
  if isUnaryOperator(operator) then (* lparen followed by a unary operator *)
    let
      val (operand1, tail1) = getOperand(tail, 0, true); (* get the operand this operator is applied to *)
    in
      if tail1 <> [")"] then
        (print(implode(tail1)); raise EXC_EXPECTED_RPAREN) (* subformula doesn't end with a rparen *)
      else
        (operator, operand1, nil)
    end
  else 
    if isBinaryOperator(operator) then (* lparen followed by a binary operator *)
      let
        val (operand1, tail1) = getOperand(tail, 0, true); (* get the 1st operand *)
        val (operand2, tail2) = getOperand(tail1, 0, true); (* get the 2nd operand *)
      in
        if tail2 <> [")"] then
	  (print(implode(tail2)); raise EXC_EXPECTED_RPAREN) (* subformula doesn't end with a rparen *)
        else
          (operator, operand1, operand2) (* return the separateed formula *)
      end
    else
      (print(operator); raise EXC_EXPECTED_OPERATOR) (* didn't get an operator after the lparen *)
  | separateFormula(illFormed, _) = (* catch any other cases that don't begin with a lparen *)
  (print(implode(illFormed)); raise EXC_EXPECTED_LPAREN);

(* parses a formula and builds a tree *)
fun parseFormula(nil, _, _) = (* nothing given! *)
    nil
  | parseFormula(formula, atomicList, n) = (* given a formula, the atomics and a restart value *)
  let
    val (operator, operand1, operand2) = separateFormula(formula, atomicList); (* separate it in parts *)
  in
    if not(operator = "") then (* we got an operator *)
      let
	val leftBranch = parseFormula(operand1, atomicList, n+1); (* recurse for the left branch *)
	val leftLength = length(leftBranch);
	val rightBranch = parseFormula(operand2, atomicList, n+leftLength+1); (* recurse for the right branch *)
	val restartIndex =
	  if isUnaryOperator(operator) then
	    ~1 (* done, no need to restart *)
	  else
	    n+leftLength+1 (* restart at the end of the leftBranch in the tree *)
      in
	(n, operator, (n+1, restartIndex))::leftBranch@rightBranch (* catenate it to build the tree *)
      end
    else (* it was actually an atomic *)
      [(n, operator, (indexInList(hd(operand1), atomicList), ~1))] (* return a leaf node here *)
  end;

(*
------------------------------------------------------------------------------
FORMULA TRUTH VALUE EVALUATOR

Contains functions to explore the tree built by the parser for the formula,
implementing Clarke's model checker.
------------------------------------------------------------------------------
*)

(* exceptions *)
exception EXC_EVALUATE_ERROR;

(* evaluates the truth value of an atomic in the states list and puts result in formulas list for each state *)
fun evaluateATOMIC(formula, atomic, nil, model) = model (* end of states list and of recursion *)
  | evaluateATOMIC(formula, atomic, start::tail, model) =
      let
	val newModel = evaluateATOMIC(formula, atomic, tail, model); (* recursively evaluate the tail for the next state *)
      in
        if isListMember(atomic, getList(start, #4model)) then (* if atomic is member in the true atomics list *)
          let
            val newList = setList(start, #5newModel, formula::getList(start, #5newModel)) (* construct a new label list *)
          in
	    (#1model, #2model, #3model, #4model, newList) (* set the corresponding labels *)
          end 
      else
	newModel (* or return the previous result, with no labels set *)
      end;

(* evaluates the truth value of an AX formula in the states list and puts result in formulas list for each state *)
fun evaluateAX(formula, atomic1, nil, model) = model (* end of states list and of recursion *)
  | evaluateAX(formula, atomic1, start::tail, model) =
      let
        val newModel = evaluateAX(formula, atomic1, tail, model); (* recurse for the next state *)
        val newStates = getList(start, #3model); (* create a new states list *)
        val newLabels = mapList(fn(x)=>getList(x, #5model), newStates); (* appply the mapping to get a new labels list *)
        val newMembers = mapList(fn(x)=>isListMember(atomic1, x), newLabels); (* create a list of truth values for the labels *)
      in
        if reduce(myAND, newMembers, true) then (* apply AND to get the truth value *)
          let
            val newList = setList(start, #5newModel, formula::getList(start, #5newModel)) (* construct a new label list *)
          in
            (#1model, #2model, #3model, #4model, newList) (* set the corresponding labels *)
          end
      else
	newModel (* or return the previous result, with no labels set *)
      end;

(* evaluates the truth value of an EX formula in the states list and puts result in formulas list for each state *)
fun evaluateEX(formula, atomic, nil, model) = model (* end of states list and of recursion *)
  | evaluateEX(formula, atomic, start::tail, model) =
      let
        val newModel = evaluateEX(formula, atomic, tail, model); (* recursively evaluate the tail for the next state *)
        val newStates = getList(start, #3model); (* create a new states list *)
        val newLabels = mapList(fn(x)=>getList(x, #5model), newStates); (* appply the mapping to get a new labels list *)
        val newMembers = mapList(fn(x)=>isListMember(atomic, x), newLabels); (* create a list of truth values for the labels *)
      in
        if reduce(myOR, newMembers, true) then (* apply OR to get the truth value *)
          let
            val newList = setList(start, #5newModel, formula::getList(start, #5newModel)) (* construct a new label list *)
          in
            (#1model, #2model, #3model, #4model, newList) (* set the corresponding labels *)
          end
      else
        newModel (* or return the previous result, with no labels set *)
      end;

(* evaluates the truth value of a NOT formula in the states list and puts result in formulas list for each state *)
fun evaluateNOT(formula, atomic, nil, model) = model (* end of states list and of recursion *)
  | evaluateNOT(formula, atomic, start::tail, model) =
      let
        val newModel = evaluateNOT(formula, atomic, tail, model); (* recursively evaluate the tail for the next state *)
      in
        if not(isListMember(atomic, getList(start, #5model))) then (* if "negated atomic" is not member in the true formulas list *)
          let
            val newList = setList(start, #5newModel, formula::getList(start, #5newModel)) (* construct a new label list *)
          in
            (#1model, #2model, #3model, #4model, newList) (* set the corresponding labels *)
          end
      else
        newModel (* or return the previous result, with no labels set *)
      end;

(* evaluates the truth value of an OR formula in the states list and puts result in formulas list for each state *)
fun evaluateOR(formula, atomic1, atomic2, nil, model) = model (* end of states list and of recursion *)
  | evaluateOR(formula, atomic1, atomic2, start::tail, model) =
      let
        val newModel = evaluateOR(formula, atomic1, atomic2, tail, model); (* recursively evaluate the tail for the next state *)
      in
        if isListMember(atomic1, getList(start, #5model)) orelse isListMember(atomic2, getList(start, #5model)) then
          let
            val newList = setList(start, #5newModel, formula::getList(start, #5newModel)) (* construct a new label list *)
          in
            (#1model, #2model, #3model, #4model, newList) (* set the corresponding labels *)
          end
      else   
        newModel (* or return the previous result, with no labels set *)
      end;   
  
(* evaluates the truth value of an AND formula in the states list and puts result in formulas list for each state *)
fun evaluateAND(formula, atomic1, atomic2, nil, model) = model (* end of states list and of recursion *)
  | evaluateAND(formula, atomic1, atomic2, start::tail, model) =
      let
        val newModel = evaluateAND(formula, atomic1, atomic2, tail, model); (* recursively evaluate the tail for the next state *)
      in
        if isListMember(atomic1, getList(start, #5model)) andalso isListMember(atomic2, getList(start, #5model)) then
          let
            val newList = setList(start, #5newModel, formula::getList(start, #5newModel)) (* construct a new label list *)
          in
            (#1model, #2model, #3model, #4model, newList) (* set the corresponding labels *)
          end
      else   
        newModel (* or return the previous result, with no labels set *)
      end;   
  
(* mutually recursive functions for depth search *)
fun depthAU(formula, atomic1, atomic2, start, nil, model, markList) =
      ((#1model, #2model, #3model, #4model, setList(start, #5model, formula::getList(start, #5model))), markList, true)
  | depthAU(formula, atomic1, atomic2, start, head::tail, model, markList) =
      let
	val (newModel, newMarkList, bool) = doAU(formula, atomic1, atomic2, head, model, markList); (* evaluate the formula for the current state *)
      in
	if not(bool) then(* found a false formula! *)
	  (newModel, newMarkList, false) (* one false value, end of recursion *)
	else
	  depthAU(formula, atomic1, atomic2, start, tail, newModel, newMarkList) (* continue recursion with next state *)
      end
and doAU(formula, atomic1, atomic2, start, model, markList) = 
  if getList(start, markList) then
    if isListMember(formula, getList(start, #5model)) then (* check if subformula is true in this state *)
      (model, markList, true) (* end of recursion, subformula is true *)
    else
      (model, markList, false) (* end of recursion, subformula is false *)
  else if isListMember(atomic2, getList(start, #5model)) then (* check if atomic2 is true in this state *)
          let
            val newList = setList(start, #5model, formula::getList(start, #5model)) (* construct a new label list *)
          in
            ((#1model, #2model, #3model, #4model, newList), setList(start, markList, true), true) (* return to higher level *)
          end
  else if isListMember(atomic1, getList(start, #5model)) then (* check if atomic1 is true in this state *)
    depthAU(formula, atomic1, atomic2, start, getList(start, #3model), model, setList(start, markList, true)) (* propagate to neighbor states *)
  else
    (model, setList(start, markList, true), false); (* both atomics are false, end of recursion *)

fun evaluateAU(_, _, _, nil, model, _) = model (* end of states list and of recursion *)
  | evaluateAU(formula, atomic1, atomic2, head::tail, model, markList) =
      if getList(head, markList) then (* head state is already marked *)
        evaluateAU(formula, atomic1, atomic2, tail, model, markList) (* recursively evaluate the tail for the next state *)
      else
        let
          val (newModel, newMarkList, _) = doAU(formula, atomic1, atomic2, head, model, markList) (* mark the head *)
        in
          evaluateAU(formula, atomic1, atomic2, tail, newModel, newMarkList) (* recursively evaluate the tail for the next state *)
        end;

(* mutually recursive functions for depth search *)
fun depthEU(formula, atomic1, atomic2, start, nil, model, markList) =
      (model, markList, false)
  | depthEU(formula, atomic1, atomic2, start, head::tail, model, markList) =
      let
        val (newModel, newMarkList, bool) = doEU(formula, atomic1, atomic2, head, model, markList); (* evaluate the formula for the current state *)
      in
        if bool then (* found a true formula! *)
          let
            val newList = setList(start, #5newModel, formula::getList(start, #5newModel)); (* construct a new label list *)
          in
            ((#1newModel, #2newModel, #3newModel, #4newModel, newList), newMarkList, true) (* return the list into a new model, end of recursion *)
          end
        else
          depthEU(formula, atomic1, atomic2, start, tail, newModel, newMarkList) (* continue recursion with next state *)
      end
and doEU(formula, atomic1, atomic2, start, model, markList) =
  if getList(start, markList) then
    if isListMember(formula, getList(start, #5model)) then (* check if subformula is true in this state *)
      (model, markList, true) (* end of recursion, subformula is true *)
    else
      (model, markList, false) (* end of recursion, subformula is false *)
  else if isListMember(atomic2, getList(start, #5model)) then (* check if atomic2 is true in this state *)
    let
      val newList = setList(start, #5model, formula::getList(start, #5model)) (* construct a new label list *)
    in
      ((#1model, #2model, #3model, #4model, newList), setList(start, markList, true), true) (* return the list into a new model, end of recursion *)
    end
  else if isListMember(atomic1, getList(start, #5model)) then (* check if atomic1 is true in this state *)
    depthEU(formula, atomic1, atomic2, start, getList(start, #3model), model, setList(start, markList, true)) (* propagate to neighbor states *)
  else
    (model, setList(start, markList, true), false); (* both atomics are false, end of recursion *)

fun evaluateEU(_, _, _, nil, model, _) = model (* end of states list and of recursion *)
  | evaluateEU(formula, atomic1, atomic2, head::tail, model, markList) =
      if getList(head, markList) then (* head state is already marked *)
        evaluateEU(formula, atomic1, atomic2, tail, model, markList) (* recursively evaluate the tail for the next state *)
      else
        let
          val (newModel, newMarkList, _) = doEU(formula, atomic1, atomic2, head, model, markList);
        in
          evaluateEU(formula, atomic1, atomic2, tail, newModel, newMarkList) (* recursively evaluate the tail for the next state *)
        end;

(* evaluates all the subformulae in the tree generated by parsing the fromula *)
fun evaluateFormula(nil, model) = model
  | evaluateFormula((formula, "", (atomic, _))::tail, model) =
      evaluateFormula(tail, evaluateATOMIC(formula, atomic, #2model, model)) (* recursive call to evaluate tail subformula *)
  | evaluateFormula((formula, "~", (atomic, _))::tail, model) = 
      evaluateFormula(tail, evaluateNOT(formula, atomic, #2model, model)) (* recursive call to evaluate tail subformula *)
  | evaluateFormula((formula, "AX", (atomic, _))::tail, model) =
      evaluateFormula(tail, evaluateAX(formula, atomic, #2model, model)) (* recursive call to evaluate tail subformula *)
  | evaluateFormula((formula, "EX", (atomic, _))::tail, model) =
      evaluateFormula(tail, evaluateEX(formula, atomic, #2model, model)) (* recursive call to evaluate tail subformula *)
  | evaluateFormula((formula, "OR", (atomic1, atomic2))::tail, model) =
      evaluateFormula(tail, evaluateOR(formula, atomic1, atomic2, #2model, model)) (* recursive call to evaluate tail subformula *)
  | evaluateFormula((formula, "AND", (atomic1, atomic2))::tail, model) =
      evaluateFormula(tail, evaluateAND(formula, atomic1, atomic2, #2model, model)) (* recursive call to evaluate tail subformula *)
  | evaluateFormula((formula, "AU", (atomic1, atomic2))::tail, model) =
      let
        val markList = mapList(fn(x)=>(x, false), #2model) (* generate a list of state * false pairs *)
      in 
        evaluateFormula(tail, evaluateAU(formula, atomic1, atomic2, #2model, model, markList)) (* recursive call to evaluate tail subformula *)
      end
  | evaluateFormula((formula, "EU", (atomic1, atomic2))::tail, model) =
      let
        val markList = mapList(fn(x)=>(x, false), #2model) (* generate a list of state * false pairs *)
      in 
        evaluateFormula(tail, evaluateEU(formula, atomic1, atomic2, #2model, model, markList)) (* recursive call to evaluate tail subformula *)
      end
  | evaluateFormula(_, _) = 
	raise EXC_EVALUATE_ERROR; (* catch all the other cases *)

(* clears the labels list for all the states *)
fun resetLabels((atomics, states, stateArcs, stateAtomics, stateLabels)) =
  let
    val emptyLabels = mapList(fn(x)=>(x,[]), states) (* generate a list of state * empty list pairs *)
  in
    ((atomics, states, stateArcs, stateAtomics, emptyLabels))
  end;

(* evaluates a formula passed as a string *)
fun evaluateStringFormula(stringFormula, model) = 
    let
      val cleanModel = resetLabels(model); (* clear the labels *)
      val formula = doTokenize(explode(stringFormula)); (* get the next command, tokenized *)
      val newModel = evaluateFormula(reverseOrder(parseFormula(formula, #1cleanModel, 1)), cleanModel); (* evaluate it *)
      val first = 0; (* dummy first state number *)
    in
     if not(formula = nil) then
       (
        print("Model checker\n");
        print(stringFormula);
        print(" : ");
        print(isListMember(1, getList(first, #5newModel)));
        print("\nDone evaluating.\n")
       )
     else
       print("ERROR!\n")
    end;

(* creates a model from an input file *)
fun createModel(modelFileName) = makeModel (map(tokenize ATOMTOKS)(stripItDown(fileToList(modelFileName))));

(* reads formulas from the file and evaluates them *)
fun evaluateFormulas(model, file) =
  if end_of_stream(file) then
    print("Done evaluating.\n")
  else
    let
      val cleanModel = resetLabels(model); (* clear the labels *)
      val formula = doTokenize(makeListFromInput(file)); (* get the next command, tokenized *)
      val newModel = evaluateFormula(reverseOrder(parseFormula(formula, #1cleanModel, 1)), cleanModel); (* evaluate it *)
      val first = 0; (* dummy first state number *)
    in
     if not(formula = nil) then
       (
        print(implode(formula));
        print(" : ");
        print(isListMember(1, getList(first, #5newModel)));
        print("\n");
        evaluateFormulas(model, file) (* recursive call to get the next formula in the file *)
       )
     else
       print("Done evaluating.\n")
    end;

(*
------------------------------------------------------------------------------
MAIN FUNCTION

This just calls the read model and evaluate formulas functions.
------------------------------------------------------------------------------
*)

(* evaluates formulas in file formulaFileName in the model constructed from the file formulaFileName *)
fun main(modelFileName, formulaFileName) = 
  let
    val model = makeModel (map(tokenize ATOMTOKS)(stripItDown(fileToList(modelFileName))));
  in
    (
    print("Model checker\n");
    evaluateFormulas(model, open_in(formulaFileName))
    )
  end;