From dc3dca98a847fa62d29dd4dea14d03b78a9a8c8e Mon Sep 17 00:00:00 2001 From: Julian Mendez Date: Mon, 28 Oct 2024 08:43:27 +0100 Subject: [PATCH] Add module to create instances for measurements --- build.sbt | 15 +- .../example/market/measurement/Basic.soda | 30 ++ .../example/market/measurement/Main.soda | 88 ++++++ .../measurement/OperationGenerator.soda | 92 ++++++ .../measurement/OperationSerializer.soda | 25 ++ .../example/market/measurement/Package.scala | 299 ++++++++++++++++++ .../example/market/measurement/Package.soda | 25 ++ .../measurement/OperationGeneratorSpec.soda | 45 +++ .../example/market/measurement/Package.scala | 69 ++++ .../example/market/measurement/Package.soda | 23 ++ 10 files changed, 709 insertions(+), 2 deletions(-) create mode 100644 measurement/src/main/scala/soda/se/umu/cs/soda/prototype/example/market/measurement/Basic.soda create mode 100644 measurement/src/main/scala/soda/se/umu/cs/soda/prototype/example/market/measurement/Main.soda create mode 100644 measurement/src/main/scala/soda/se/umu/cs/soda/prototype/example/market/measurement/OperationGenerator.soda create mode 100644 measurement/src/main/scala/soda/se/umu/cs/soda/prototype/example/market/measurement/OperationSerializer.soda create mode 100644 measurement/src/main/scala/soda/se/umu/cs/soda/prototype/example/market/measurement/Package.scala create mode 100644 measurement/src/main/scala/soda/se/umu/cs/soda/prototype/example/market/measurement/Package.soda create mode 100644 measurement/src/test/scala/soda/se/umu/cs/soda/prototype/example/market/measurement/OperationGeneratorSpec.soda create mode 100644 measurement/src/test/scala/soda/se/umu/cs/soda/prototype/example/market/measurement/Package.scala create mode 100644 measurement/src/test/scala/soda/se/umu/cs/soda/prototype/example/market/measurement/Package.soda diff --git a/build.sbt b/build.sbt index a52c00b..7fda609 100644 --- a/build.sbt +++ b/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"), diff --git a/measurement/src/main/scala/soda/se/umu/cs/soda/prototype/example/market/measurement/Basic.soda b/measurement/src/main/scala/soda/se/umu/cs/soda/prototype/example/market/measurement/Basic.soda new file mode 100644 index 0000000..94343f3 --- /dev/null +++ b/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 diff --git a/measurement/src/main/scala/soda/se/umu/cs/soda/prototype/example/market/measurement/Main.soda b/measurement/src/main/scala/soda/se/umu/cs/soda/prototype/example/market/measurement/Main.soda new file mode 100644 index 0000000..1a752db --- /dev/null +++ b/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 + diff --git a/measurement/src/main/scala/soda/se/umu/cs/soda/prototype/example/market/measurement/OperationGenerator.soda b/measurement/src/main/scala/soda/se/umu/cs/soda/prototype/example/market/measurement/OperationGenerator.soda new file mode 100644 index 0000000..f58b227 --- /dev/null +++ b/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 + diff --git a/measurement/src/main/scala/soda/se/umu/cs/soda/prototype/example/market/measurement/OperationSerializer.soda b/measurement/src/main/scala/soda/se/umu/cs/soda/prototype/example/market/measurement/OperationSerializer.soda new file mode 100644 index 0000000..c69c0b7 --- /dev/null +++ b/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 + diff --git a/measurement/src/main/scala/soda/se/umu/cs/soda/prototype/example/market/measurement/Package.scala b/measurement/src/main/scala/soda/se/umu/cs/soda/prototype/example/market/measurement/Package.scala new file mode 100644 index 0000000..cf7a378 --- /dev/null +++ b/measurement/src/main/scala/soda/se/umu/cs/soda/prototype/example/market/measurement/Package.scala @@ -0,0 +1,299 @@ +package soda.se.umu.cs.soda.prototype.example.market.measurement + +/* + * This package contains classes to create instances for measurements + * + */ + +import soda.se.umu.cs.soda.prototype.example.market.core.Market +import soda.se.umu.cs.soda.prototype.example.market.core.Operation +import soda.se.umu.cs.soda.prototype.example.market.core.OperationProcessor +import soda.se.umu.cs.soda.prototype.example.market.core.Operation +import soda.se.umu.cs.soda.prototype.example.market.core.OpAssign +import soda.se.umu.cs.soda.prototype.example.market.core.OpAssign_ +import soda.se.umu.cs.soda.prototype.example.market.core.OpDeposit +import soda.se.umu.cs.soda.prototype.example.market.core.OpDeposit_ +import soda.se.umu.cs.soda.prototype.example.market.core.OpPrice +import soda.se.umu.cs.soda.prototype.example.market.core.OpPrice_ +import soda.se.umu.cs.soda.prototype.example.market.core.OpSell +import soda.se.umu.cs.soda.prototype.example.market.core.OpSell_ +import soda.se.umu.cs.soda.prototype.example.market.core.OpUndefined +import soda.se.umu.cs.soda.prototype.example.market.core.OpUndefined_ +import soda.se.umu.cs.soda.prototype.example.market.core.OperationEnum + +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) . +*/ + +trait Range +{ + + + + private def _tailrec_range (non_negative_number : Nat) (sequence : List [Nat] ) : List [Nat] = + non_negative_number match { + case Succ_ (k) => + _tailrec_range (k) ( (k) +: (sequence) ) + case _otherwise => sequence + } + + def apply (length : Int) : List [Nat] = + _tailrec_range (length) (Nil) + +} + +case class Range_ () extends Range + +object Range { + def mk : Range = + Range_ () +} + + +/** + * This is the main entry point. + */ + +trait Main +{ + + + + import scala.util.control.Exception.allCatch + + lazy val 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" + + lazy val operation_generator = OperationGenerator .mk + + lazy val operation_serializer = OperationSerializer .mk + + def generate_operations (accounts : Nat) (items : Nat) (transactions : Nat) : List [Operation] = + operation_generator + .generate (accounts) (items) (transactions) + + def serialize_operations (operations : List [Operation] ) : String = + "operations:" + + "\n- " + + operations + .map ( operation => operation_serializer .serialize (operation) ) + .mkString ("\n- ") + + "\n\n" + + def to_nat (n : Int) : Nat = + if ( n < 0 + ) 0 + else n + + def to_int_or_zero (s : String) : Int = + allCatch + .opt (s .toInt) + .getOrElse (0) + + def to_nat_or_zero (s : String) : Nat = + to_nat ( + to_int_or_zero (s) + ) + + def 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" + + def create_output (accounts : Nat) (items : Nat) (transactions : Nat) : String = + (create_header (accounts) (items) (transactions) ) + + serialize_operations ( + generate_operations (accounts) (items) (transactions) + ) + + def execute (arguments : List [String] ) : Unit = + if ( arguments .length > 2 + ) 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) + + def main (arguments : Array [String] ) : Unit = + execute (arguments .toList) + +} + +object EntryPoint { + def main (args: Array [String]): Unit = Main_ ().main (args) +} + + +case class Main_ () extends Main + +object Main { + def mk : Main = + Main_ () +} + + +trait OperationGenerator +{ + + + + lazy val deposit_factor = 100 + + lazy val deposit_offset = 0 + + lazy val max_deposit = 1000000 + + lazy val owner_factor = 65537 + + lazy val owner_offset = 1 + + lazy val buyer_factor = 8191 + + lazy val buyer_offset = 1 + + lazy val merchandise_factor = 31 + + lazy val merchandise_offset = 1 + + lazy val price_factor = 127 + + lazy val price_offset = 0 + + lazy val max_price = 100000 + + def abs (x : Int) : Nat = + if ( x < 0 + ) -x + else x + + def generate (index : Nat) (multiplier : Nat) (increment : Nat) (modulus : Nat) : Nat = + abs ( (index * multiplier + increment) % modulus) + + def deposit_of_user (user_id : Nat) : Nat = + generate (user_id) (deposit_factor) (deposit_offset) (max_deposit) + + def owner_of_item (item_id : Nat) (accounts : Nat) : Nat = + generate (item_id) (owner_factor) (owner_offset) (accounts) + + def price_of_item (item_id : Nat) : Nat = + generate (item_id) (price_factor) (price_offset) (max_price) + + def buyer_of_item (transaction_id : Nat) (accounts : Nat) : Nat = + generate (transaction_id) (buyer_factor) (buyer_offset) (accounts) + + def item_being_sold (transaction_id : Nat) (items : Nat) : Nat = + generate (transaction_id) (merchandise_factor) (merchandise_offset) (items) + + def make_deposits (accounts : Nat) : List [Operation] = + Range .mk .apply (accounts) + .map ( user_id => + OpDeposit .mk (user_id) (deposit_of_user (user_id) ) + ) + + def make_items (accounts : Nat) (items : Nat) : List [Operation] = + Range .mk .apply (items) + .map ( item_id => + OpAssign .mk (item_id) (owner_of_item (item_id) (accounts) ) + ) + + def put_prices (items : Nat) : List [Operation] = + Range .mk .apply (items) + .map ( item_id => + OpPrice .mk (item_id) (price_of_item (item_id) ) + ) + + def make_transactions (accounts : Nat) (items : Nat) (transactions : Nat) : List [Operation] = + Range .mk .apply (transactions) + .map ( transaction_id => + OpSell .mk ( + item_being_sold (transaction_id) (items) ) ( + buyer_of_item (transaction_id) (accounts) + ) + ) + + def generate (accounts : Nat) (items : Nat) (transactions : Nat) : List [Operation] = + if ( (accounts > 0) && (items > 0) && (transactions > 0) + ) + make_deposits (accounts) .++ ( + make_items (accounts) (items) .++ ( + put_prices (items) .++ ( + make_transactions (accounts) (items) (transactions) + ) + ) + ) + else List [Operation] () + +} + +case class OperationGenerator_ () extends OperationGenerator + +object OperationGenerator { + def mk : OperationGenerator = + OperationGenerator_ () +} + + +trait OperationSerializer +{ + + + + lazy val op_enum = OperationEnum .mk + + lazy val empty = "" + + lazy val sp = " " + + def serialize (op : Operation) : String = + op match { + 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 + } + +} + +case class OperationSerializer_ () extends OperationSerializer + +object OperationSerializer { + def mk : OperationSerializer = + OperationSerializer_ () +} + diff --git a/measurement/src/main/scala/soda/se/umu/cs/soda/prototype/example/market/measurement/Package.soda b/measurement/src/main/scala/soda/se/umu/cs/soda/prototype/example/market/measurement/Package.soda new file mode 100644 index 0000000..02b28bb --- /dev/null +++ b/measurement/src/main/scala/soda/se/umu/cs/soda/prototype/example/market/measurement/Package.soda @@ -0,0 +1,25 @@ +package soda.se.umu.cs.soda.prototype.example.market.measurement + +/* + * This package contains classes to create instances for measurements + * + */ + +import + soda.se.umu.cs.soda.prototype.example.market.core.Market + soda.se.umu.cs.soda.prototype.example.market.core.Operation + soda.se.umu.cs.soda.prototype.example.market.core.OperationProcessor + soda.se.umu.cs.soda.prototype.example.market.core.Operation + soda.se.umu.cs.soda.prototype.example.market.core.OpAssign + soda.se.umu.cs.soda.prototype.example.market.core.OpAssign_ + soda.se.umu.cs.soda.prototype.example.market.core.OpDeposit + soda.se.umu.cs.soda.prototype.example.market.core.OpDeposit_ + soda.se.umu.cs.soda.prototype.example.market.core.OpPrice + soda.se.umu.cs.soda.prototype.example.market.core.OpPrice_ + soda.se.umu.cs.soda.prototype.example.market.core.OpSell + soda.se.umu.cs.soda.prototype.example.market.core.OpSell_ + soda.se.umu.cs.soda.prototype.example.market.core.OpUndefined + soda.se.umu.cs.soda.prototype.example.market.core.OpUndefined_ + soda.se.umu.cs.soda.prototype.example.market.core.OperationEnum + + diff --git a/measurement/src/test/scala/soda/se/umu/cs/soda/prototype/example/market/measurement/OperationGeneratorSpec.soda b/measurement/src/test/scala/soda/se/umu/cs/soda/prototype/example/market/measurement/OperationGeneratorSpec.soda new file mode 100644 index 0000000..cce42a6 --- /dev/null +++ b/measurement/src/test/scala/soda/se/umu/cs/soda/prototype/example/market/measurement/OperationGeneratorSpec.soda @@ -0,0 +1,45 @@ + +class OperationGeneratorSpec () + extends + AnyFunSuite + + check [A : Type] (obtained : A) (expected : A) : org.scalatest.compatible.Assertion = + assert (obtained == expected) + + generator = OperationGenerator .mk + + accounts = 10000 + + items = 20000 + + transactions = 1000000 + + instance : List [Operation] = + generator .generate (accounts) (items) (transactions) + + complies_invariant (op : Operation) : Boolean = + match op + case OpDeposit_ (user_id , amount) ==> + (0 <= user_id) and (user_id < accounts) and (amount >= 0) + case OpAssign_ (item_id , user_id) ==> + (0 <= item_id) and (item_id < items) and (0 <= user_id) and (user_id < accounts) + case OpPrice_ (item_id , price) ==> + (0 <= item_id) and (item_id < items) and (price >= 0) + case OpSell_ (item_id , user_id) ==> + (0 <= item_id) and (item_id < items) and (0 <= user_id) and (user_id < accounts) + case otherwise ==> false + + find_exceptions_to_invariant (operations : List [Operation] ) : List [Operation] = + operations + .filter (lambda operation --> not complies_invariant (operation) ) + + test ("count exceptions to invariant") ( + check ( + obtained := find_exceptions_to_invariant (instance) .length + ) ( + expected := 0 + ) + ) + +end + diff --git a/measurement/src/test/scala/soda/se/umu/cs/soda/prototype/example/market/measurement/Package.scala b/measurement/src/test/scala/soda/se/umu/cs/soda/prototype/example/market/measurement/Package.scala new file mode 100644 index 0000000..fce1ea5 --- /dev/null +++ b/measurement/src/test/scala/soda/se/umu/cs/soda/prototype/example/market/measurement/Package.scala @@ -0,0 +1,69 @@ +package soda.se.umu.cs.soda.prototype.example.market.measurement + +/* + * This package contains classes to create instances for measurements + * + */ + +import org.scalatest.funsuite.AnyFunSuite +import soda.se.umu.cs.soda.prototype.example.market.core.Operation +import soda.se.umu.cs.soda.prototype.example.market.core.OperationProcessor +import soda.se.umu.cs.soda.prototype.example.market.core.Operation +import soda.se.umu.cs.soda.prototype.example.market.core.OpAssign +import soda.se.umu.cs.soda.prototype.example.market.core.OpAssign_ +import soda.se.umu.cs.soda.prototype.example.market.core.OpDeposit +import soda.se.umu.cs.soda.prototype.example.market.core.OpDeposit_ +import soda.se.umu.cs.soda.prototype.example.market.core.OpPrice +import soda.se.umu.cs.soda.prototype.example.market.core.OpPrice_ +import soda.se.umu.cs.soda.prototype.example.market.core.OpSell +import soda.se.umu.cs.soda.prototype.example.market.core.OpSell_ +import soda.se.umu.cs.soda.prototype.example.market.core.OpUndefined +import soda.se.umu.cs.soda.prototype.example.market.core.OpUndefined_ +import soda.se.umu.cs.soda.prototype.example.market.core.OperationEnum + +case class OperationGeneratorSpec () + extends + AnyFunSuite +{ + + def check [A ] (obtained : A) (expected : A) : org.scalatest.compatible.Assertion = + assert (obtained == expected) + + lazy val generator = OperationGenerator .mk + + lazy val accounts = 10000 + + lazy val items = 20000 + + lazy val transactions = 1000000 + + lazy val instance : List [Operation] = + generator .generate (accounts) (items) (transactions) + + def complies_invariant (op : Operation) : Boolean = + op match { + case OpDeposit_ (user_id , amount) => + (0 <= user_id) && (user_id < accounts) && (amount >= 0) + case OpAssign_ (item_id , user_id) => + (0 <= item_id) && (item_id < items) && (0 <= user_id) && (user_id < accounts) + case OpPrice_ (item_id , price) => + (0 <= item_id) && (item_id < items) && (price >= 0) + case OpSell_ (item_id , user_id) => + (0 <= item_id) && (item_id < items) && (0 <= user_id) && (user_id < accounts) + case otherwise => false + } + + def find_exceptions_to_invariant (operations : List [Operation] ) : List [Operation] = + operations + .filter ( operation => ! complies_invariant (operation) ) + + test ("count exceptions to invariant") ( + check ( + obtained = find_exceptions_to_invariant (instance) .length + ) ( + expected = 0 + ) + ) + +} + diff --git a/measurement/src/test/scala/soda/se/umu/cs/soda/prototype/example/market/measurement/Package.soda b/measurement/src/test/scala/soda/se/umu/cs/soda/prototype/example/market/measurement/Package.soda new file mode 100644 index 0000000..14dba53 --- /dev/null +++ b/measurement/src/test/scala/soda/se/umu/cs/soda/prototype/example/market/measurement/Package.soda @@ -0,0 +1,23 @@ +package soda.se.umu.cs.soda.prototype.example.market.measurement + +/* + * This package contains classes to create instances for measurements + * + */ + +import + org.scalatest.funsuite.AnyFunSuite + soda.se.umu.cs.soda.prototype.example.market.core.Operation + soda.se.umu.cs.soda.prototype.example.market.core.OperationProcessor + soda.se.umu.cs.soda.prototype.example.market.core.Operation + soda.se.umu.cs.soda.prototype.example.market.core.OpAssign + soda.se.umu.cs.soda.prototype.example.market.core.OpAssign_ + soda.se.umu.cs.soda.prototype.example.market.core.OpDeposit + soda.se.umu.cs.soda.prototype.example.market.core.OpDeposit_ + soda.se.umu.cs.soda.prototype.example.market.core.OpPrice + soda.se.umu.cs.soda.prototype.example.market.core.OpPrice_ + soda.se.umu.cs.soda.prototype.example.market.core.OpSell + soda.se.umu.cs.soda.prototype.example.market.core.OpSell_ + soda.se.umu.cs.soda.prototype.example.market.core.OpUndefined + soda.se.umu.cs.soda.prototype.example.market.core.OpUndefined_ + soda.se.umu.cs.soda.prototype.example.market.core.OperationEnum