Theory Munta_Compile_MLton

section ‹Build and Test Exported Program With MLton›
text_raw ‹\label{build-mlton}›

theory Munta_Compile_MLton
  imports Munta_Model_Checker.Simple_Network_Language_Export_Code
begin

― ‹Produces a command for checking a single benchmark, e.g.:
▩‹./check_benchmark.sh 568 "Property is not satisfied" ./munta -m benchmarks/PM_all_5.muntax›
›
ML ‹
fun mk_benchmark_check_gen munta mk_prop name num_states satisfied =
  let
    val prop = mk_prop satisfied
    val benchmark = name ^ ".muntax"
  in
    ― ‹this line checks that number of states and property satisfaction are correct›
    "./check_benchmark.sh " ^ string_of_int num_states ^ " " ^ prop
    ― ‹this line runs Munta on the actual benchmark›
    ^ " " ^ munta ^ " " ^ benchmark
  end
val mk_benchmark_check =
  mk_benchmark_check_gen "./munta -m"
    (fn satisfied =>
      if satisfied then
        ▩‹"Property is satisfied!"›
      else
        ▩‹"Property is not satisfied!"›)
val mk_benchmark_check_dc =
  mk_benchmark_check_gen "./munta -dc -m"
    (fn satisfied =>
      if satisfied then
        ▩‹"Model has a deadlock!"›
      else
        ▩‹"Model has no deadlock!"›)
val it  = mk_benchmark_check "PM_all_5" 568 false
val it1 = mk_benchmark_check_dc "hddi_08" 466 false
›

text ‹Here is how to compile Munta with MLton and then run some benchmarks:›

― ‹Commenting this out since the AFP submission machine sandboxing somehow breaks MLton.›
compile_generated_files "code/Simple_Model_Checker.ML" (in Simple_Network_Language_Export_Code)
  external_files
    ‹Unsynchronized.sml›
    ‹Writeln.sml›
    ‹Util.sml›
    ‹Muntax.sml›
    ‹Mlton_Main.sml›
    ‹library.ML›
    ‹muntax.mlb›
    ‹check_benchmark.sh›
    (in "../ML")
  and
    ‹HDDI_02.muntax›
    ‹HDDI_02_broadcast.muntax›
    ‹HDDI_08_broadcast.muntax›
    ‹PM_all_1.muntax›
    ‹PM_all_2.muntax›
    ‹PM_all_3.muntax›
    ‹PM_all_4.muntax›
    ‹PM_all_5.muntax›
    ‹PM_all_6.muntax›
    ‹PM_all_urgent.muntax›
    ‹bridge.muntax›
    ‹csma_05.muntax›
    ‹csma_06.muntax›
    ‹fischer.muntax›
    ‹fischer_05.muntax›
    ‹hddi_08.muntax›
    ‹light_switch.muntax› (in "../benchmarks")
  export_files ‹munta› (exe)
  where ‹fn dir =>
    let
      val exec = Generated_Files.execute dir
      val _ =
        exec ‹Preparation›
          "mv code/Simple_Model_Checker.ML Simple_Model_Checker.ML"
      val _ =
        exec ‹Compilation›
          (⌦‹▩‹"$ISABELLE_MLTON" $ISABELLE_MLTON_OPTIONS› ^›
           ▩‹"$ISABELLE_MLTON" › ^
            ― ‹these additional settings have been copied from the AFP entry ‹PAC_Checker››
            ― ‹they bring down ‹benchmarks/PM_all_6.muntax› from 1000 s to 180 s on an M1 Mac›
             "-const 'MLton.safe false' -verbose 1 -inline 700 -cc-opt -O3 " ^
            ― ‹this one from ‹PAC_Checker› does not work on ARM64 though›
            ⌦‹"-codegen native " ^›
            ― ‹these used to be the only setting for Munta›
            "-default-type int64 " ^
            "-output munta " ^
            "muntax.mlb")
      val _ = exec ‹Test HDDI_02› (mk_benchmark_check "HDDI_02" 34 false)
      val _ = exec ‹Test HDDI_02_broadcast› (mk_benchmark_check "HDDI_02_broadcast" 34 false)
      val _ = exec ‹Test HDDI_08_broadcast› (mk_benchmark_check "HDDI_08_broadcast" 466 false)
      val _ = exec ‹Test PM_all_1› (mk_benchmark_check "PM_all_4" 529 false)
      val _ = exec ‹Test PM_all_1› (mk_benchmark_check "PM_all_1" 338 false)
      val _ = exec ‹Test PM_all_2› (mk_benchmark_check "PM_all_2" 2828 false)
      val _ = exec ‹Test PM_all_3› (mk_benchmark_check "PM_all_3" 3994 false)
      val _ = exec ‹Test PM_all_4› (mk_benchmark_check "PM_all_4" 529 false)
      val _ = exec ‹Test PM_all_5› (mk_benchmark_check "PM_all_5" 568 false)
      ― ‹180 s on an M1 Mac›
      ⌦‹val _ = exec ‹Test PM_all_6› (mk_benchmark_check "PM_all_6" 416245 false)›
      val _ = exec ‹Test PM_all_urgent› (mk_benchmark_check "PM_all_urgent" 8 true)
      val _ = exec ‹Test bridge› (mk_benchmark_check "bridge" 73 true)
      val _ = exec ‹Test csma_05› (mk_benchmark_check "csma_05" 8217 false)
      val _ = exec ‹Test csma_06› (mk_benchmark_check "csma_06" 68417 false)
      val _ = exec ‹Test fischer› (mk_benchmark_check "fischer" 4500 true)
      val _ = exec ‹Test fischer_05› (mk_benchmark_check "fischer_05" 38579 false)
      val _ = exec ‹Test hddi_08› (mk_benchmark_check "hddi_08" 466 false)
      val _ = exec ‹Test light_switch› (mk_benchmark_check "light_switch" 2 true)
      ― ‹a test for the deadlock checker›
      val _ = exec ‹Test hddi_08› (mk_benchmark_check_dc "hddi_08" 466 false)
    in () end›

end