The following code require imandra-tools installed on the build switch and where imandra-merlin and imandra are running:
[@@@require "imandra-tools"];;
module DecompositionConfig = struct
module State_machine = struct
type state = Non;;
type event = Event;;
let init_state = Non;;
let step event state =
state;;
let is_valid event state =
true;;
end;;
let module_name = "DecompositionConfig"
module Template = struct
type t = TemplateT
type c = State_machine.event;;
let data = "";;
let concrete = fun _ _ -> true;;
end
end ;;
[@@@program]
let basis = ["abs"];;
module Idf = Imandra_tools.Idf;;
module D = Idf.Make(DecompositionConfig);;
module IDF_S = D.Symbolic;;
module IDF_C = D.Sampling;;
[@@@logic]
This errors because the line module D = Idf.Make(DecompositionConfig);; does not return properly from the server. Running on the command line is fine.
The following code require
imandra-tools
installed on the build switch and where imandra-merlin and imandra are running:This errors because the line
module D = Idf.Make(DecompositionConfig);;
does not return properly from the server. Running on the command line is fine.