Add module to create instances for measurements

build.sbt

@@ -54,13 +54,24 @@ lazy val core =
       assembly / assemblyJarName := "core-" + version.value + ".jar"
     )
 
+lazy val measurement =
+  project
+    .withId("measurement")
+    .in(file("measurement"))
+    .aggregate(core)
+    .dependsOn(core)
+    .settings(
+      commonSettings,
+      assembly / mainClass := Some("soda.se.umu.cs.soda.prototype.example.market.measurement.EntryPoint"),
+      assembly / assemblyJarName := "measurement-" + version.value + ".jar"
+    )
 
 lazy val root =
   project
     .withId("market")
     .in(file("."))
-    .aggregate(core)
-    .dependsOn(core)
+    .aggregate(core, measurement)
+    .dependsOn(core, measurement)
     .settings(
       commonSettings,
       assembly / mainClass := Some("soda.se.umu.cs.soda.prototype.example.market.main.EntryPoint"),

measurement/src/main/scala/soda/se/umu/cs/soda/prototype/example/market/measurement/Basic.soda

@@ -0,0 +1,30 @@
+
+directive scala
+type Nat = Int
+object Succ_ {
+  def apply (n : Int) : Int = n + 1
+  def unapply (n : Int) : Option [Int] =
+    if (n <= 0) None else Some (n - 1)
+}
+
+directive lean
+notation "Succ_" => Nat.succ
+
+directive coq
+Notation "'Succ_'" := S (at level 99) .
+
+
+class Range
+
+  abstract
+
+  _tailrec_range (non_negative_number : Nat) (sequence : List [Nat] ) : List [Nat] =
+    match non_negative_number
+      case Succ_ (k) ==>
+        _tailrec_range (k) ( (k) +: (sequence) )
+      case _otherwise ==> sequence
+
+  apply (length : Int) : List [Nat] =
+    _tailrec_range (length) (Nil)
+
+end

measurement/src/main/scala/soda/se/umu/cs/soda/prototype/example/market/measurement/Main.soda

@@ -0,0 +1,88 @@
+
+/**
+ * This is the main entry point.
+ */
+
+class Main
+
+  abstract
+
+  import
+    scala.util.control.Exception.allCatch
+
+  help = "" +
+    "This creates an instance of synthetically generated transactions." +
+    "\nIt outputs a YAML string containing the operations." +
+    "\n" +
+    "\nParameters: ACCOUNTS ITEMS TRANSACTIONS" +
+    "\n" +
+    "\n    ACCOUNTS     The number of accounts ('deposit') in the market" +
+    "\n    ITEMS        The number of instance ('item') in the market" +
+    "\n    TRANSACTIONS The number of transactions ('sell') in the market" +
+    "\n" +
+    "\n"
+
+  operation_generator = OperationGenerator .mk
+
+  operation_serializer = OperationSerializer .mk
+
+  generate_operations (accounts : Nat) (items : Nat) (transactions : Nat) : List [Operation] =
+    operation_generator
+      .generate (accounts) (items) (transactions)
+
+  serialize_operations (operations : List [Operation] ) : String =
+    "operations:" +
+    "\n- " +
+    operations
+      .map (lambda operation --> operation_serializer .serialize (operation) )
+      .mkString ("\n- ") +
+    "\n\n"
+
+  to_nat (n : Int) : Nat =
+    if n < 0
+    then 0
+    else n
+
+  to_int_or_zero (s : String) : Int =
+    allCatch
+      .opt (s .toInt)
+      .getOrElse (0)
+
+  to_nat_or_zero (s : String) : Nat =
+    to_nat (
+      to_int_or_zero (s)
+    )
+
+  create_header (accounts : Nat) (items : Nat) (transactions : Nat) : String =
+    "---" +
+    "\n# "+
+    "\n# This is a synthetically generated instance." +
+    "\n# " +
+    "\n#   accounts: " + accounts .toString +
+    "\n#   items: " + items .toString +
+    "\n#   transactions: " + transactions .toString +
+    "\n#" +
+    "\n"
+
+  create_output (accounts : Nat) (items : Nat) (transactions : Nat) : String =
+    (create_header (accounts) (items) (transactions) ) +
+      serialize_operations (
+        generate_operations (accounts) (items) (transactions)
+      )
+
+  execute (arguments : List [String] ) : Unit =
+    if arguments .length > 2
+    then println (
+      create_output (
+        to_nat_or_zero (arguments .apply (0) ) ) (
+        to_nat_or_zero (arguments .apply (1) ) ) (
+        to_nat_or_zero (arguments .apply (2) )
+      )
+    )
+    else println (help)
+
+  main (arguments : Array [String] ) : Unit =
+    execute (arguments .toList)
+
+end
+

measurement/src/main/scala/soda/se/umu/cs/soda/prototype/example/market/measurement/OperationGenerator.soda

@@ -0,0 +1,92 @@
+class OperationGenerator
+
+  abstract
+
+  deposit_factor = 100
+
+  deposit_offset = 0
+
+  max_deposit = 1000000
+
+  owner_factor = 65537
+
+  owner_offset = 1
+
+  buyer_factor = 8191
+
+  buyer_offset = 1
+
+  merchandise_factor = 31
+
+  merchandise_offset = 1
+
+  price_factor = 127
+
+  price_offset = 0
+
+  max_price = 100000
+
+  abs (x : Int) : Nat =
+    if x < 0
+    then -x
+    else x
+
+  generate (index : Nat) (multiplier : Nat) (increment : Nat) (modulus : Nat) : Nat =
+    abs ( (index * multiplier + increment) % modulus)
+
+  deposit_of_user (user_id : Nat) : Nat =
+    generate (user_id) (deposit_factor) (deposit_offset) (max_deposit)
+
+  owner_of_item (item_id : Nat) (accounts : Nat) : Nat =
+    generate (item_id) (owner_factor) (owner_offset) (accounts)
+
+  price_of_item (item_id : Nat) : Nat =
+    generate (item_id) (price_factor) (price_offset) (max_price)
+
+  buyer_of_item (transaction_id : Nat) (accounts : Nat) : Nat =
+    generate (transaction_id) (buyer_factor) (buyer_offset) (accounts)
+
+  item_being_sold (transaction_id : Nat) (items : Nat) : Nat =
+    generate (transaction_id) (merchandise_factor) (merchandise_offset) (items)
+
+  make_deposits (accounts : Nat) : List [Operation] =
+    Range .mk .apply (accounts)
+      .map (lambda user_id -->
+        OpDeposit .mk (user_id) (deposit_of_user (user_id) )
+      )
+
+  make_items (accounts : Nat) (items : Nat) : List [Operation] =
+    Range .mk .apply (items)
+      .map (lambda item_id -->
+        OpAssign .mk (item_id) (owner_of_item (item_id) (accounts) )
+      )
+
+  put_prices (items : Nat) : List [Operation] =
+    Range .mk .apply (items)
+      .map (lambda item_id -->
+        OpPrice .mk (item_id) (price_of_item (item_id) )
+      )
+
+  make_transactions (accounts : Nat) (items : Nat) (transactions : Nat) : List [Operation] =
+    Range .mk .apply (transactions)
+      .map (lambda transaction_id -->
+        OpSell .mk (
+          item_being_sold (transaction_id) (items) ) (
+          buyer_of_item (transaction_id) (accounts)
+        )
+      )
+
+  generate (accounts : Nat) (items : Nat) (transactions : Nat) : List [Operation] =
+    if (accounts > 0) and (items > 0) and (transactions > 0)
+    then
+      make_deposits (accounts) .++ (
+        make_items (accounts) (items) .++ (
+          put_prices (items) .++ (
+            make_transactions (accounts) (items) (transactions)
+          )
+        )
+      )
+    else List [Operation] ()
+
+end
+

measurement/src/main/scala/soda/se/umu/cs/soda/prototype/example/market/measurement/OperationSerializer.soda

@@ -0,0 +1,25 @@
+
+class OperationSerializer
+
+  abstract
+
+  op_enum = OperationEnum .mk
+
+  empty = ""
+
+  sp = " "
+
+  serialize (op : Operation) : String =
+    match op
+      case OpDeposit_ (user_id , amount) ==>
+        op_enum .deposit .name + sp + user_id .toString + sp + amount .toString
+      case OpAssign_ (item_id , user_id) ==>
+        op_enum .assign .name + sp + item_id  .toString + sp + user_id .toString
+      case OpPrice_ (item_id , price) ==>
+        op_enum .price .name + sp + item_id  .toString + sp + price .toString
+      case OpSell_ (item_id , user_id) ==>
+        op_enum .sell .name + sp + item_id .toString + sp + user_id .toString
+      case otherwise ==> empty
+
+end
+