3210
|
1 |
(* Title: HOL/Modelcheck/MuCalculus.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Olaf Mueller, Jan Philipps, Robert Sandner
|
|
4 |
Copyright 1997 TU Muenchen
|
|
5 |
*)
|
|
6 |
|
|
7 |
exception MCOracleExn of term;
|
|
8 |
exception MCFailureExn of string;
|
|
9 |
|
|
10 |
|
|
11 |
val trace_mc = ref false;
|
|
12 |
|
|
13 |
|
|
14 |
fun termtext sign term =
|
|
15 |
setmp print_mode ["Eindhoven"]
|
|
16 |
(Sign.string_of_term sign) term;
|
|
17 |
|
|
18 |
fun call_mc s =
|
|
19 |
execute ( "echo \"" ^ s ^ "\" | pmu -w" );
|
|
20 |
|
|
21 |
|
|
22 |
fun mk_mc_oracle (sign, MCOracleExn trm) =
|
|
23 |
let
|
|
24 |
val tmtext = termtext sign trm;
|
|
25 |
val debug = writeln ("MC debugger: " ^ tmtext);
|
|
26 |
val result = call_mc tmtext;
|
|
27 |
in
|
|
28 |
if ! trace_mc then
|
|
29 |
(writeln tmtext; writeln("----"); writeln result)
|
|
30 |
else ();
|
|
31 |
(case result of
|
|
32 |
"TRUE\n" => trm |
|
|
33 |
"FALSE\n" => (error "MC oracle yields FALSE") |
|
|
34 |
_ => (error ("MC syntax error: " ^ result)))
|
|
35 |
end;
|