Commit 518466c2 authored by Sarah Grebing's avatar Sarah Grebing
Browse files

removed comments in examples scripts

parent e35d6ac7
Pipeline #17348 passed with stages
in 10 minutes
...@@ -15,9 +15,12 @@ import java.nio.charset.Charset; ...@@ -15,9 +15,12 @@ import java.nio.charset.Charset;
public class JavaExample extends Example { public class JavaExample extends Example {
private URL projectFile;
public void setJavaFile(URL javaFile) { public void setJavaFile(URL javaFile) {
this.javaFile = javaFile; this.javaFile = javaFile;
} }
//public void setProjectFile(URL projectFile){this.projectFile = projectFile;}
protected URL javaFile; protected URL javaFile;
......
package edu.kit.iti.formal.psdbg.examples.lulu.bigIntProof;
import edu.kit.iti.formal.psdbg.examples.JavaExample;
public class BigIntExample extends JavaExample {
public BigIntExample() {
}
}
...@@ -6,15 +6,12 @@ import de.uka.ilkd.key.control.DefaultUserInterfaceControl; ...@@ -6,15 +6,12 @@ import de.uka.ilkd.key.control.DefaultUserInterfaceControl;
import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.java.Services;
import de.uka.ilkd.key.logic.Sequent; import de.uka.ilkd.key.logic.Sequent;
import de.uka.ilkd.key.logic.SequentFormula; import de.uka.ilkd.key.logic.SequentFormula;
import de.uka.ilkd.key.logic.Term;
import de.uka.ilkd.key.logic.op.SchemaVariable;
import de.uka.ilkd.key.macros.scripts.EngineState; import de.uka.ilkd.key.macros.scripts.EngineState;
import de.uka.ilkd.key.macros.scripts.RuleCommand; import de.uka.ilkd.key.macros.scripts.RuleCommand;
import de.uka.ilkd.key.macros.scripts.ScriptException; import de.uka.ilkd.key.macros.scripts.ScriptException;
import de.uka.ilkd.key.proof.Goal; import de.uka.ilkd.key.proof.Goal;
import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.proof.Node;
import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.proof.Proof;
import de.uka.ilkd.key.rule.inst.InstantiationEntry;
import edu.kit.iti.formal.psdbg.LabelFactory; import edu.kit.iti.formal.psdbg.LabelFactory;
import edu.kit.iti.formal.psdbg.RuleCommandHelper; import edu.kit.iti.formal.psdbg.RuleCommandHelper;
import edu.kit.iti.formal.psdbg.gui.controls.ScriptArea; import edu.kit.iti.formal.psdbg.gui.controls.ScriptArea;
...@@ -41,11 +38,13 @@ import lombok.val; ...@@ -41,11 +38,13 @@ import lombok.val;
import org.apache.logging.log4j.LogManager; import org.apache.logging.log4j.LogManager;
import org.apache.logging.log4j.Logger; import org.apache.logging.log4j.Logger;
import org.key_project.util.collection.ImmutableList; import org.key_project.util.collection.ImmutableList;
import org.key_project.util.collection.ImmutableMapEntry;
import recoder.util.Debug; import recoder.util.Debug;
import java.math.BigInteger; import java.math.BigInteger;
import java.util.*; import java.util.ArrayList;
import java.util.HashMap;
import java.util.List;
import java.util.Map;
import java.util.stream.Collectors; import java.util.stream.Collectors;
@Getter @Getter
...@@ -171,6 +170,7 @@ public class InteractiveModeController { ...@@ -171,6 +170,7 @@ public class InteractiveModeController {
int occ = rch.getOccurence(tap.getApp()); int occ = rch.getOccurence(tap.getApp());
Parameters callp = new Parameters(); Parameters callp = new Parameters();
// callp.put(new Variable("formula"), new TermLiteral(sfTerm));
callp.put(new Variable("formula"), new TermLiteral(sfTerm)); callp.put(new Variable("formula"), new TermLiteral(sfTerm));
callp.put(new Variable("occ"), new IntegerLiteral(BigInteger.valueOf(occ))); callp.put(new Variable("occ"), new IntegerLiteral(BigInteger.valueOf(occ)));
callp.put(new Variable("on"), new TermLiteral(onTerm)); callp.put(new Variable("on"), new TermLiteral(onTerm));
...@@ -289,6 +289,9 @@ public class InteractiveModeController { ...@@ -289,6 +289,9 @@ public class InteractiveModeController {
map.put("#2", call.getCommand()); map.put("#2", call.getCommand());
EngineState estate = new EngineState(g.proof()); EngineState estate = new EngineState(g.proof());
estate.setGoal(g); estate.setGoal(g);
// System.out.println("on = " + map.get("on"));
// System.out.println("formula = " +map.get("formula"));
// System.out.println("occ = " + map.get("occ"));
RuleCommand.Parameters cc = c.evaluateArguments(estate, map); //reflection exception RuleCommand.Parameters cc = c.evaluateArguments(estate, map); //reflection exception
AbstractUserInterfaceControl uiControl = new DefaultUserInterfaceControl(); AbstractUserInterfaceControl uiControl = new DefaultUserInterfaceControl();
......
...@@ -346,7 +346,6 @@ public class TacletContextMenu extends ContextMenu { ...@@ -346,7 +346,6 @@ public class TacletContextMenu extends ContextMenu {
pos.getPosInOccurrence());*/ pos.getPosInOccurrence());*/
//System.out.println("event = [" + event + "]"); //System.out.println("event = [" + event + "]");
Events.fire(new Events.TacletApplicationEvent(event, pos.getPosInOccurrence(), goal)); Events.fire(new Events.TacletApplicationEvent(event, pos.getPosInOccurrence(), goal));
} }
......
...@@ -9,6 +9,7 @@ script interactive(){ ...@@ -9,6 +9,7 @@ script interactive(){
impRight; impRight;
impRight; impRight;
impLeft; impLeft;
} }
script interactive_with_match(){ script interactive_with_match(){
......
...@@ -12,25 +12,3 @@ script main() { ...@@ -12,25 +12,3 @@ script main() {
close; close;
} }
script main1() {
impRight;
//instantiate var=`x` with=`c`;
//allLeft formula=`\forall` with=`a`;
//allLeft on=`\forall s x; f(f(x)) = f(x)` inst_t=`c`;
}
script proj() {
impRight;
eqSymm formula = `f(c) = f(f(f(c)))`;
instantiate var=`x` with=`f(f(c))`;
//allLeft on =`\forall s x; f(f(x)) = f(x)` inst_t=`f(f(c))`;
allLeft on =`\forall s x; f(f(x)) = f(x)` inst_t=`c`;
//applyEqRigid;
//applyEq formula=`f(f(f(c))) = f(c)` occ=`f(f(c))`;
//applyEq formula=`f(f(f(c))) = f(c)` occ=4;
applyEq on=`f(f(c))` formula=`f(f(f(c))) = f(c)` ;
close;
//close formula=`f(f(c))=f(c)`;
}
\ No newline at end of file
...@@ -208,18 +208,18 @@ interactive rule applications. ...@@ -208,18 +208,18 @@ interactive rule applications.
<h2>Downloads</h2> <h2>Downloads</h2>
<ul> <ul>
<li>PSDBG - <strong>Version 1.0.1b-FM</strong> <li>PSDBG - <strong>Version 1.0.1c-FM</strong>
<a href="../psdbg_releases/psdbg-1.0.1b-fm.jar">psdbg-1.0.1b-fm.jar</a> <a href="../psdbg_releases/psdbg-1.0.1c-fm.jar">psdbg-1.0.1c-fm.jar</a>
<br> <br>
Special Version for the tool paper at Formal Methods 2018. Special Version for the tool paper at Formal Methods 2018.
Including examples and all dependencies. Including examples and all dependencies.
<br> <br>
<!-- Requires Java version 1.8.0_121 or higher --> Requires Java version 1.8.0_111 or higher; Not working with Java 9, because of depdendencies.
<br> <br>
<a href="https://www.gnu.org/licenses/gpl-3.0.txt">License: GPLv3</a> <a href="https://www.gnu.org/licenses/gpl-3.0.txt">License: GPLv3</a>
<a href="thirdparty.txt">Third Party Licenses</a> <a href="thirdparty.txt">Third Party Licenses</a>
<br> <br>
Executable with <code>java -jar psdbg-1.0.1b-fm.jar</code> Executable with <code>java -jar psdbg-1.0.1c-fm.jar</code>
</li> </li>
</ul> </ul>
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment