src/HOL/Modelcheck/EindhovenSyn.thy
author paulson
Tue Jun 28 15:27:45 2005 +0200 (2005-06-28)
changeset 16587 b34c8aa657a5
parent 7295 fe09a0c5cebe
child 17272 c63e5220ed77
permissions -rw-r--r--
Constant "If" is now local
mueller@6466
     1
(*  Title:      HOL/Modelcheck/EindhovenSyn.thy
mueller@6466
     2
    ID:         $Id$
mueller@6466
     3
    Author:     Olaf Mueller, Jan Philipps, Robert Sandner
mueller@6466
     4
    Copyright   1997  TU Muenchen
mueller@6466
     5
*)
mueller@6466
     6
mueller@6466
     7
EindhovenSyn = MuCalculus + 
mueller@6466
     8
  
mueller@6466
     9
mueller@6466
    10
syntax (Eindhoven output)
mueller@6466
    11
mueller@6466
    12
  True		:: bool					("TRUE")
mueller@6466
    13
  False		:: bool					("FALSE")
mueller@6466
    14
mueller@6466
    15
  Not		:: bool => bool				("NOT _" [40] 40)
mueller@6466
    16
  "op &"	:: [bool, bool] => bool			(infixr "AND" 35)
mueller@6466
    17
  "op |"	:: [bool, bool] => bool			(infixr "OR" 30)
mueller@6466
    18
mueller@6466
    19
  "! " 		:: [idts, bool] => bool			("'((3A _./ _)')" [0, 10] 10)
mueller@6466
    20
  "? "		:: [idts, bool] => bool			("'((3E _./ _)')" [0, 10] 10)
mueller@6466
    21
  "ALL " 	:: [idts, bool] => bool			("'((3A _./ _)')" [0, 10] 10)
mueller@6466
    22
  "EX "		:: [idts, bool] => bool			("'((3E _./ _)')" [0, 10] 10)
mueller@6466
    23
   "_lambda"	:: [pttrns, 'a] => 'b			("(3L _./ _)" 10)
mueller@6466
    24
mueller@6466
    25
  "_idts"     	:: [idt, idts] => idts		        ("_,/_" [1, 0] 0)
mueller@6466
    26
  "_pattern"    :: [pttrn, patterns] => pttrn     	("_,/_" [1, 0] 0)
mueller@6466
    27
mueller@6466
    28
  "Mu "		:: [idts, 'a pred] => 'a pred		("(3[mu _./ _])" 1000)
mueller@6466
    29
  "Nu "		:: [idts, 'a pred] => 'a pred		("(3[nu _./ _])" 1000)
mueller@6466
    30
mueller@6466
    31
oracle
mueller@6466
    32
  eindhoven_mc = mk_eindhoven_mc_oracle
mueller@6466
    33
mueller@6466
    34
end
mueller@6466
    35
mueller@6466
    36
mueller@6466
    37
mueller@6466
    38
ML
mueller@6466
    39
mueller@6466
    40
mueller@6466
    41
exception EindhovenOracleExn of term;
mueller@6466
    42
mueller@6466
    43
mueller@6466
    44
val trace_mc = ref false;
mueller@6466
    45
mueller@6466
    46
local
mueller@6466
    47
mueller@6466
    48
fun termtext sign term =
mueller@6466
    49
  setmp print_mode ["Eindhoven"]
mueller@6466
    50
    (Sign.string_of_term sign) term;
mueller@6466
    51
mueller@6466
    52
fun call_mc s =
wenzelm@7295
    53
  let
wenzelm@7295
    54
    val eindhoven_home = getenv "EINDHOVEN_HOME";
wenzelm@7295
    55
    val pmu =
wenzelm@7295
    56
      if eindhoven_home = "" then error "Environment variable EINDHOVEN_HOME not set"
wenzelm@7295
    57
      else eindhoven_home ^ "/pmu";
wenzelm@7295
    58
  in execute ("echo \"" ^ s ^ "\" | " ^ pmu ^ " -w") end;
mueller@6466
    59
mueller@6466
    60
in
mueller@6466
    61
mueller@6466
    62
fun mk_eindhoven_mc_oracle (sign, EindhovenOracleExn trm) =
mueller@6466
    63
  let
mueller@6466
    64
    val tmtext = termtext sign trm;
mueller@6466
    65
    val debug = writeln ("MC debugger: " ^ tmtext);
mueller@6466
    66
    val result = call_mc tmtext;
mueller@6466
    67
  in
mueller@6466
    68
    if ! trace_mc then
mueller@6466
    69
      (writeln tmtext; writeln("----"); writeln result)
mueller@6466
    70
    else ();
mueller@6466
    71
    (case result of
mueller@6466
    72
      "TRUE\n"  =>  trm |
mueller@6466
    73
      "FALSE\n" => (error "MC oracle yields FALSE") |
mueller@6466
    74
    _ => (error ("MC syntax error: " ^ result)))
mueller@6466
    75
  end;
mueller@6466
    76
mueller@6466
    77
end;