From f8a17f4e69accf4d7aae19c30ba56c4c535f15b6 Mon Sep 17 00:00:00 2001
From: Nicola Mometto <me@bronsa.net>
Date: Wed, 4 Sep 2019 14:50:05 +0100
Subject: [PATCH] update to latest imandra-tools

---
 notebooks-src/Imandra-tools Introduction.md    | 17 ++++++++++-------
 .../Iterative Decomposition Framework.md       | 18 ++++++++++--------
 2 files changed, 20 insertions(+), 15 deletions(-)

diff --git a/notebooks-src/Imandra-tools Introduction.md b/notebooks-src/Imandra-tools Introduction.md
index 27d86a703..c03a6675f 100644
--- a/notebooks-src/Imandra-tools Introduction.md	
+++ b/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
diff --git a/notebooks-src/Iterative Decomposition Framework.md b/notebooks-src/Iterative Decomposition Framework.md
index 2593d375f..f616ae8bf 100644
--- a/notebooks-src/Iterative Decomposition Framework.md	
+++ b/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
 ```