src/HOL/Modelcheck/MuCalculus.ML
author paulson
Mon, 29 Sep 1997 11:46:33 +0200
changeset 3729 6be7cf5086ab
parent 3210 e80db1660614
child 3818 5a1116b69196
permissions -rw-r--r--
Renamed XA, XB to PA, PB and removed the certificate from Client Verify
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
3210
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
     1
(*  Title:      HOL/Modelcheck/MuCalculus.ML
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
     2
    ID:         $Id$
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
     3
    Author:     Olaf Mueller, Jan Philipps, Robert Sandner
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
     4
    Copyright   1997  TU Muenchen
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
     5
*)
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
     6
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
     7
exception MCOracleExn of term;
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
     8
exception MCFailureExn of string;
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
     9
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
    10
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
    11
val trace_mc = ref false;
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
    12
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
    13
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
    14
fun termtext sign term =
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
    15
  setmp print_mode ["Eindhoven"]
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
    16
    (Sign.string_of_term sign) term;
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
    17
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
    18
fun call_mc s =
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
    19
  execute ( "echo \"" ^ s ^ "\" | pmu -w" );
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
    20
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
    21
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
    22
fun mk_mc_oracle (sign, MCOracleExn trm) =
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
    23
  let
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
    24
    val tmtext = termtext sign trm;
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
    25
    val debug = writeln ("MC debugger: " ^ tmtext);
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
    26
    val result = call_mc tmtext;
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
    27
  in
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
    28
    if ! trace_mc then
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
    29
      (writeln tmtext; writeln("----"); writeln result)
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
    30
    else ();
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
    31
    (case result of
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
    32
      "TRUE\n"  =>  trm |
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
    33
      "FALSE\n" => (error "MC oracle yields FALSE") |
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
    34
    _ => (error ("MC syntax error: " ^ result)))
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
    35
  end;