From b0313723efbfe44b6b74072407c9d77720380603 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= <a-mikmay@microsoft.com>
Date: Wed, 25 Nov 2015 17:16:36 +0100
Subject: [PATCH] Added more benchmarks for string rendering.
---
testcases/stringrender/ChoiceRender.scala | 31 +++++++++++++++
testcases/stringrender/ConstantRender.scala | 43 +++++++++++++++++++++
testcases/stringrender/Example-Stack.scala | 33 ++++++++++++++++
3 files changed, 107 insertions(+)
create mode 100644 testcases/stringrender/ChoiceRender.scala
create mode 100644 testcases/stringrender/ConstantRender.scala
diff --git a/testcases/stringrender/ChoiceRender.scala b/testcases/stringrender/ChoiceRender.scala
new file mode 100644
index 000000000..3547d6fdc
--- /dev/null
+++ b/testcases/stringrender/ChoiceRender.scala
@@ -0,0 +1,31 @@
+/**
+ * Name: TupleWrapperRender.scala
+ * Creation: 15.10.2015
+ * Author: Mikaël Mayer (mikael.mayer@epfl.ch)
+ * Comments: Tuple rendering specifications.
+ */
+
+import leon.lang._
+import leon.annotation._
+import leon.collection._
+import leon.collection.ListOps._
+import leon.lang.synthesis._
+
+object ChoiceRender {
+ sealed abstract class Thread
+ case class T1() extends Thread
+ case class T2() extends Thread
+ case class T3() extends Thread
+
+ sealed abstract class Action
+ case class Call(t: Thread, args: Option[Int]) extends Action
+
+ @inline def psStandard(s: Action) = (res: String) => (s, res) passes {
+ case Call(T1(),None()) => "T1 call"
+ case Call(T1(),Some(2)) => "T1 -> 2"
+ }
+
+ def synthesizeStandard(s: Action): String = {
+ ???[String]
+ } ensuring psStandard(s)
+}
\ No newline at end of file
diff --git a/testcases/stringrender/ConstantRender.scala b/testcases/stringrender/ConstantRender.scala
new file mode 100644
index 000000000..f208fdb2b
--- /dev/null
+++ b/testcases/stringrender/ConstantRender.scala
@@ -0,0 +1,43 @@
+/**
+ * Name: TupleWrapperRender.scala
+ * Creation: 15.10.2015
+ * Author: Mikaël Mayer (mikael.mayer@epfl.ch)
+ * Comments: Tuple rendering specifications.
+ */
+
+import leon.lang._
+import leon.annotation._
+import leon.collection._
+import leon.collection.ListOps._
+import leon.lang.synthesis._
+
+object ConstantRender {
+ sealed abstract class Thread
+ case class T1() extends Thread
+ case class T2() extends Thread
+ case class T3() extends Thread
+
+ @inline def psStandard(s: Thread) = (res: String) => (s, res) passes {
+ case T1() => "T1"
+ }
+
+ @inline def psSuffix(s: Thread) = (res: String) => (s, res) passes {
+ case T1() => "T1()"
+ }
+
+ @inline def psPrefix(s: Thread) = (res: String) => (s, res) passes {
+ case T1() => "Call: T1()"
+ }
+
+ def synthesizeStandard(s: Thread): String = {
+ ???[String]
+ } ensuring psStandard(s)
+
+ def synthesizeSuffix(s: Thread): String = {
+ ???[String]
+ } ensuring psSuffix(s)
+
+ def synthesizePrefix(s: Thread): String = {
+ ???[String]
+ } ensuring psPrefix(s)
+}
\ No newline at end of file
diff --git a/testcases/stringrender/Example-Stack.scala b/testcases/stringrender/Example-Stack.scala
index 1f5024671..bb9f64d1f 100644
--- a/testcases/stringrender/Example-Stack.scala
+++ b/testcases/stringrender/Example-Stack.scala
@@ -326,6 +326,39 @@ object AtomicStack {
} holds
+ def threadToStringSimplest(p: StackTid): String = {
+ ???[String]
+ } ensuring {
+ res => (p, res) passes {
+ case T1()
+ =>
+ "T1: call Push(5)"
+ }
+ }
+
+ def threadToStringSimple0(p: Event[StackTid,StackMethodName,Option[BigInt],Option[BigInt]]): String = {
+ ???[String]
+ } ensuring {
+ res => (p, res) passes {
+ case CallEvent(T1(), Push(), Some(BigInt(5)))
+ =>
+ "T1: call Push(5)"
+ }
+ }
+
+ def threadToStringSimple1(p: List[Event[StackTid,StackMethodName,Option[BigInt],Option[BigInt]]]): String = {
+ ???[String]
+ } ensuring {
+ res => (p, res) passes {
+ case Cons(CallEvent(T1(), Push(), Some(BigInt(5))),
+ Cons(InternalEvent(T1()), Nil()))
+ =>
+ "T1: call Push(5)\nT1: internal"
+ }
+ }
+
+
+ /** This is THE method we want to render */
def threadToString(p: List[Event[StackTid,StackMethodName,Option[BigInt],Option[BigInt]]]): String = {
???[String]
} ensuring {
--
GitLab