src/HOL/Modelcheck/MuCalculus.ML
author paulson
Tue Jun 28 15:27:45 2005 +0200 (2005-06-28)
changeset 16587 b34c8aa657a5
parent 14980 267cc670317a
permissions -rw-r--r--
Constant "If" is now local
mueller@3210
     1
(*  Title:      HOL/Modelcheck/MuCalculus.ML
mueller@3210
     2
    ID:         $Id$
mueller@3210
     3
    Author:     Olaf Mueller, Jan Philipps, Robert Sandner
mueller@3210
     4
    Copyright   1997  TU Muenchen
mueller@3210
     5
*)
mueller@3210
     6
mueller@3210
     7
exception MCOracleExn of term;
mueller@3210
     8
exception MCFailureExn of string;
mueller@3210
     9
mueller@3210
    10
mueller@3210
    11
val trace_mc = ref false;
mueller@3210
    12
wenzelm@3818
    13
local
mueller@3210
    14
mueller@3210
    15
fun termtext sign term =
wenzelm@14980
    16
  setmp print_mode ["Eindhoven"] (Sign.string_of_term sign) term;
mueller@3210
    17
mueller@3210
    18
fun call_mc s =
mueller@3210
    19
  execute ( "echo \"" ^ s ^ "\" | pmu -w" );
mueller@3210
    20
wenzelm@3818
    21
in
mueller@3210
    22
mueller@3210
    23
fun mk_mc_oracle (sign, MCOracleExn trm) =
mueller@3210
    24
  let
mueller@3210
    25
    val tmtext = termtext sign trm;
mueller@3210
    26
    val debug = writeln ("MC debugger: " ^ tmtext);
mueller@3210
    27
    val result = call_mc tmtext;
mueller@3210
    28
  in
mueller@3210
    29
    if ! trace_mc then
mueller@3210
    30
      (writeln tmtext; writeln("----"); writeln result)
mueller@3210
    31
    else ();
mueller@3210
    32
    (case result of
mueller@3210
    33
      "TRUE\n"  =>  trm |
mueller@3210
    34
      "FALSE\n" => (error "MC oracle yields FALSE") |
mueller@3210
    35
    _ => (error ("MC syntax error: " ^ result)))
mueller@3210
    36
  end;
wenzelm@3818
    37
wenzelm@3818
    38
end;