change time stamp

classicwuhao · Oct 9, 2021 · 43aaa6c · 43aaa6c
1 parent 29fb58b
commit 43aaa6c
Show file tree

Hide file tree

Showing 19 changed files with 50 additions and 29 deletions.
diff --git a/build/classes/org/tzi/use/main/shell/Shell.class b/build/classes/org/tzi/use/main/shell/Shell.class
diff --git a/build/classes/org/tzi/use/query/QueryCompiler.class b/build/classes/org/tzi/use/query/QueryCompiler.class
diff --git a/lib/qmaxuse.jar b/lib/qmaxuse.jar
diff --git a/lib/query.smt2 b/lib/query.smt2
@@ -1,31 +1,43 @@
 
-;this file is automatically generated: Fri Oct 08 12:06:44 IST 2021
+;this file is automatically generated: Sat Oct 09 12:05:34 IST 2021
 
 ;declarations generated
 
 (declare-fun Gender ( Int) Int)
 (declare-fun oclExcludes ( Int Int) Bool)
-(declare-fun type_4b39a4df_257d_47b3_8433_3fc5e160ed6b_Child ( Int) Bool)
+(declare-fun rel_513ed927_c474_4439_9b03_bfb41440ceac_choose ( Int Int) Bool)
+(declare-fun type_f98975bc_f44c_4fea_a8d1_931336031c56_Person ( Int) Bool)
 (declare-fun Cardinality ( Int) Int)
-(declare-fun type_4b39a4df_257d_47b3_8433_3fc5e160ed6b_Student ( Int) Bool)
-(declare-fun type_4b39a4df_257d_47b3_8433_3fc5e160ed6b_Person ( Int) Bool)
+(declare-fun obj_80fc0bf1_e6bc_49f5_81ef_35f9a0752dfa ( Int) Int)
+(declare-fun student_year ( Int) Int)
 (declare-fun person_age ( Int) Int)
-(declare-fun type_4b39a4df_257d_47b3_8433_3fc5e160ed6b_Department ( Int) Bool)
-(declare-fun type_4b39a4df_257d_47b3_8433_3fc5e160ed6b_University ( Int) Bool)
+(declare-fun k29ba979d_dba0_47bf_99d8_8ac3f7ce7a4a () Int)
+(declare-fun type_f98975bc_f44c_4fea_a8d1_931336031c56_Module ( Int) Bool)
+(declare-fun type_f98975bc_f44c_4fea_a8d1_931336031c56_Child ( Int) Bool)
 (declare-fun oclSelect ( Int Bool) Int)
-(declare-fun obj_43a5862c_514e_47a8_b954_45d461df7bc9 ( Int) Int)
+(declare-fun type_f98975bc_f44c_4fea_a8d1_931336031c56_Student ( Int) Bool)
+(declare-fun module_year ( Int) Int)
+(declare-fun type_f98975bc_f44c_4fea_a8d1_931336031c56_Department ( Int) Bool)
 (declare-fun container_ ( Int) Int)
-(declare-fun type_4b39a4df_257d_47b3_8433_3fc5e160ed6b_Module ( Int) Bool)
+(declare-fun type_f98975bc_f44c_4fea_a8d1_931336031c56_University ( Int) Bool)
+(declare-fun k2c8acb06_ff95_4751_9c70_3ced7154f447 () Int)
 (declare-fun oclIncludes ( Int Int) Bool)
+(declare-fun student_id ( Int) Int)
 (declare-fun ObjAt ( Int Int) Int)
 
 ;formula(s) generated
-(assert (! (forall ((p Int)) (=> ( type_4b39a4df_257d_47b3_8433_3fc5e160ed6b_Person p )  (and (> ( person_age ( obj_43a5862c_514e_47a8_b954_45d461df7bc9 p )  )  0) (< ( person_age ( obj_43a5862c_514e_47a8_b954_45d461df7bc9 p )  )  18)))):named l0))
-(assert (! (exists ((o Int)) (and ( type_4b39a4df_257d_47b3_8433_3fc5e160ed6b_Child ( obj_43a5862c_514e_47a8_b954_45d461df7bc9 o )  )  ( type_4b39a4df_257d_47b3_8433_3fc5e160ed6b_Person ( obj_43a5862c_514e_47a8_b954_45d461df7bc9 o )  ) )):named c0))
-(assert (! (exists ((o Int)) ( type_4b39a4df_257d_47b3_8433_3fc5e160ed6b_Department ( obj_43a5862c_514e_47a8_b954_45d461df7bc9 o )  ) ):named c1))
-(assert (! (exists ((o Int)) ( type_4b39a4df_257d_47b3_8433_3fc5e160ed6b_Module ( obj_43a5862c_514e_47a8_b954_45d461df7bc9 o )  ) ):named c2))
-(assert (! (exists ((o Int)) ( type_4b39a4df_257d_47b3_8433_3fc5e160ed6b_Person ( obj_43a5862c_514e_47a8_b954_45d461df7bc9 o )  ) ):named c3))
-(assert (! (exists ((o Int)) (and ( type_4b39a4df_257d_47b3_8433_3fc5e160ed6b_Student ( obj_43a5862c_514e_47a8_b954_45d461df7bc9 o )  )  ( type_4b39a4df_257d_47b3_8433_3fc5e160ed6b_Person ( obj_43a5862c_514e_47a8_b954_45d461df7bc9 o )  ) )):named c4))
-(assert (! (exists ((o Int)) ( type_4b39a4df_257d_47b3_8433_3fc5e160ed6b_University ( obj_43a5862c_514e_47a8_b954_45d461df7bc9 o )  ) ):named c5))
+(assert (forall ((x Int)(y Int)) (=> (and ( rel_513ed927_c474_4439_9b03_bfb41440ceac_choose ( obj_80fc0bf1_e6bc_49f5_81ef_35f9a0752dfa x )   ( obj_80fc0bf1_e6bc_49f5_81ef_35f9a0752dfa y )  )  (and (and ( type_f98975bc_f44c_4fea_a8d1_931336031c56_Student x )  ( type_f98975bc_f44c_4fea_a8d1_931336031c56_Person x ) ) ( type_f98975bc_f44c_4fea_a8d1_931336031c56_Module y ) )) (or (or (or (= (* ( Cardinality ( container_ x )  )  0) (* ( Cardinality ( container_ y )  )  1)) (and (= (* ( Cardinality ( container_ y )  )  1) (* ( Cardinality ( container_ x )  )  k29ba979d_dba0_47bf_99d8_8ac3f7ce7a4a)) (>= k29ba979d_dba0_47bf_99d8_8ac3f7ce7a4a 0))) (= (* ( Cardinality ( container_ x )  )  0) (* ( Cardinality ( container_ y )  )  1))) (and (= (* ( Cardinality ( container_ y )  )  1) (* ( Cardinality ( container_ x )  )  k2c8acb06_ff95_4751_9c70_3ced7154f447)) (>= k2c8acb06_ff95_4751_9c70_3ced7154f447 0))))))
+(assert (! (forall ((v Int)) (=> (and ( type_f98975bc_f44c_4fea_a8d1_931336031c56_Student v )  ( type_f98975bc_f44c_4fea_a8d1_931336031c56_Person v ) ) (> ( person_age ( obj_80fc0bf1_e6bc_49f5_81ef_35f9a0752dfa v )  )  18))):named l0))
+(assert (! (forall ((s1 Int)(s2 Int)) (=> (and (and ( type_f98975bc_f44c_4fea_a8d1_931336031c56_Student s1 )  ( type_f98975bc_f44c_4fea_a8d1_931336031c56_Person s1 ) ) (and ( type_f98975bc_f44c_4fea_a8d1_931336031c56_Student s2 )  ( type_f98975bc_f44c_4fea_a8d1_931336031c56_Person s2 ) )) (=> (not (= ( obj_80fc0bf1_e6bc_49f5_81ef_35f9a0752dfa s1 )  ( obj_80fc0bf1_e6bc_49f5_81ef_35f9a0752dfa s2 ) ) ) (not (= ( student_id ( obj_80fc0bf1_e6bc_49f5_81ef_35f9a0752dfa s1 )  )  ( student_id ( obj_80fc0bf1_e6bc_49f5_81ef_35f9a0752dfa s2 )  ) ) )))):named l1))
+(assert (! (and (forall ((v Int)) (=> (and ( type_f98975bc_f44c_4fea_a8d1_931336031c56_Student v )  ( type_f98975bc_f44c_4fea_a8d1_931336031c56_Person v ) ) (>= ( student_year ( obj_80fc0bf1_e6bc_49f5_81ef_35f9a0752dfa v )  )  1))) (forall ((v Int)) (=> (and ( type_f98975bc_f44c_4fea_a8d1_931336031c56_Student v )  ( type_f98975bc_f44c_4fea_a8d1_931336031c56_Person v ) ) (<= ( student_year ( obj_80fc0bf1_e6bc_49f5_81ef_35f9a0752dfa v )  )  6)))):named l2))
+(assert (! (and (exists ((s Int)) (and (and ( type_f98975bc_f44c_4fea_a8d1_931336031c56_Student s )  ( type_f98975bc_f44c_4fea_a8d1_931336031c56_Person s ) ) (= ( student_year ( obj_80fc0bf1_e6bc_49f5_81ef_35f9a0752dfa s )  )  6))) (exists ((s Int)) (and (and ( type_f98975bc_f44c_4fea_a8d1_931336031c56_Student s )  ( type_f98975bc_f44c_4fea_a8d1_931336031c56_Person s ) ) (< ( student_year ( obj_80fc0bf1_e6bc_49f5_81ef_35f9a0752dfa s )  )  6)))):named l3))
+(assert (! (forall ((s1 Int)) (=> (and ( type_f98975bc_f44c_4fea_a8d1_931336031c56_Student s1 )  ( type_f98975bc_f44c_4fea_a8d1_931336031c56_Person s1 ) ) (forall ((m1 Int)) (=> (and ( type_f98975bc_f44c_4fea_a8d1_931336031c56_Module m1 )  ( rel_513ed927_c474_4439_9b03_bfb41440ceac_choose ( obj_80fc0bf1_e6bc_49f5_81ef_35f9a0752dfa s1 )   ( obj_80fc0bf1_e6bc_49f5_81ef_35f9a0752dfa m1 )  ) ) (= ( student_year ( obj_80fc0bf1_e6bc_49f5_81ef_35f9a0752dfa s1 )  )  ( module_year ( obj_80fc0bf1_e6bc_49f5_81ef_35f9a0752dfa m1 )  ) ))))):named l4))
+(assert (! (forall ((s Int)) (=> (and ( type_f98975bc_f44c_4fea_a8d1_931336031c56_Student s )  ( type_f98975bc_f44c_4fea_a8d1_931336031c56_Person s ) ) (exists ((v Int)) (and ( type_f98975bc_f44c_4fea_a8d1_931336031c56_Module v )  ( rel_513ed927_c474_4439_9b03_bfb41440ceac_choose ( obj_80fc0bf1_e6bc_49f5_81ef_35f9a0752dfa s )   ( obj_80fc0bf1_e6bc_49f5_81ef_35f9a0752dfa v )  ) )))):named l5))
+(assert (! (exists ((o Int)) (and ( type_f98975bc_f44c_4fea_a8d1_931336031c56_Child ( obj_80fc0bf1_e6bc_49f5_81ef_35f9a0752dfa o )  )  ( type_f98975bc_f44c_4fea_a8d1_931336031c56_Person ( obj_80fc0bf1_e6bc_49f5_81ef_35f9a0752dfa o )  ) )):named c0))
+(assert (! (exists ((o Int)) ( type_f98975bc_f44c_4fea_a8d1_931336031c56_Department ( obj_80fc0bf1_e6bc_49f5_81ef_35f9a0752dfa o )  ) ):named c1))
+(assert (! (exists ((o Int)) ( type_f98975bc_f44c_4fea_a8d1_931336031c56_Module ( obj_80fc0bf1_e6bc_49f5_81ef_35f9a0752dfa o )  ) ):named c2))
+(assert (! (exists ((o Int)) ( type_f98975bc_f44c_4fea_a8d1_931336031c56_Person ( obj_80fc0bf1_e6bc_49f5_81ef_35f9a0752dfa o )  ) ):named c3))
+(assert (! (exists ((o Int)) (and ( type_f98975bc_f44c_4fea_a8d1_931336031c56_Student ( obj_80fc0bf1_e6bc_49f5_81ef_35f9a0752dfa o )  )  ( type_f98975bc_f44c_4fea_a8d1_931336031c56_Person ( obj_80fc0bf1_e6bc_49f5_81ef_35f9a0752dfa o )  ) )):named c4))
+(assert (! (exists ((o Int)) ( type_f98975bc_f44c_4fea_a8d1_931336031c56_University ( obj_80fc0bf1_e6bc_49f5_81ef_35f9a0752dfa o )  ) ):named c5))
 
  ;end of formula 
diff --git a/src/main/org/tzi/use/main/shell/Shell.java b/src/main/org/tzi/use/main/shell/Shell.java
@@ -385,6 +385,8 @@ private void processLine(String line) throws NoSystemException {
             cmdHelp(line);
 		else if (line.startsWith("maxuse"))
 			cmdMaxuse(line);
+        else if (line.startsWith("select")||line.startsWith("Select"))
+            query_help();
         else if (line.equals("q") || line.equals("quit") || line.equals("exit"))
             cmdExit();
         else if (line.equals("qverify"))
@@ -785,6 +787,12 @@ else if (line.equals("maxuse")){
         //threadCounter.start();
 	}
 
+    private void query_help() throws NoSystemException{
+        System.out.println("QMaxUSE Help v1.0");
+        System.out.println("please use a $ at the begin of a selection statement.");
+        System.out.println("Use command <qverify> to start concurrent verification.");
+    }
+
     private void query(String line) throws NoSystemException{
         // compile query
         MSystem system;
@@ -795,6 +803,7 @@ private void query(String line) throws NoSystemException{
             MModel model = new ModelFactory().createModel("empty model");
             system = new MSystem(model);
         }
+
         InputStream stream = new ByteArrayInputStream(line.getBytes());
         //int r = QueryCompiler.compileExpression(system.model(),system.state(),stream,"<input>",new PrintWriter(System.err),system.varBindings());
         int r =QueryCompiler.compileExpression(system.model(),system.state(),stream,"<input>",new PrintWriter(System.err));

diff --git a/src/main/org/tzi/use/parser/generator/GeneratorLexer.java b/src/main/org/tzi/use/parser/generator/GeneratorLexer.java
@@ -1,4 +1,4 @@
-// $ANTLR 3.4 Generator.g 2021-10-08 12:03:38
+// $ANTLR 3.4 Generator.g 2021-10-08 14:15:21
 
 package org.tzi.use.parser.generator;
 

diff --git a/src/main/org/tzi/use/parser/generator/GeneratorParser.java b/src/main/org/tzi/use/parser/generator/GeneratorParser.java
@@ -1,4 +1,4 @@
-// $ANTLR 3.4 Generator.g 2021-10-08 12:03:38
+// $ANTLR 3.4 Generator.g 2021-10-08 14:15:21
 
 /*
  * USE - UML based specification environment

diff --git a/src/main/org/tzi/use/parser/ocl/OCLLexer.java b/src/main/org/tzi/use/parser/ocl/OCLLexer.java
@@ -1,4 +1,4 @@
-// $ANTLR 3.4 OCL.g 2021-10-08 12:03:32
+// $ANTLR 3.4 OCL.g 2021-10-08 14:15:14
 
 package org.tzi.use.parser.ocl; 
 

diff --git a/src/main/org/tzi/use/parser/ocl/OCLParser.java b/src/main/org/tzi/use/parser/ocl/OCLParser.java
@@ -1,4 +1,4 @@
-// $ANTLR 3.4 OCL.g 2021-10-08 12:03:31
+// $ANTLR 3.4 OCL.g 2021-10-08 14:15:14
 
 /*
  * USE - UML based specification environment

diff --git a/src/main/org/tzi/use/parser/shell/ShellCommandLexer.java b/src/main/org/tzi/use/parser/shell/ShellCommandLexer.java
@@ -1,4 +1,4 @@
-// $ANTLR 3.4 ShellCommand.g 2021-10-08 12:03:37
+// $ANTLR 3.4 ShellCommand.g 2021-10-08 14:15:20
 
 /*
  * USE - UML based specification environment

diff --git a/src/main/org/tzi/use/parser/shell/ShellCommandParser.java b/src/main/org/tzi/use/parser/shell/ShellCommandParser.java
@@ -1,4 +1,4 @@
-// $ANTLR 3.4 ShellCommand.g 2021-10-08 12:03:36
+// $ANTLR 3.4 ShellCommand.g 2021-10-08 14:15:19
 
 /*
  * USE - UML based specification environment

diff --git a/src/main/org/tzi/use/parser/soil/SoilLexer.java b/src/main/org/tzi/use/parser/soil/SoilLexer.java
@@ -1,4 +1,4 @@
-// $ANTLR 3.4 Soil.g 2021-10-08 12:03:33
+// $ANTLR 3.4 Soil.g 2021-10-08 14:15:16
 
 /*
  * USE - UML based specification environment

diff --git a/src/main/org/tzi/use/parser/soil/SoilParser.java b/src/main/org/tzi/use/parser/soil/SoilParser.java
@@ -1,4 +1,4 @@
-// $ANTLR 3.4 Soil.g 2021-10-08 12:03:32
+// $ANTLR 3.4 Soil.g 2021-10-08 14:15:15
 
 /*
  * USE - UML based specification environment

diff --git a/src/main/org/tzi/use/parser/testsuite/TestSuiteLexer.java b/src/main/org/tzi/use/parser/testsuite/TestSuiteLexer.java
@@ -1,4 +1,4 @@
-// $ANTLR 3.4 TestSuite.g 2021-10-08 12:03:40
+// $ANTLR 3.4 TestSuite.g 2021-10-08 14:15:23
 
 /*
  * USE - UML based specification environment

diff --git a/src/main/org/tzi/use/parser/testsuite/TestSuiteParser.java b/src/main/org/tzi/use/parser/testsuite/TestSuiteParser.java
@@ -1,4 +1,4 @@
-// $ANTLR 3.4 TestSuite.g 2021-10-08 12:03:39
+// $ANTLR 3.4 TestSuite.g 2021-10-08 14:15:22
 
 /*
  * USE - UML based specification environment

diff --git a/src/main/org/tzi/use/parser/use/USELexer.java b/src/main/org/tzi/use/parser/use/USELexer.java
@@ -1,4 +1,4 @@
-// $ANTLR 3.4 USE.g 2021-10-08 12:03:34
+// $ANTLR 3.4 USE.g 2021-10-08 14:15:17
 
 /*
  * USE - UML based specification environment

diff --git a/src/main/org/tzi/use/parser/use/USEParser.java b/src/main/org/tzi/use/parser/use/USEParser.java
@@ -1,4 +1,4 @@
-// $ANTLR 3.4 USE.g 2021-10-08 12:03:34
+// $ANTLR 3.4 USE.g 2021-10-08 14:15:17
 
 /*
  * USE - UML based specification environment

diff --git a/src/main/org/tzi/use/query/QueryLexer.java b/src/main/org/tzi/use/query/QueryLexer.java
@@ -1,4 +1,4 @@
-// $ANTLR 3.4 Query.g 2021-10-08 12:03:36
+// $ANTLR 3.4 Query.g 2021-10-08 14:15:18
 
 package org.tzi.use.query;
 import org.tzi.use.query.ast.*;

diff --git a/src/main/org/tzi/use/query/QueryParser.java b/src/main/org/tzi/use/query/QueryParser.java
@@ -1,4 +1,4 @@
-// $ANTLR 3.4 Query.g 2021-10-08 12:03:35
+// $ANTLR 3.4 Query.g 2021-10-08 14:15:18
 
 package org.tzi.use.query;
 import org.tzi.use.query.ast.*;