use strings for client id

palmskog · palmskog · commit 161ff6863bb5 · 2016-11-19T17:38:30.000-06:00
diff --git a/extraction/aggregation-dynamic/coq/ExtractTreeAggregation.v b/extraction/aggregation-dynamic/coq/ExtractTreeAggregation.v
@@ -17,6 +17,7 @@ Require Import mathcomp.algebra.zmodp.
 
 Require Import ExtrOcamlBasic.
 Require Import ExtrOcamlNatInt.
+Require Import ExtrOcamlString.
 
 Require Import ExtrOcamlBasicExt.
 Require Import ExtrOcamlNatIntExt.
diff --git a/extraction/aggregation-dynamic/ocaml/Serialization.ml b/extraction/aggregation-dynamic/ocaml/Serialization.ml
@@ -3,6 +3,7 @@ open Printf
 open Scanf
 open TreeAggregation
 open TreeAggregationNames
+open Util
 
 let serializeName : Names.name -> string = string_of_int
 
@@ -16,24 +17,24 @@ let deserializeMsg : string -> coq_Msg = fun s ->
 let serializeMsg : coq_Msg -> string = fun msg ->
   Marshal.to_string msg []
 
-let deserializeInput (s : string) (client_id : int) : coq_Input option =
+let deserializeInput (s : string) (c : string) : coq_Input option =
   match s with
   | "SendAggregate" -> Some SendAggregate
   | "Broadcast" -> Some Broadcast
-  | "AggregateRequest" -> Some (AggregateRequest client_id)
-  | "LevelRequest" -> Some (LevelRequest client_id)
+  | "AggregateRequest" -> Some (AggregateRequest (char_list_of_string c))
+  | "LevelRequest" -> Some (LevelRequest (char_list_of_string c))
   | _ -> 
-    try sscanf s "Local %d" (fun x -> Some (Local (Obj.magic x))) 
+    try Scanf.sscanf s "Local %d" (fun x -> Some (Local (Obj.magic x)))
     with _ -> None
 
 let serializeLevelOption olv : string =
   match olv with
   | Some lv -> string_of_int lv
   | _ -> ""
 
-let serializeOutput : coq_Output -> int * string = function
-  | AggregateResponse (client_id, x) -> (client_id, sprintf "AggregateResponse %d" (Obj.magic x))
-  | LevelResponse (client_id, olv) -> (client_id, sprintf "LevelResponse %s" (serializeLevelOption olv))
+let serializeOutput : coq_Output -> string * string = function
+  | AggregateResponse (c, x) -> (string_of_char_list c, sprintf "AggregateResponse %d" (Obj.magic x))
+  | LevelResponse (c, olv) -> (string_of_char_list c, sprintf "LevelResponse %s" (serializeLevelOption olv))
 
 let debugSerializeInput : coq_Input -> string = function
   | SendAggregate -> "SendAggregate"
diff --git a/extraction/aggregation-dynamic/ocaml/TreeAggregationArrangement.ml b/extraction/aggregation-dynamic/ocaml/TreeAggregationArrangement.ml
@@ -8,6 +8,7 @@ module TreeAggregationArrangement = struct
   type output = coq_Output
   type msg = coq_Msg
   type res = (output list * state) * ((name * msg) list)
+  type client_id = string
 
   let systemName : string = "Dynamic Tree Aggregation Protocol"
 
@@ -28,13 +29,13 @@ module TreeAggregationArrangement = struct
 
   let setTimeout : name -> state -> float = fun _ _ -> 1.0
 
-  let deserializeMsg : string -> msg = Serialization.deserializeMsg
+  let deserializeMsg = Serialization.deserializeMsg
 
-  let serializeMsg : msg -> string = Serialization.serializeMsg
+  let serializeMsg = Serialization.serializeMsg
 
   let deserializeInput = Serialization.deserializeInput
 
-  let serializeOutput : output -> int * string = Serialization.serializeOutput
+  let serializeOutput = Serialization.serializeOutput
 
   let failMsg = Some Fail
 
@@ -55,5 +56,6 @@ module TreeAggregationArrangement = struct
     print_newline ()
 
   let debugTimeout : state -> unit = fun _ -> ()
-end
 
+  let createClientId () = Uuidm.to_string (Uuidm.create `V4)
+end
diff --git a/extraction/aggregation/coq/ExtractTreeAggregation.v b/extraction/aggregation/coq/ExtractTreeAggregation.v
@@ -18,6 +18,7 @@ Require Import mathcomp.algebra.zmodp.
 
 Require Import ExtrOcamlBasic.
 Require Import ExtrOcamlNatInt.
+Require Import ExtrOcamlString.
 
 Require Import ExtrOcamlBasicExt.
 Require Import ExtrOcamlNatIntExt.
diff --git a/extraction/aggregation/ocaml/Serialization.ml b/extraction/aggregation/ocaml/Serialization.ml
@@ -3,6 +3,7 @@ open Printf
 open Scanf
 open TreeAggregation
 open TreeAggregationNames
+open Util
 
 let serializeName : Names.name -> string = string_of_int
 
@@ -16,12 +17,12 @@ let deserializeMsg : string -> coq_Msg = fun s ->
 let serializeMsg : coq_Msg -> string = fun msg ->
   Marshal.to_string msg []
 
-let deserializeInput (s : string) (client_id : int) : coq_Input option =
+let deserializeInput (s : string) (c : string) : coq_Input option =
   match s with
   | "SendAggregate" -> Some SendAggregate
   | "Broadcast" -> Some Broadcast
-  | "AggregateRequest" -> Some (AggregateRequest client_id)
-  | "LevelRequest" -> Some (LevelRequest client_id)
+  | "AggregateRequest" -> Some (AggregateRequest (char_list_of_string c))
+  | "LevelRequest" -> Some (LevelRequest (char_list_of_string c))
   | _ -> 
     try Scanf.sscanf s "Local %d" (fun x -> Some (Local (Obj.magic x)))
     with _ -> None
@@ -31,9 +32,9 @@ let serializeLevelOption olv : string =
   | Some lv -> string_of_int lv
   | _ -> "-"
 
-let serializeOutput : coq_Output -> int * string = function
-  | AggregateResponse (client_id, x) -> (client_id, sprintf "AggregateResponse %d" (Obj.magic x))
-  | LevelResponse (client_id, olv) -> (client_id, sprintf "LevelResponse %s" (serializeLevelOption olv))
+let serializeOutput : coq_Output -> string * string = function
+  | AggregateResponse (c, x) -> (string_of_char_list c, sprintf "AggregateResponse %d" (Obj.magic x))
+  | LevelResponse (c, olv) -> (string_of_char_list c, sprintf "LevelResponse %s" (serializeLevelOption olv))
 
 let debugSerializeInput : coq_Input -> string = function
   | SendAggregate -> "SendAggregate"
diff --git a/extraction/aggregation/ocaml/TreeAggregationArrangement.ml b/extraction/aggregation/ocaml/TreeAggregationArrangement.ml
@@ -8,6 +8,7 @@ module TreeAggregationArrangement = struct
   type output = coq_Output
   type msg = coq_Msg
   type res = (output list * state) * ((name * msg) list)
+  type client_id = string
 
   let systemName : string = "Static Tree Aggregation Protocol"
 
@@ -32,9 +33,9 @@ module TreeAggregationArrangement = struct
 
   let serializeMsg : msg -> string = Serialization.serializeMsg
 
-  let deserializeInput : string -> int -> input option = Serialization.deserializeInput
+  let deserializeInput : string -> client_id -> input option = Serialization.deserializeInput
 
-  let serializeOutput : output -> int * string = Serialization.serializeOutput
+  let serializeOutput : output -> client_id * string = Serialization.serializeOutput
 
   let failMsg : msg option = Some Fail
 
@@ -55,4 +56,6 @@ module TreeAggregationArrangement = struct
     print_newline ()
 
   let debugTimeout : state -> unit = fun _ -> ()
+
+  let createClientId () = Uuidm.to_string (Uuidm.create `V4)
 end
diff --git a/extraction/tree-dynamic/coq/ExtractTree.v b/extraction/tree-dynamic/coq/ExtractTree.v
@@ -8,6 +8,7 @@ Require Import StructTact.Fin.
 
 Require Import ExtrOcamlBasic.
 Require Import ExtrOcamlNatInt.
+Require Import ExtrOcamlString.
 
 Require Import ExtrOcamlBasicExt.
 Require Import ExtrOcamlNatIntExt.
diff --git a/extraction/tree-dynamic/ocaml/Serialization.ml b/extraction/tree-dynamic/ocaml/Serialization.ml
@@ -3,6 +3,7 @@ open Printf
 open Scanf
 open Tree
 open TreeNames
+open Util
 
 let serializeName : Names.name -> string = string_of_int
 
@@ -16,19 +17,19 @@ let deserializeMsg : string -> coq_Msg = fun s ->
 let serializeMsg : coq_Msg -> string = fun msg ->
   Marshal.to_string msg []
 
-let deserializeInput (s : string) (client_id : int) : coq_Input option =
+let deserializeInput (s : string) (c : string) : coq_Input option =
   match s with
   | "Broadcast" -> Some Broadcast
-  | "LevelRequest" -> Some (LevelRequest client_id)
+  | "LevelRequest" -> Some (LevelRequest (char_list_of_string c))
   | _ -> None
 
 let serializeLevelOption olv : string =
   match olv with
   | Some lv -> string_of_int lv
   | _ -> "-"
 
-let serializeOutput : coq_Output -> int * string = function
-  | LevelResponse (client_id, olv) -> (client_id, sprintf "LevelResponse %s" (serializeLevelOption olv))
+let serializeOutput : coq_Output -> string * string = function
+  | LevelResponse (c, olv) -> (string_of_char_list c, sprintf "LevelResponse %s" (serializeLevelOption olv))
 
 let debugSerializeInput : coq_Input -> string = function
   | Broadcast -> "Broadcast"
diff --git a/extraction/tree-dynamic/ocaml/TreeArrangement.ml b/extraction/tree-dynamic/ocaml/TreeArrangement.ml
@@ -8,6 +8,7 @@ module TreeArrangement = struct
   type output = coq_Output
   type msg = coq_Msg
   type res = (output list * state) * ((name * msg) list)
+  type client_id = string
 
   let systemName : string = "Dynamic Tree Building Protocol"
 
@@ -55,4 +56,6 @@ module TreeArrangement = struct
     print_newline ()
 
   let debugTimeout : state -> unit = fun _ -> ()
+
+  let createClientId () = Uuidm.to_string (Uuidm.create `V4)
 end
diff --git a/extraction/tree/coq/ExtractTree.v b/extraction/tree/coq/ExtractTree.v
@@ -8,6 +8,7 @@ Require Import StructTact.Fin.
 
 Require Import ExtrOcamlBasic.
 Require Import ExtrOcamlNatInt.
+Require Import ExtrOcamlString.
 
 Require Import ExtrOcamlBasicExt.
 Require Import ExtrOcamlNatIntExt.
diff --git a/extraction/tree/ocaml/Serialization.ml b/extraction/tree/ocaml/Serialization.ml
@@ -3,6 +3,7 @@ open Printf
 open Scanf
 open Tree
 open TreeNames
+open Util
 
 let serializeName : Names.name -> string = string_of_int
 
@@ -16,19 +17,19 @@ let deserializeMsg : string -> coq_Msg = fun s ->
 let serializeMsg : coq_Msg -> string = fun msg ->
   Marshal.to_string msg []
 
-let deserializeInput (s : string) (client_id : int) : coq_Input option =
+let deserializeInput (s : string) (c : string) : coq_Input option =
   match s with
   | "Broadcast" -> Some Broadcast
-  | "LevelRequest" -> Some (LevelRequest client_id)
+  | "LevelRequest" -> Some (LevelRequest (char_list_of_string c))
   | _ -> None
 
 let serializeLevelOption olv : string =
   match olv with
   | Some lv -> string_of_int lv
   | _ -> "-"
 
-let serializeOutput : coq_Output -> int * string = function
-  | LevelResponse (client_id, olv) -> (client_id, sprintf "LevelResponse %s" (serializeLevelOption olv))
+let serializeOutput : coq_Output -> string * string = function
+  | LevelResponse (c, olv) -> (string_of_char_list c, sprintf "LevelResponse %s" (serializeLevelOption olv))
 
 let debugSerializeInput : coq_Input -> string = function
   | Broadcast -> "Broadcast"
diff --git a/extraction/tree/ocaml/TreeArrangement.ml b/extraction/tree/ocaml/TreeArrangement.ml
@@ -8,6 +8,7 @@ module TreeArrangement = struct
   type output = coq_Output
   type msg = coq_Msg
   type res = (output list * state) * ((name * msg) list)
+  type client_id = string
 
   let systemName : string = "Static Tree Building Protocol"
 
@@ -55,4 +56,6 @@ module TreeArrangement = struct
     print_newline ()
 
   let debugTimeout : state -> unit = fun _ -> ()
+
+  let createClientId () = Uuidm.to_string (Uuidm.create `V4)
 end
diff --git a/systems/AggregationDynamic.v b/systems/AggregationDynamic.v
@@ -14,6 +14,8 @@ Require Import mathcomp.ssreflect.fintype.
 Require Import mathcomp.ssreflect.finset.
 Require Import mathcomp.fingroup.fingroup.
 
+Require String.
+
 Local Arguments update {_} {_} _ _ _ _ _ : simpl never.
 
 Set Implicit Arguments.
@@ -42,24 +44,24 @@ Defined.
 Inductive Input : Type :=
 | Local : m -> Input
 | SendAggregate : name -> Input
-| AggregateRequest : nat -> Input.
+| AggregateRequest : String.string -> Input.
 
 Definition Input_eq_dec : forall x y : Input, {x = y} + {x <> y}.
-decide equality; auto using Nat.eq_dec, m_eq_dec, name_eq_dec.
+decide equality; auto using String.string_dec, m_eq_dec, name_eq_dec.
 Defined.
 
 Inductive Output : Type :=
-| AggregateResponse : nat -> m -> Output.
+| AggregateResponse : String.string -> m -> Output.
 
 Definition Output_eq_dec : forall x y : Output, {x = y} + {x <> y}.
-decide equality; auto using Nat.eq_dec, m_eq_dec.
+decide equality; auto using String.string_dec, m_eq_dec.
 Defined.
 
-Record Data := mkData { 
-  local : m ; 
-  aggregate : m ; 
-  adjacent : NS ; 
-  balance : NM 
+Record Data := mkData {
+  local : m ;
+  aggregate : m ;
+  adjacent : NS ;
+  balance : NM
 }.
 
 Definition InitData (n : name) := 
diff --git a/systems/AggregationStatic.v b/systems/AggregationStatic.v
@@ -15,6 +15,8 @@ Require Import mathcomp.ssreflect.fintype.
 Require Import mathcomp.ssreflect.finset.
 Require Import mathcomp.fingroup.fingroup.
 
+Require String.
+
 Local Arguments update {_} {_} _ _ _ _ _ : simpl never.
 
 Set Implicit Arguments.
@@ -43,17 +45,17 @@ Defined.
 Inductive Input : Type :=
 | Local : m -> Input
 | SendAggregate : name -> Input
-| AggregateRequest : nat -> Input.
+| AggregateRequest : String.string -> Input.
 
 Definition Input_eq_dec : forall x y : Input, {x = y} + {x <> y}.
-decide equality; auto using Nat.eq_dec, m_eq_dec, name_eq_dec.
+decide equality; auto using String.string_dec, m_eq_dec, name_eq_dec.
 Defined.
 
 Inductive Output : Type :=
-| AggregateResponse : nat -> m -> Output.
+| AggregateResponse : String.string -> m -> Output.
 
 Definition Output_eq_dec : forall x y : Output, {x = y} + {x <> y}.
-decide equality; auto using Nat.eq_dec, m_eq_dec.
+decide equality; auto using String.string_dec, m_eq_dec.
 Defined.
 
 Record Data := mkData { 
diff --git a/systems/AggregatorDynamic.v b/systems/AggregatorDynamic.v
@@ -11,6 +11,7 @@ Require Import Orders.
 Require Import MSetFacts.
 Require Import MSetProperties.
 Require Import Sumbool.
+Require String.
 
 Require Import mathcomp.ssreflect.ssreflect.
 Require Import mathcomp.ssreflect.ssrbool.
@@ -50,7 +51,7 @@ Inductive Input : Type :=
 | New : name -> Input
 | Local : m -> Input
 | SendAggregate : name -> Input
-| AggregateRequest : nat -> Input.
+| AggregateRequest : String.string -> Input.
 
 Definition Input_eq_dec : forall x y : Input, {x = y} + {x <> y}.
 decide equality.
@@ -60,14 +61,14 @@ decide equality.
 - exact: name_eq_dec.
 - exact: m_eq_dec.
 - exact: name_eq_dec.
-- exact: Nat.eq_dec.
+- exact: String.string_dec.
 Defined.
 
 Inductive Output : Type :=
-| AggregateResponse : nat -> m -> Output.
+| AggregateResponse : String.string -> m -> Output.
 
 Definition Output_eq_dec : forall x y : Output, {x = y} + {x <> y}.
-decide equality; auto using Nat.eq_dec, m_eq_dec.
+decide equality; auto using String.string_dec, m_eq_dec.
 Defined.
 
 Record Data := mkData { 
diff --git a/systems/AggregatorStatic.v b/systems/AggregatorStatic.v
diff --git a/systems/TreeAggregationDynamic.v b/systems/TreeAggregationDynamic.v
diff --git a/systems/TreeAggregationStatic.v b/systems/TreeAggregationStatic.v
diff --git a/systems/TreeAggregationStaticLabeled.v b/systems/TreeAggregationStaticLabeled.v
diff --git a/systems/TreeDynamic.v b/systems/TreeDynamic.v
diff --git a/systems/TreeStatic.v b/systems/TreeStatic.v
diff --git a/systems/TreeStaticLabeled.v b/systems/TreeStaticLabeled.v
