update to latest imandra-tools

notebooks-src/Imandra-tools Introduction.md

@@ -87,7 +87,8 @@ We need to do is define a module implementing the `Idf_intf.DFSM_SIG` module sig
 - a `module_name` value mapping to the name of the module being defined (this is necessary for reflection purposes)
 - a `Template` module implementing the `Idf_intf.TPL_SIG` module signature:
   - a `t` variant type symbolically describing events from our model
-  - a `concrete` function from `t` to a list of strings mapping the symbolic event to concrete `event` type names
+  - a `c` variant type mapping to the concrete `event` type
+  - a `concrete` function mapping `t` events to `c` events
 
 ```{.imandra .input}
 open Imandra_tools
@@ -118,12 +119,14 @@ module Decomp = struct
 
   module Template = struct
     type t = Add | Sub | Reset | Any
-
-    let concrete = function
-        | Add -> ["Model.Add"]
-        | Sub -> ["Model.Sub"]
-        | Reset -> ["Model.Reset"]
-        | Any -> []
+    type c = State_machine.event
+
+    let concrete c t = match c, t with
+        | Add, Model.Add _ -> true
+        | Sub, Model.Sub _ -> true
+        | Reset, Model.Reset -> true
+        | Any, _ -> true
+        | _ -> false
   end
 
 end

notebooks-src/Iterative Decomposition Framework.md

@@ -87,14 +87,16 @@ Note that there's not necessarily a 1:1 correspondence between the variant const
 module TPL = struct
   (* type of a symbolic state machine event *)
   type t = Add | AddInt | Sub | Reset | Any
-
-  (* mapping function from a symbolic state machine event to a concrete event name *)
-  let concrete = function
-    | Any -> []
-    | Add -> ["SM.Add"]
-    | AddInt -> ["SM.Add"; "SM.Int"]
-    | Sub -> ["SM.Sub"]
-    | Reset -> ["SM.Reset"]
+  type c = SM.event
+
+  (* mapping function from a symbolic state machine event to a concrete event *)
+  let concrete t c = match t,c with
+    | Any, _ -> true
+    | Add, SM.Add _ -> true
+    | AddInt, SM.Add(SM.Int _) -> true
+    | Sub, SM.Sub _ -> true
+    | Reset, SM.Reset -> true
+    | _ -> false
 end
 ```