KJ-21 Bug discovered by Andrei: Investigated. Adapted the programs to our naming pattern. Needs further investigation.

Author: denis-bogdanas

symbolic/max3.java symbolic/symbolic_01_max3.javasymbolic/max3.java renamed to symbolic/symbolic_01_max3.java

@@ -1,13 +1,16 @@
 /*
-$KOMPILE_CMD -v java --symbolic-rules "symbolic-rule" --backend symbolic
+kompile -v java --symbolic-rules "symbolic-rule" --backend symbolic
 
-time timeout 300 krun --debug-info --color extended --directory="/home/andrei.arusoaie/work/java-semantics/tools/../semantics" --main-module=JAVA -cMainClass="ListItem(\"max3\")" -cModelCheck="false" --output=pretty --parser="kj-parse-aggreg.sh" ../symbolic/max3.java -cIN="ListItem(3) ListItem(#symInt(x)) ListItem(8)" -cPC=true --search
+time timeout 300 krun --debug-info --color extended --directory="." --main-module=JAVA \
+  -cMainClass="ListItem(\"symbolic_01_max3\")" -cModelCheck="false" --output=pretty --parser="kj-parse-aggreg.sh" \
+  ../symbolic/symbolic_01_max3.java \
+  -cIN="ListItem(3) ListItem(#symInt(x)) ListItem(8)" -cPC=true --search
 
 Expected output: 3 solutions
 */
 import java.util.*;
 
-public class max3 {
+public class symbolic_01_max3 {
 
 	public static void main(String[] args) {
     System.out.print("Insert 3 numbers: ");

symbolic/test.java symbolic/symbolic_02_BasicList.javasymbolic/test.java renamed to symbolic/symbolic_02_BasicList.java

@@ -1,17 +1,20 @@
 /*
-$KOMPILE_CMD -v java --symbolic-rules "symbolic-rule" --backend symbolic
+kompile -v java --symbolic-rules "symbolic-rule" --backend symbolic
 
-time timeout 300 krun --debug-info --color extended --directory="/home/andrei.arusoaie/work/java-semantics/tools/../semantics" --main-module=JAVA -cMainClass="ListItem(\"test\")" -cModelCheck="false" --output=pretty --parser="kj-parse-aggreg.sh" ../symbolic/test.java -cIN="ListItem(#symInt(e1)) ListItem(#symInt(e2)) ListItem(#symInt(x))" -cPC="true" --search
+time timeout 300 krun --debug-info --color extended --directory="." --main-module=JAVA \
+  -cMainClass="ListItem(\"symbolic_02_BasicList\")" -cModelCheck="false" --output=pretty --parser="kj-parse-aggreg.sh" \
+  ../symbolic/symbolic_02_BasicList.java \
+  -cIN="ListItem(#symInt(e1)) ListItem(#symInt(e2)) ListItem(#symInt(x))" -cPC="true" --search
 
 Expected output: 4 solutions, one of them containing error message.
 */
 import java.util.*;
 
-class List {
+class BasicList {
   int a[] = new int[10];
   int size, capacity;
 
-  List () { size = 0; capacity = 10; }
+  BasicList() { size = 0; capacity = 10; }
 
   void insert (int x) {
     if (size < capacity) {
@@ -41,7 +44,7 @@ int getAt(int i) {
     return -1;
   }
 
-  boolean eqTo(List l) {
+  boolean eqTo(BasicList l) {
     if (size != l.size) {
         return false;
     }
@@ -55,8 +58,8 @@ boolean eqTo(List l) {
     return false;
   }
 
-  List copy() {
-    List t = new List();
+  BasicList copy() {
+    BasicList t = new BasicList();
     int i = 0;
     t.size = size;
     while(i < size) {
@@ -67,18 +70,18 @@ List copy() {
   }
 }
 
-public class test {
+public class symbolic_02_BasicList {
   public static void main(String[] args) {
     int i = 0;
-    List l1 = new List();
+    BasicList l1 = new BasicList();
     Scanner scanner = new Scanner(System.in);
     while (i < 2) {
       l1.insert(scanner.nextInt());
       i = i+1;
     }
     int x = scanner.nextInt();
 
-    List l2 = l1.copy();
+    BasicList l2 = l1.copy();
     l1.insert(x);
     l1.delete(x);
     if (l2.eqTo(l1) == false) {

symbolic/main.java symbolic/symbolic_03_OrderedList.javasymbolic/main.java renamed to symbolic/symbolic_03_OrderedList.java

@@ -1,17 +1,21 @@
 /*
-$KOMPILE_CMD -v java --symbolic-rules "symbolic-rule" --backend symbolic
+kompile -v java --symbolic-rules "symbolic-rule" --backend symbolic
 
-time timeout 300 krun --debug-info --color extended --directory="/home/andrei.arusoaie/work/java-semantics/tools/../semantics" --main-module=JAVA -cMainClass="ListItem(\"test\")" -cModelCheck="false" --output=pretty --parser="kj-parse-aggreg.sh" ../symbolic/main.java -cIN="ListItem(#symInt(e1)) ListItem(#symInt(e2)) ListItem(#symInt(x))" -cPC="true" --search
+time timeout 300 krun --debug-info --color extended --directory="." --main-module=JAVA \
+  -cMainClass="ListItem(\"symbolic_03_OrderedList\")" \
+  -cModelCheck="false" --output=pretty --parser="kj-parse-aggreg.sh" \
+  ../symbolic/symbolic_03_OrderedList.java \
+  -cIN="ListItem(#symInt(e1)) ListItem(#symInt(e2)) ListItem(#symInt(x))" -cPC="true" --search
 
 Expected output (unreached at the moment): 11 solutions, none of them containing error message.
 */
 import java.util.*;
 
-class LList {
+class BasicList {
   int a[] = new int[10];
   int size, capacity;
 
-  LList () { size = 0; capacity = 10; }
+  BasicList() { size = 0; capacity = 10; }
 
   void insert (int x) {
     if (size < capacity) {
@@ -41,7 +45,7 @@ int getAt(int i) {
     return -1;
   }
 
-  boolean eqTo(LList l) {
+  boolean eqTo(BasicList l) {
     if (size != l.size) {
         return false;
     }
@@ -55,8 +59,8 @@ boolean eqTo(LList l) {
     return false;
   }
 
-  LList copy() {
-    LList t = new LList();
+  BasicList copy() {
+    BasicList t = new BasicList();
     int i = 0;
     t.size = size;
     while(i < size) {
@@ -67,7 +71,7 @@ LList copy() {
   }
 }
 
-class OrderedList extends LList {
+class OrderedList extends BasicList {
 
     OrderedList() {
         super();
@@ -93,18 +97,18 @@ OrderedList copy() {
     }
 }
 
-public class main {
+public class symbolic_03_OrderedList {
   public static void main(String[] args) {
     int i = 0;
-    LList l1 = new OrderedList();
+    BasicList l1 = new OrderedList();
     Scanner scanner = new Scanner(System.in);
     while (i < 2) {
       l1.insert(scanner.nextInt());
       i = i+1;
     }
     int x = scanner.nextInt();
 
-    LList l2 = l1.copy();
+    BasicList l2 = l1.copy();
     l1.insert(x);
     l1.delete(x);
     if (l2.eqTo(l1) == false) {