Update make files for performance analysis

benchmarks/README.md

 **Analysis of the Performance in the generated code:**
 
 1. Switch to the directory *java*
-1. Compile one of the machine (LiftExec, Sieve, TrafficLightExec)
-2. Execute the machine
+2. Switch to the directory *persistent* or *nonpersistent*
+3. Use belonging make command (Example: make lift)
 
 <br>
 <br>
@@ -10,6 +10,4 @@
 
 **Analysis of the Performance in ProB:**
 1. Switch to folder *prob*
-2. Open probcli with one of the machine (Example: ./probcli.sh -repl TrafficLightExec.mch)
-3. Initialize the machine with "-init"
-4. Execute the performance analysis with "-execute 1"
+2. Use belonging make command (Example: make lift)
\ No newline at end of file

benchmarks/java/Makefile → benchmarks/java/nonpersistent/Makefile

-
-bench: Liftexec.class
+lift: LiftExec.class
 	java -cp :btypes.jar LiftExec
+traffic: TrafficLightExec.class
+	java -cp :btypes.jar TrafficLightExec
 sieve: Sieve.class
 	java -cp :btypes.jar Sieve
 iset: IncreasingSet.class
@@ -10,11 +11,18 @@ set: SetOperation.class
 
 Lift.class: Lift.java
 	javac -cp btypes.jar Lift.java
-Liftexec.class: LiftExec.java
+LiftExec.class: LiftExec.java
 	javac -cp btypes.jar LiftExec.java Lift.java
+TrafficLight.class: TrafficLight.java
+	javac -cp btypes.jar TrafficLight.java
+TrafficLightExec.class: TrafficLightExec.java
+	javac -cp btypes.jar TrafficLightExec.java TrafficLight.java
 Sieve.class: Sieve.java
 	javac -cp btypes.jar Sieve.java
 IncreasingSet.class: IncreasingSet.java
 	javac -cp btypes.jar IncreasingSet.java
 SetOperation.class: SetOperation.java
 	javac -cp btypes.jar SetOperation.java
+
+clean:
+	rm *.class
\ No newline at end of file

benchmarks/java/persistent/IncreasingSet.java

+import de.hhu.stups.btypes.BSet;
+import de.hhu.stups.btypes.BInteger;
+
+public class IncreasingSet {
+
+
+
+
+    private BInteger counter;
+    private BSet set;
+
+    private boolean initialized = false;
+
+    public void initialize() {
+        if(initialized) {
+            throw new RuntimeException("Machine is already initialized");
+        }
+        counter = (BInteger) new BInteger("0");
+        set = (BSet) new BSet(new BInteger("1"), new BInteger("2"), new BInteger("3"));
+        initialized = true;
+    }
+
+    public void simulate() {
+        if(!initialized) {
+            throw new RuntimeException("Machine was not initialized");
+        }
+        while((counter.less(new BInteger("25000"))).booleanValue()) {
+            set = (BSet) set.union(new BSet(counter));
+            counter = (BInteger) counter.plus(new BInteger("1"));
+        }
+    }
+
+    public static void main(String[] args) {
+        IncreasingSet exec = new IncreasingSet();
+        exec.initialize();
+        long start = System.nanoTime();
+        exec.simulate();
+        long end = System.nanoTime();
+        System.out.println("Execution: " + (end - start));
+    }
+
+}

benchmarks/java/persistent/Lift.java

+import de.hhu.stups.btypes.BInteger;
+
+public class Lift {
+
+
+
+
+    private BInteger floor;
+
+    private boolean initialized = false;
+
+    public void initialize() {
+        if(initialized) {
+            throw new RuntimeException("Machine is already initialized");
+        }
+        floor = (BInteger) new BInteger("0");
+        initialized = true;
+    }
+
+    public void inc() {
+        if(!initialized) {
+            throw new RuntimeException("Machine was not initialized");
+        }
+        floor = (BInteger) floor.plus(new BInteger("1"));
+    }
+
+    public void dec() {
+        if(!initialized) {
+            throw new RuntimeException("Machine was not initialized");
+        }
+        floor = (BInteger) floor.minus(new BInteger("1"));
+    }
+
+}

benchmarks/java/persistent/LiftExec.java

+import de.hhu.stups.btypes.BInteger;
+
+public class LiftExec {
+
+    private Lift Lift = new Lift();
+
+
+
+    private BInteger counter;
+
+    private boolean initialized = false;
+
+    public void initialize() {
+        if(initialized) {
+            throw new RuntimeException("Machine is already initialized");
+        }
+        Lift.initialize();
+        counter = (BInteger) new BInteger("0");
+        initialized = true;
+    }
+
+    public void simulate() {
+        if(!initialized) {
+            throw new RuntimeException("Machine was not initialized");
+        }
+        while((counter.less(new BInteger("3000"))).booleanValue()) {
+            BInteger i = null;
+            i = (BInteger) new BInteger("0");
+            while((i.less(new BInteger("100"))).booleanValue()) {
+                this.Lift.inc();
+                i = (BInteger) i.plus(new BInteger("1"));
+            }
+            BInteger _i = null;
+            _i = (BInteger) new BInteger("0");
+            while((_i.less(new BInteger("100"))).booleanValue()) {
+                this.Lift.dec();
+                _i = (BInteger) _i.plus(new BInteger("1"));
+            }
+            counter = (BInteger) counter.plus(new BInteger("1"));
+        }
+    }
+
+    public static void main(String[] args) {
+        LiftExec exec = new LiftExec();
+        exec.initialize();
+        long start = System.nanoTime();
+        exec.simulate();
+        long end = System.nanoTime();
+        System.out.println("Execution: " + (end - start));
+    }
+
+}

benchmarks/java/persistent/Makefile

+lift: LiftExec.class
+	java -cp :btypes_persistent.jar LiftExec
+traffic: TrafficLightExec.class
+	java -cp :btypes_persistent.jar TrafficLightExec
+sieve: Sieve.class
+	java -cp :btypes_persistent.jar Sieve
+iset: IncreasingSet.class
+	java -cp :btypes_persistent.jar IncreasingSet
+set: SetOperation.class
+	java -cp :btypes_persistent.jar SetOperation
+
+Lift.class: Lift.java
+	javac -cp btypes_persistent.jar Lift.java
+LiftExec.class: LiftExec.java
+	javac -cp btypes_persistent.jar LiftExec.java Lift.java
+TrafficLight.class: TrafficLight.java
+	javac -cp btypes_persistent.jar TrafficLight.java
+TrafficLightExec.class: TrafficLightExec.java
+	javac -cp btypes_persistent.jar TrafficLightExec.java TrafficLight.java
+Sieve.class: Sieve.java
+	javac -cp btypes_persistent.jar Sieve.java
+IncreasingSet.class: IncreasingSet.java
+	javac -cp btypes_persistent.jar IncreasingSet.java
+SetOperation.class: SetOperation.java
+	javac -cp btypes_persistent.jar SetOperation.java
+
+clean:
+	rm *.class
\ No newline at end of file

benchmarks/java/persistent/SetOperation.java

+import de.hhu.stups.btypes.BSet;
+import de.hhu.stups.btypes.BInteger;
+
+public class SetOperation {
+
+
+
+
+    private BInteger counter;
+    private BSet set;
+
+    private boolean initialized = false;
+
+    public void initialize() {
+        if(initialized) {
+            throw new RuntimeException("Machine is already initialized");
+        }
+        counter = (BInteger) new BInteger("0");
+        set = (BSet) new BSet(new BInteger("1"), new BInteger("2"), new BInteger("3"));
+        initialized = true;
+    }
+
+    public void simulate() {
+        if(!initialized) {
+            throw new RuntimeException("Machine was not initialized");
+        }
+        while((counter.less(new BInteger("500000"))).booleanValue()) {
+            set = (BSet) set.union(new BSet(new BInteger("1")));
+            counter = (BInteger) counter.plus(new BInteger("1"));
+        }
+    }
+
+    public static void main(String[] args) {
+        SetOperation exec = new SetOperation();
+        exec.initialize();
+        long start = System.nanoTime();
+        exec.simulate();
+        long end = System.nanoTime();
+        System.out.println("Execution: " + (end - start));
+    }
+
+}

benchmarks/java/persistent/Sieve.java

+import de.hhu.stups.btypes.BSet;
+import de.hhu.stups.btypes.BInteger;
+
+public class Sieve {
+
+
+
+
+    private BSet numbers;
+    private BInteger cur;
+    private BInteger limit;
+
+    private boolean initialized = false;
+
+    public void initialize() {
+        if(initialized) {
+            throw new RuntimeException("Machine is already initialized");
+        }
+        numbers = (BSet) BSet.range(new BInteger("2"),new BInteger("10000"));
+        cur = (BInteger) new BInteger("2");
+        limit = (BInteger) new BInteger("10000");
+        initialized = true;
+    }
+
+    public BInteger ComputeNumberOfPrimes() {
+        if(!initialized) {
+            throw new RuntimeException("Machine was not initialized");
+        }
+        BInteger res = null;
+        while((cur.greater(new BInteger("1")).and(cur.multiply(cur).lessEqual(limit))).booleanValue()) {
+            if((numbers.elementOf(cur)).booleanValue()) {
+                BInteger n = null;
+                BSet set = null;
+                n = (BInteger) cur;
+                set = (BSet) new BSet();
+                while((n.lessEqual(limit.divide(cur))).booleanValue()) {
+                    set = (BSet) set.union(new BSet(cur.multiply(n)));
+                    n = (BInteger) n.plus(new BInteger("1"));
+                }
+                numbers = (BSet) numbers.complement(set);
+            } 
+            cur = (BInteger) cur.plus(new BInteger("1"));
+        }
+        res = (BInteger) numbers.card();
+        return res;
+    }
+
+    public static void main(String[] args) {
+        Sieve sieve = new Sieve();
+        sieve.initialize();
+        long start = System.nanoTime();
+        sieve.ComputeNumberOfPrimes();
+        long end = System.nanoTime();
+        System.out.println("Execution: " + (end - start));
+    }
+}

benchmarks/java/persistent/TrafficLight.java

+import de.hhu.stups.btypes.BSet;
+import de.hhu.stups.btypes.BObject;
+import de.hhu.stups.btypes.BBoolean;
+
+public class TrafficLight {
+
+
+    public enum colors implements BObject {
+        red, 
+        redyellow, 
+        yellow, 
+        green;
+
+        public BBoolean equal(colors o) {
+            return new BBoolean(this == o);
+        }
+
+        public BBoolean unequal(colors o) {
+            return new BBoolean(this != o);
+        }
+    }
+
+    private BSet _colors = new BSet(colors.red, colors.redyellow, colors.yellow, colors.green);
+
+    private colors tl_cars;
+    private colors tl_peds;
+
+    private boolean initialized = false;
+
+    public void initialize() {
+        if(initialized) {
+            throw new RuntimeException("Machine is already initialized");
+        }
+        tl_cars = (colors) colors.red;
+        tl_peds = (colors) colors.red;
+        initialized = true;
+    }
+
+    public void cars_ry() {
+        if(!initialized) {
+            throw new RuntimeException("Machine was not initialized");
+        }
+        if((tl_cars.equal(colors.red).and(tl_peds.equal(colors.red))).booleanValue()) {
+            tl_cars = (colors) colors.redyellow;
+        } else {
+            throw new RuntimeException("Invocation of the operation is not possible");
+        }
+    }
+
+    public void cars_y() {
+        if(!initialized) {
+            throw new RuntimeException("Machine was not initialized");
+        }
+        if((tl_cars.equal(colors.green).and(tl_peds.equal(colors.red))).booleanValue()) {
+            tl_cars = (colors) colors.yellow;
+        } else {
+            throw new RuntimeException("Invocation of the operation is not possible");
+        }
+    }
+
+    public void cars_g() {
+        if(!initialized) {
+            throw new RuntimeException("Machine was not initialized");
+        }
+        if((tl_cars.equal(colors.redyellow).and(tl_peds.equal(colors.red))).booleanValue()) {
+            tl_cars = (colors) colors.green;
+        } else {
+            throw new RuntimeException("Invocation of the operation is not possible");
+        }
+    }
+
+    public void cars_r() {
+        if(!initialized) {
+            throw new RuntimeException("Machine was not initialized");
+        }
+        if((tl_cars.equal(colors.yellow).and(tl_peds.equal(colors.red))).booleanValue()) {
+            tl_cars = (colors) colors.red;
+        } else {
+            throw new RuntimeException("Invocation of the operation is not possible");
+        }
+    }
+
+    public void peds_r() {
+        if(!initialized) {
+            throw new RuntimeException("Machine was not initialized");
+        }
+        if((tl_peds.equal(colors.green).and(tl_cars.equal(colors.red))).booleanValue()) {
+            tl_peds = (colors) colors.red;
+        } else {
+            throw new RuntimeException("Invocation of the operation is not possible");
+        }
+    }
+
+    public void peds_g() {
+        if(!initialized) {
+            throw new RuntimeException("Machine was not initialized");
+        }
+        if((tl_peds.equal(colors.red).and(tl_cars.equal(colors.red))).booleanValue()) {
+            tl_peds = (colors) colors.green;
+        } else {
+            throw new RuntimeException("Invocation of the operation is not possible");
+        }
+    }
+
+}

benchmarks/java/persistent/TrafficLightExec.java

+import de.hhu.stups.btypes.BInteger;
+
+public class TrafficLightExec {
+
+    private TrafficLight TrafficLight = new TrafficLight();
+
+
+
+    private BInteger counter;
+
+    private boolean initialized = false;
+
+    public void initialize() {
+        if(initialized) {
+            throw new RuntimeException("Machine is already initialized");
+        }
+        TrafficLight.initialize();
+        counter = (BInteger) new BInteger("0");
+        initialized = true;
+    }
+
+    public void simulate() {
+        if(!initialized) {
+            throw new RuntimeException("Machine was not initialized");
+        }
+        while((counter.less(new BInteger("500000"))).booleanValue()) {
+            this.TrafficLight.cars_ry();
+            this.TrafficLight.cars_g();
+            this.TrafficLight.cars_y();
+            this.TrafficLight.cars_r();
+            this.TrafficLight.peds_g();
+            this.TrafficLight.peds_r();
+            counter = (BInteger) counter.plus(new BInteger("1"));
+        }
+    }
+
+    public static void main(String[] args) {
+        TrafficLightExec exec = new TrafficLightExec();
+        exec.initialize();
+        long start = System.nanoTime();
+        exec.simulate();
+        long end = System.nanoTime();
+        System.out.println("Execution: " + (end - start));
+    }
+
+}

benchmarks/prob/Makefile

-PROBCLI=probcli
+PROBCLI=./probcli.sh
 sieve:
 	$(PROBCLI) Sieve.mch -init -execute 1
 lift:
@@ -9,3 +9,6 @@ set:
 	$(PROBCLI) SetOperation.mch -init -execute 1
 iset:
 	$(PROBCLI) IncreasingSet.mch -init -execute 1
+
+clean:
+	rm *.prob