Docu, and changed package building plugin

e35d6ac7 · Sarah Grebing · b2d6b0e4 · e35d6ac7 · e35d6ac7 · e35d6ac7
Commit e35d6ac7 authored Jan 24, 2018 by Sarah Grebing
31 changed files
--- a/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/KeYMatcher.java
+++ b/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/KeYMatcher.java
@@ -156,7 +156,7 @@ public class KeYMatcher implements MatcherApi<KeyData> {
        }


-        assignments.forEach(variableAssignment -> System.out.println(variableAssignment));
+        // assignments.forEach(variableAssignment -> System.out.println(variableAssignment));
        return assignments.isEmpty()? null: assignments;
    }

@@ -198,11 +198,11 @@ public class KeYMatcher implements MatcherApi<KeyData> {
                    Value<String> value = toValueTerm(currentState.getData(), matched);
                    va.declare(s, value.getType());
                    va.assign(s, value);
-                    LOGGER.error("Variables to match " + s + " : " + value);
+                    //LOGGER.info("Variables to match " + s + " : " + value);
                }
            }
            List<VariableAssignment> retList = new LinkedList();
-            LOGGER.error("Matched Variables " + va.toString());
+            LOGGER.info("Matched Variables " + va.toString());
            retList.add(va);
            return retList;
        }

--- a/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/commands/assume.html
+++ b/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/commands/assume.html
+<!DOCTYPE html>
+<html lang="en">
+<head>
+
+<body>
+This command is currently not supported by PSDBG.
+</body>
+</html>
\ No newline at end of file
--- a/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/macros/auto.html
+++ b/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/macros/auto.html
--- a/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/commands/cut.html
+++ b/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/commands/cut.html
+<!DOCTYPE html>
+<html lang="en">
+<head>
+    <meta charset="UTF-8">
+    <title>smt</title>
+</head>
+<body>
+<h2 id="smt">smt</h2>
+<blockquote>
+    <p>Synopsis: <code>cut TERM</code></p>
+</blockquote>
+<p></strong>Description:</strong>
+    Performs a cut and thus splits the sequent into two goals. The unnamed
+    argument is the formula to cut with
+</p>
+
+
+<p><strong>Arguments:</strong></p>
+<ul>
+    <li><em>TERM</em> formula to cut with</li>
+</ul>
+
+Examples:
+<code>cut `value1 = value2`;</code>
+
+</body>
+</html>
--- a/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/commands/exit.html
+++ b/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/commands/exit.html
+<!DOCTYPE html>
+<html lang="en">
+<head>
+
+<body>
+This command is currently not supported by PSDBG.
+</body>
+</html>
\ No newline at end of file
--- a/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/commands/focus.html
+++ b/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/commands/focus.html
+<!DOCTYPE html>
+<html lang="en">
+<head>
+
+<body>
+This command is currently not supported by PSDBG.
+</body>
+</html>
\ No newline at end of file
--- a/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/commands/instantiate.html
+++ b/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/commands/instantiate.html
@@ -11,10 +11,10 @@
 </blockquote>
 <p><strong>Arguments:</strong></p>
 <ul>
-    <li><code>formula</code> : <em>TERM</em> (<em>R</em>)null</li>
-    <li><code>var</code> : <em>STRING</em> (<em>R</em>)null</li>
-    <li><code>occ</code> : <em>INT</em> (<em>R</em>)null</li>
-    <li><code>with</code> : <em>TERM</em> (<em>R</em>)null</li>
+    <li><code>formula</code> : <em>TERM</em> top-level formula where variables should be instantiated</li>
+    <li><code>var</code> : <em>STRING</em> the variable name that shoudl be instantiated</li>
+    <li><code>occ</code> : <em>INT</em> occurence of the top-level formula</li>
+    <li><code>with</code> : <em>TERM</em> the term with which variables should be instantiated</li>
 </ul>
 </body>
 </html>
\ No newline at end of file
--- a/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/commands/javascript.html
+++ b/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/commands/javascript.html
+<!DOCTYPE html>
+<html lang="en">
+<head>
+
+<body>
+This command is currently not supported by PSDBG.
+</body>
+</html>
\ No newline at end of file
--- a/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/commands/leave.html
+++ b/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/commands/leave.html
+<html lang="en">
+<head>
+
+<body>
+This command is currently not supported by PSDBG.
+</body>
+</html>
\ No newline at end of file
--- a/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/commands/let.html
+++ b/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/commands/let.html
+<!DOCTYPE html>
+<html lang="en">
+<head>
+    <meta charset="UTF-8">
+    <title>Title</title>
+</head>
+<body>
+
+</body>
+</html>
\ No newline at end of file
--- a/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/commands/macro.html
+++ b/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/commands/macro.html
+<!DOCTYPE html>
+<html lang="en">
+<head>
+    <meta charset="UTF-8">
+    <title>macro</title>
+</head>
+<body>
+<h2 id="macro">macro</h2>
+<blockquote>
+    <p>Synopsis: <code>macro macroname </code></p>
+</blockquote>
+<p></strong>Description:</strong>
+    The macro command applies the macro specified as argument
+</p>
+
+<code>macro</code> keyword can be ommited
+<p><strong>Arguments:</strong></p>
+<ul>
+    <li>macroname : <em>STRING</em> name of macro to apply</li>
+</ul>
+</body>
+</html>
\ No newline at end of file
--- a/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/commands/schemaVar.html
+++ b/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/commands/schemaVar.html
+<!DOCTYPE html>
+<html lang="en">
+<head>
+
+<body>
+This command is currently not supported by PSDBG.
+</body>
+</html>
\ No newline at end of file
--- a/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/commands/script.html
+++ b/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/commands/script.html
+<!DOCTYPE html>
+<html lang="en">
+<head>
+    <meta charset="UTF-8">
+    <title>Call to subscripts</title>
+</head>
+<body>
+<h2 id="script">Call to subscripts</h2>
+<blockquote>
+    <p>Synopsis: <code>scriptname; </code></p>
+</blockquote>
+Call of a subscript.
+<p><strong>Arguments:</strong></p>
+Arguments according to the subscript's declaration.
+</body>
+</html>
--- a/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/commands/select.html
+++ b/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/commands/select.html
+<!DOCTYPE html>
+<html lang="en">
+<head>
+
+<body>
+This command is currently not supported by PSDBG.
+</body>
+</html>
\ No newline at end of file
--- a/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/commands/set.html
+++ b/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/commands/set.html
+<!DOCTYPE html>
+<html lang="en">
+<head>
+
+<body>
+This command is currently not supported by PSDBG.
+</body>
+</html>
\ No newline at end of file
--- a/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/commands/skip.html
+++ b/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/commands/skip.html
+<!DOCTYPE html>
+<html lang="en">
+<head>
+
+<body>
+This command is currently not supported by PSDBG.
+</body>
+</html>
\ No newline at end of file
--- a/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/commands/smt.html
+++ b/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/commands/smt.html
+<!DOCTYPE html>
+<html lang="en">
+<head>
+    <meta charset="UTF-8">
+    <title>smt</title>
+</head>
+<body>
+<h2 id="smt">smt</h2>
+<blockquote>
+    <p>Synopsis: <code>smt solver=&lt;STRING&gt;</code></p>
+</blockquote>
+<p></strong>Description:</strong>
+
+    Invoke an external SMT solver. That solver must be adequately
+    configured outside the script mechanism. By default, Z3 is invoked,
+    but that can be chosen.
+</p>
+
+
+<p><strong>Arguments:</strong></p>
+<ul>
+    <li>solver : <em>STRING</em> comma separated list of SMT solvers (currently supported: "z3", "yices")</li>
+</ul>
+</body>
+</html>
\ No newline at end of file
--- a/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/macros/autopilot-prep.html
+++ b/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/macros/autopilot-prep.html
@@ -2,12 +2,12 @@
 <html lang="en">
 <head>
    <meta charset="UTF-8">
-    <title>autopilot-prep</title>
+    <title>autopilot_prep</title>
 </head>
 <body>
-<h2 id="autopilot-prep">autopilot-prep</h2>
+<h2 id="autopilot-prep">autopilot_prep</h2>
 <blockquote>
-    <p>Synopsis: <code>autopilot-prep;</code></p>
+    <p>Synopsis: <code>autopilot_prep;</code></p>
 </blockquote>
 <p><strong></strong>Description:</strong></strong></p>
 This macro performs the following steps:

--- a/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/macros/infflow-autopilot.html
+++ b/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/macros/infflow-autopilot.html
@@ -2,12 +2,12 @@
 <html lang="en">
 <head>
    <meta charset="UTF-8">
-    <title>infflow-autopilot</title>
+    <title>infflow_autopilot</title>
 </head>
 <body>
-<h2 id="infflow-autopilot">infflow-autopilot</h2>
+<h2 id="infflow-autopilot">infflow_autopilot</h2>
 <blockquote>
-    <p>Synopsis: <code>infflow-autopilot;</code></p>
+    <p>Synopsis: <code>infflow_autopilot;</code></p>
 </blockquote>
 <p><strong></strong>Description:</strong></strong></p>
 This macro is tailored to information flow problems.

--- a/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/macros/nosplit-prop.html
+++ b/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/macros/nosplit-prop.html
@@ -2,12 +2,12 @@
 <html lang="en">
 <head>
    <meta charset="UTF-8">
-    <title>nosplit-prop</title>
+    <title>nosplit_prop</title>
 </head>
 <body>
-<h2 id="symbex">nosplit-prop</h2>
+<h2 id="symbex">nosplit_prop</h2>
 <blockquote>
-    <p>Synopsis: <code>nosplit-prop;</code></p>
+    <p>Synopsis: <code>nosplit_prop;</code></p>
 </blockquote>
 <p><strong></strong>Description:</strong></strong></p>
 This macros applies rules to decompose propositional toplevel formulas without applying splitting rules.

--- a/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/macros/simp-heap.html
+++ b/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/macros/simp-heap.html
@@ -2,12 +2,12 @@
 <html lang="en">
 <head>
    <meta charset="UTF-8">
-    <title>simp-heap</title>
+    <title>simp_heap</title>
 </head>
 <body>
-<h2 id="symbex">simp-heap</h2>
+<h2 id="symbex">simp_heap</h2>
 <blockquote>
-    <p>Synopsis: <code>simp-heap;</code></p>
+    <p>Synopsis: <code>simp_heap;</code></p>
 </blockquote>
 <p><strong></strong>Description:</strong></strong></p>
 This macro performs simplification of Heap and LocSet terms.

--- a/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/macros/simp-int.html
+++ b/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/macros/simp-int.html
@@ -2,12 +2,12 @@
 <html lang="en">
 <head>
    <meta charset="UTF-8">
-    <title>simp-int</title>
+    <title>simp_int</title>
 </head>
 <body>
-<h2 id="symbex">simp-int</h2>
+<h2 id="symbex">simp_int</h2>
 <blockquote>
-    <p>Synopsis: <code>simp-int;</code></p>
+    <p>Synopsis: <code>simp_int;</code></p>
 </blockquote>
 <p><strong></strong>Description:</strong></strong></p>
 This macro performs simplification of integers and terms with integers.

--- a/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/macros/simp-upd.html
+++ b/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/macros/simp-upd.html
@@ -2,12 +2,12 @@
 <html lang="en">
 <head>
    <meta charset="UTF-8">
-    <title>simp-upd</title>
+    <title>simp_upd</title>
 </head>
 <body>
-<h2 id="simp-upd">simp-upd</h2>
+<h2 id="simp-upd">simp_upd</h2>
 <blockquote>
-    <p>Synopsis: <code>simp-upd;</code></p>
+    <p>Synopsis: <code>simp_upd;</code></p>
 </blockquote>
 <p><strong></strong>Description:</strong></strong></p>
 This macro applies only update simplification rules, i.e., that simplify the update term.

--- a/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/macros/split-prop.html
+++ b/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/macros/split-prop.html
@@ -5,9 +5,9 @@
    <title>split-prop</title>
 </head>
 <body>
-<h2 id="symbex">split-prop</h2>
+<h2 id="symbex">split_prop</h2>
 <blockquote>
-    <p>Synopsis: <code>split-prop;</code></p>
+    <p>Synopsis: <code>split_prop;</code></p>
 </blockquote>
 <p><strong></strong>Description:</strong></strong></p>
 This macros applies rules to decompose propositional toplevel formulas and also applies splitting rules.

--- a/ui/pom.xml
+++ b/ui/pom.xml
@@ -72,50 +72,29 @@

    <build>
        <plugins>
-
            <plugin>
-                <groupId>org.codehaus.mojo</groupId>
-                <artifactId>appassembler-maven-plugin</artifactId>
-                <version>1.10</version>
+                <groupId>org.apache.maven.plugins</groupId>
+                <artifactId>maven-assembly-plugin</artifactId>
                <configuration>
-                    <repositoryLayout>flat</repositoryLayout>
-                    <repositoryName>libs</repositoryName>
-                    <binFolder>./</binFolder>
-                    <!-- Set the target configuration directory to be used in the bin scripts -->
-                    <configurationDirectory>conf</configurationDirectory>
-                    <!-- Copy the contents from "/src/main/config" to the target
-                         configuration directory in the assembled application -->
-                    <copyConfigurationDirectory>true</copyConfigurationDirectory>
-                    <!-- Include the target configuration directory in the beginning of
-                         the classpath declaration in the bin scripts -->
-                    <includeConfigurationDirectoryInClasspath>true</includeConfigurationDirectoryInClasspath>
-                    <!-- set alternative assemble directory -->
-                    <assembleDirectory>${project.build.directory}/dist</assembleDirectory>
-                    <!-- Extra JVM arguments that will be included in the bin scripts -->
-                    <extraJvmArguments>-Xms128m</extraJvmArguments>
-                    <!-- Generate bin scripts for windows and unix pr default -->
-                    <platforms>
-                        <platform>windows</platform>
-                        <platform>unix</platform>
-                    </platforms>
-                    <programs>
-                        <program>
+                    <descriptorRefs>
+                        <descriptorRef>jar-with-dependencies</descriptorRef>
+                    </descriptorRefs>
+                    <archive>
+                        <manifest>
                            <mainClass>edu.kit.iti.formal.psdbg.gui.ProofScriptDebugger</mainClass>
-                            <id>psdbg</id>
-                            <!-- Only generate unix shell script for this application -->
-                            <platforms>
-                                <platform>unix</platform>
-                                <platform>windows</platform>
-                            </platforms>
-                        </program>
-                    </programs>
+                        </manifest>
+                    </archive>
                </configuration>
                <executions>
                    <execution>
                        <phase>package</phase>
+                        <goals>
+                            <goal>single</goal>
+                        </goals>
                    </execution>
                </executions>
            </plugin>
+            <!--HIER EVTL. PLUGIN HIN-->


            <plugin>

--- a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/CommandHelp.java
+++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/CommandHelp.java
@@ -121,9 +121,20 @@ public class CommandHelp extends BorderPane {
    class CommandEntry {
        String name, additionalInformation;

+
        @Override
        public String toString() {
-            return name + " (" + additionalInformation + ")";
+            return beautifyName(name) + " (" + additionalInformation + ")";
+        }
+
+        private String beautifyName(String cname) {
+            String ret;
+            if (cname.contains("-")) {
+                ret = cname.replace("-", "_");
+                return ret;
+            } else {
+                return cname;
+            }
        }
    }
 }
--- a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ScriptController.java
+++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ScriptController.java
@@ -317,7 +317,7 @@ public class ScriptController {
                lastScriptArea = area;
                lastRegion = r;
            } else {
-                logger.error("Could not find editor for: " + node.getOrigin());
+                logger.error("Could not find editor for the node to highlight: " + node.getOrigin());
            }
        }


--- a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/SequentMatcher.java
+++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/SequentMatcher.java
@@ -26,9 +26,7 @@ import javafx.scene.input.MouseEvent;
 import javafx.scene.layout.BorderPane;

 import java.util.HashMap;
-import java.util.List;
 import java.util.Map;
-import java.util.regex.Pattern;

 public class SequentMatcher extends BorderPane {

@@ -86,7 +84,7 @@ public class SequentMatcher extends BorderPane {
                    Range r = cursorPosition.get(pio);
                    sequentView.setStyleClass(r.start(), r.end(), "sequent-highlight");

-                    System.out.println("Highlight " + r.start() + " " + r.end());
+                    //System.out.println("Highlight " + r.start() + " " + r.end());
                });

            }

--- a/ui/src/main/resources/about.html
+++ b/ui/src/main/resources/about.html
@@ -18,7 +18,7 @@

 <h3>Thanks to:</h3>
 <ul>
-    <li>Lulu Luang</li>
+    <li>An Thuy Tien Luong</li>
    <li>Mattias Ulbrich</li>
 </ul>
 </body>

--- a/ui/src/main/resources/about.txt
+++ b/ui/src/main/resources/about.txt
@@ -12,4 +12,5 @@ Authors:
 * Alexander Weigl <weigl@ira.uka.de>
  https://formal.iti.kit.edu/~weigl

-* Lulu Lulong
+* An Thuy Tien Luong
+
--- a/website/docs/index.md
+++ b/website/docs/index.md
@@ -208,16 +208,18 @@ interactive rule applications.
 <h2>Downloads</h2>

 <ul>
- <li>PSDBG - <strong>Version 1.0-FM</strong> 
-    <a href="../psdbg_releases/psdbg-1.0-fm.jar">psdbg-1.0-fm.jar</a>
+ <li>PSDBG - <strong>Version 1.0.1b-FM</strong> 
+    <a href="../psdbg_releases/psdbg-1.0.1b-fm.jar">psdbg-1.0.1b-fm.jar</a>
    <br>
    Special Version for the tool paper at Formal Methods 2018.
    Including examples and all dependencies.
    <br>
+   <!-- Requires Java version 1.8.0_121 or higher -->
+    <br>
    <a href="https://www.gnu.org/licenses/gpl-3.0.txt">License: GPLv3</a>
    <a href="thirdparty.txt">Third Party Licenses</a> 
    <br>
-    Executable with <code>java -jar psdbg-1.0-fm.jar</code>
+    Executable with <code>java -jar psdbg-1.0.1b-fm.jar</code>
 </li>
 </ul>