TYPE

  ParityFlattened = flat(str)
  BoolFlattened = flat(bool)
  State          = Var -> ParityFlattened

PROBLEM Parity

  direction  : forward
  carrier    : State
  init       : bot
  init_start : [-> top]
  combine    : mylub


TRANSFER

  // in assignments calculate the new value of the variable and add it to the state
  ASSIGN(variable, expression) = if (@=bot) then bot else
      @\[variable -> evalAExp(expression, @)] endif

  // test conditions
  IF(expression), true_edge = branch(expression,@,true)
  IF(expression), false_edge = branch(expression,@,false)

  // loop conditions
  WHILE(expression), true_edge = branch(expression,@,true)  
  WHILE(expression), false_edge = branch(expression,@,false)

SUPPORT

  mylub :: State * State -> State
  mylub(e1,e2) = e1 lub e2

  evalAExp :: Expression * State -> ParityFlattened
  evalAExp(expression, state) =
    case expType(expression) of
      "ARITH_BINARY" => case expOp(expression) of
        "+" => let valLeft  <= evalAExp(expSubLeft(expression),  state),
                   valRight <= evalAExp(expSubRight(expression), state) in
                 lift(if (valLeft=valRight) then "even" else "odd" endif);
        "-" => let valLeft  <= evalAExp(expSubLeft(expression),  state),
                   valRight <= evalAExp(expSubRight(expression), state) in
                 lift(if (valLeft=valRight) then "even" else "odd" endif);
        "*" => let valLeft  = evalAExp(expSubLeft(expression),  state),
                   valRight = evalAExp(expSubRight(expression), state) in
                 if (valLeft=bot || valRight=bot) then bot
                   else if (valLeft=lift("even") || valRight = lift("even")) then lift("even") 
                   else if (valLeft=lift("odd") && valRight = lift("odd")) then lift("odd") 
                   else top endif endif endif;
        "/" => let valLeft  <= evalAExp(expSubLeft(expression),  state),
                   valRight <= evalAExp(expSubRight(expression), state) in
                 top;
        endcase;
      "ARITH_UNARY" =>
	case expOp(expression) of
          "-" => evalAExp(expSub(expression), state);
        endcase;
      "VAR"   => state(expVar(expression));
      "CONST" => lift(if (expVal(expression)%2=0) then "even" else "odd" endif);
      _       => error("Runtime Error: evalAExp applied to nonarithmetic Expression");
    endcase

evalBExp :: Expression * State -> BoolFlattened
   evalBExp(expression,state) = 
     case expType(expression) of 
       "TRUE" => lift(true);
       "FALSE" => lift(false);
       "BOOL_UNARY" => let value <= evalBExp(expSub(expression), state) in lift(!value);
       "BOOL_BINARY" => case expOp(expression) of
	        "=" => let valLeft  <= evalAExp(expSubLeft(expression),  state),
                    valRight <= evalAExp(expSubRight(expression), state) in
             if (valLeft=valRight) then top else lift(false) endif;
         "<>" => let valLeft <= evalAExp(expSubLeft(expression),  state),
                    valRight <= evalAExp(expSubRight(expression), state) in
                   if (valLeft!=valRight) then lift(true) else top endif;
         _ => top;
         endcase;
       _ => top;
     endcase

   branch :: Expression * State * bool -> State
   branch(expression, state, edge) = let valexp = evalBExp(expression,state) in 
      if (valexp != bot && (valexp = top || drop(valexp) = edge)) then state else bot endif