From 8d737512ce183e6e5d6f2dc0e04d44754673d3ce Mon Sep 17 00:00:00 2001
From: Eduard <eduard.kamburjan@gmx.de>
Date: Fri, 26 Mar 2021 16:06:33 +0100
Subject: [PATCH] added example

---
 .idea/Chisel.iml          | 12 +++++++++-
 examples/Demo/Billard.abs | 49 +++++++++++++++++++++++++++++++++++++++
 2 files changed, 60 insertions(+), 1 deletion(-)
 create mode 100644 examples/Demo/Billard.abs

diff --git a/.idea/Chisel.iml b/.idea/Chisel.iml
index 78b2cc5..634006f 100644
--- a/.idea/Chisel.iml
+++ b/.idea/Chisel.iml
@@ -1,2 +1,12 @@
 <?xml version="1.0" encoding="UTF-8"?>
-<module type="JAVA_MODULE" version="4" />
\ No newline at end of file
+<module external.linked.project.id="Chisel" external.linked.project.path="$MODULE_DIR$" external.root.project.path="$MODULE_DIR$" external.system.id="GRADLE" external.system.module.group="Crowbar" external.system.module.version="0.2" type="JAVA_MODULE" version="4">
+  <component name="NewModuleRootManager" inherit-compiler-output="true">
+    <exclude-output />
+    <content url="file://$MODULE_DIR$">
+      <excludeFolder url="file://$MODULE_DIR$/.gradle" />
+      <excludeFolder url="file://$MODULE_DIR$/build" />
+    </content>
+    <orderEntry type="inheritedJdk" />
+    <orderEntry type="sourceFolder" forTests="false" />
+  </component>
+</module>
\ No newline at end of file
diff --git a/examples/Demo/Billard.abs b/examples/Demo/Billard.abs
new file mode 100644
index 0000000..d376758
--- /dev/null
+++ b/examples/Demo/Billard.abs
@@ -0,0 +1,49 @@
+module Demo;
+
+data HybridSpec =  ObjInv(String) | Ensures(String) | Requires(String) | Tactic(String);
+
+type Real = Rat;
+
+interface IBillard {
+     Unit accelerate(Real r);
+     Unit push(Real a, Real b);
+     Unit leap();
+     [HybridSpec: Requires("extra >= 0")]
+     Unit incSize(Real extra);
+}
+[HybridSpec: Requires("top > 0 & bottom < 0 & right > 0 & left < 0")]
+class Billard(Real top, Real bottom,
+	      Real left, Real right,
+	      Real vx,
+	      Real vy) implements IBillard{
+
+[HybridSpec: ObjInv("top >= y & bottom <= y & right >= x & left <= x")]
+	physical{
+		Real x = 0: x' = vx;
+		Real y = 0: y' = vy;
+	}
+	{
+		this!ctrlTop(); this!ctrlRight();
+		this!ctrlBottom(); this!ctrlLeft();
+	}
+	Unit ctrlTop(){
+		await diff y >= top && vy >= 0; vy = -vy; this!ctrlTop();
+	}
+	Unit ctrlBottom(){
+		await diff y >= bottom && vy <= 0; vy = -vy; this!ctrlBottom();
+	}
+	Unit ctrlRight(){
+		await diff x >= right && vx >= 0; vx = -vx; this!ctrlRight();
+	}
+	Unit ctrlLeft(){
+		await diff x >= left && vx <= 0; vx = -vx; this!ctrlLeft();
+	}
+	Unit accelerate(Real r){ vx = vx*r; vy = vy*r; }
+    Unit push(Real a, Real b){ vx = vx + a; vy = vy + b; }
+    Unit leap(){
+        if( vx > 0 && right - x > 1) x = x + 1;
+        if( vx < 0 && x -left > 1) x = x - 1;
+    }
+    Unit incSize(Real extra){ top = top + extra; }
+}
+{}
\ No newline at end of file