Skip to content
Snippets Groups Projects
Commit 7b6c193c authored by Jens Bendisposto's avatar Jens Bendisposto
Browse files

Merge branch 'develop' of github.com:bendisposto/prob into develop

parents b8fce742 f441e987
Branches
Tags
No related merge requests found
Show whitespace changes
Inline Side-by-side
Showing
with 75 additions and 51 deletions
.travis.yml
+ 18
− 1
View file @ 7b6c193c
language: java
script: gradle createPoms downloadCli collectDependencies && mvn -f de.prob.parent/pom.xml install && gradle collectArtifacts
sudo: true
before_install:
- sudo rm -f /etc/mavenrc
- wget http://www.us.apache.org/dist/maven/maven-3/3.0.5/binaries/apache-maven-3.0.5-bin.tar.gz
- tar -zxvf apache-maven-3.0.5-bin.tar.gz
- export MAVEN_OPTS="-Xmx512m -XX:MaxPermSize=192m"
- export M2_HOME=$PWD/apache-maven-3.0.5
- export PATH=$M2_HOME/bin:$PATH
- mvn --version
script:
- gradle createPoms
- gradle downloadCli
- gradle collectDependencies
- ant -f de.bmotionstudio.help/customBuild.xml generate-help
- mvn -f de.prob.parent/pom.xml install
- gradle collectArtifacts
branches:
only:
- develop
......
README.md
+ 2
− 0
View file @ 7b6c193c
<img src="https://github.com/bendisposto/prob/raw/develop/logo.png" width="500" align="center">
[![Build Status](https://travis-ci.org/bendisposto/prob.svg?branch=develop)](https://travis-ci.org/bendisposto/prob)
# The ProB Model Checker and Animator
[![Build Status](https://travis-ci.org/bendisposto/prob.svg?branch=develop)](https://travis-ci.org/bendisposto/prob)
......
build.gradle
+ 11
− 17
View file @ 7b6c193c
......@@ -28,24 +28,21 @@ completeInstall.dependsOn bMotionStudioHelpCustumBuild
project(':de.prob.core') {
repositories {
maven {
name "cobra"
url "http://cobra.cs.uni-duesseldorf.de/artifactory/repo"
}
mavenCentral()
}
def parser_version = '2.4.33-SNAPSHOT'
def parser_version = '2.4.40'
dependencies {
compile group: "de.prob", name: "answerparser", version: parser_version , changing: true
compile group: "de.prob", name: "bparser", version: parser_version , changing: true
compile group: "de.prob", name: "cliparser", version: parser_version , changing: true
compile group: "de.prob", name: "ltlparser", version: parser_version , changing: true
compile group: "de.prob", name: "parserbase", version: parser_version , changing: true
compile group: "de.prob", name: "prologlib", version: parser_version , changing: true
compile group: "de.prob", name: "unicode", version: parser_version , changing: true
compile group: "de.prob", name: "theorymapping", version: parser_version , changing: true
compile group: "de.hhu.stups", name: "answerparser", version: parser_version , changing: true
compile group: "de.hhu.stups", name: "bparser", version: parser_version , changing: true
compile group: "de.hhu.stups", name: "cliparser", version: parser_version , changing: true
compile group: "de.hhu.stups", name: "ltlparser", version: parser_version , changing: true
compile group: "de.hhu.stups", name: "parserbase", version: parser_version , changing: true
compile group: "de.hhu.stups", name: "prologlib", version: parser_version , changing: true
compile group: "de.hhu.stups", name: "unicode", version: parser_version , changing: true
compile group: "de.hhu.stups", name: "theorymapping", version: parser_version , changing: true
compile 'commons-lang:commons-lang:2.6'
}
......@@ -53,10 +50,7 @@ project(':de.prob.core') {
project(':de.prob.ui') {
repositories {
maven {
name "cobra"
url "http://cobra.cs.uni-duesseldorf.de/artifactory/repo"
}
mavenCentral()
}
dependencies {
compile 'commons-codec:commons-codec:1.6'
......
de.prob.core/prob_target.target
+ 2
− 2
View file @ 7b6c193c
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<?pde version="3.8"?><target name="prob_target" sequenceNumber="41">
<?pde version="3.8"?><target name="prob_target" sequenceNumber="42">
<locations>
<location includeAllPlatforms="false" includeConfigurePhase="false" includeMode="planner" includeSource="true" type="InstallableUnit">
<unit id="org.eclipse.gef.sdk.feature.group" version="3.9.101.201408150207"/>
......@@ -10,7 +10,7 @@
<repository location="http://rodin-b-sharp.sourceforge.net/updates/"/>
</location>
<location includeAllPlatforms="false" includeConfigurePhase="false" includeMode="planner" includeSource="true" type="InstallableUnit">
<unit id="org.rodinp.platform.product" version="3.1.0.201412171041-e1a03f3"/>
<unit id="org.rodinp.platform.product" version="3.2.0.201506220911-ecacdcb"/>
<repository location="http://rodin-b-sharp.sourceforge.net/core-updates/"/>
</location>
</locations>
......
de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/internal/DisproverCommand.java
+ 7
− 1
View file @ 7b6c193c
......@@ -81,6 +81,9 @@ public class DisproverCommand implements IComposableCommand {
Boolean.toString(prefNode.getBoolean("chr", true)));
final SetPreferenceCommand setCSE = new SetPreferenceCommand("CSE",
Boolean.toString(prefNode.getBoolean("cse", false)));
final SetPreferenceCommand setSMT = new SetPreferenceCommand(
"SMT_SUPPORTED_INTERPRETER", Boolean.toString(prefNode
.getBoolean("smt", false)));
final SetPreferenceCommand setCSEPred = new SetPreferenceCommand(
"CSE_PRED", Boolean.toString(prefNode.getBoolean("cse", false)));
final SetPreferenceCommand setDoubleEval = new SetPreferenceCommand(
......@@ -96,7 +99,8 @@ public class DisproverCommand implements IComposableCommand {
* prefNode.getInt("timeout", 1000));
composed = new ComposedCommand(clear, setPrefs, setCLPFD, setCHR,
setCSE, setCSEPred, setDoubleEval, load, start, disprove);
setSMT, setCSE, setCSEPred, setDoubleEval, load, start,
disprove);
final Job job = new ProBCommandJob("Disproving", animator, composed);
job.setUser(true);
......@@ -135,6 +139,8 @@ public class DisproverCommand implements IComposableCommand {
}
pto.closeList();
pto.printNumber(timeout);
pto.emptyList(); // do not submit extra options because we set the
// preference above
pto.printVariable(RESULT);
pto.closeTerm();
}
......
de.prob.eventb.disprover.ui/src/de/prob/eventb/disprover/ui/DisproverExtendedTimeoutTacticProvider.java
+ 28
− 25
View file @ 7b6c193c
package de.prob.eventb.disprover.ui;
import java.util.*;
import java.util.Collections;
import java.util.List;
import org.eclipse.swt.graphics.Image;
import org.eventb.core.ast.Predicate;
import org.eventb.core.seqprover.*;
import org.eventb.core.seqprover.IProofTreeNode;
import org.eventb.core.seqprover.IReasonerInput;
import org.eventb.core.seqprover.ITactic;
import org.eventb.core.seqprover.tactics.BasicTactics;
import org.eventb.ui.prover.*;
import org.eventb.ui.prover.DefaultTacticProvider;
import org.eventb.ui.prover.IPredicateApplication;
import org.eventb.ui.prover.ITacticApplication;
import de.prob.eventb.disprover.core.*;
import de.prob.eventb.disprover.core.Disprover;
import de.prob.eventb.disprover.core.DisproverReasonerInput;
public class DisproverExtendedTimeoutTacticProvider extends
DefaultTacticProvider {
protected boolean useContexts() {
return false;
}
protected static class MyPredicateApplication implements ITacticApplication {
private final IProofTreeNode node;
public MyPredicateApplication(IProofTreeNode node) {
this.node = node;
}
protected static class MyPredicateApplication implements
IPredicateApplication {
@Override
public ITactic getTactic(String[] inputs, String globalInput) {
return getTactic(node, globalInput, inputs);
}
public ITactic getTactic(IProofTreeNode node, String globalInput,
String[] inputs) {
IReasonerInput reasonerInput = new DisproverReasonerInput();
return BasicTactics.reasonerTac(
Disprover.createDisproverReasoner(), reasonerInput);
Disprover.createExtendedTimeoutDisproverReasoner(10),
reasonerInput);
}
@Override
......@@ -42,6 +33,18 @@ public class DisproverExtendedTimeoutTacticProvider extends
return "de.prob.eventb.disprover.ui.disproverTactic";
}
@Override
public Image getIcon() {
// TODO Auto-generated method stub
return null;
}
@Override
public String getTooltip() {
// TODO Auto-generated method stub
return null;
}
}
public DisproverExtendedTimeoutTacticProvider() {
......@@ -53,7 +56,7 @@ public class DisproverExtendedTimeoutTacticProvider extends
IProofTreeNode node, Predicate hyp, String globalInput) {
if (node != null && node.isOpen()) {
ITacticApplication application = new MyPredicateApplication(node);
ITacticApplication application = new MyPredicateApplication();
return Collections.singletonList(application);
}
return Collections.<ITacticApplication> emptyList();
......
de.prob.eventb.disprover.ui/src/de/prob/eventb/disprover/ui/DisproverPreferences.java
+ 7
− 0
View file @ 7b6c193c
......@@ -52,6 +52,7 @@ public class DisproverPreferences extends PreferencePage implements
private Button checkCLPFD;
private Button checkCHR;
private Button checkCSE;
private Button checkSMT;
private Button checkDoubleEval;
public DisproverPreferences() {
......@@ -149,6 +150,11 @@ public class DisproverPreferences extends PreferencePage implements
checkCSE = new Button(pageComponent, SWT.CHECK);
checkCSE.setSelection(prefNode.getBoolean("cse", false));
new Label(pageComponent, SWT.NONE)
.setText("Enable SMT Solver Support in Interpreter:");
checkSMT = new Button(pageComponent, SWT.CHECK);
checkSMT.setSelection(prefNode.getBoolean("smt", false));
new Label(pageComponent, SWT.NONE)
.setText("Check (Hypotheses ^ Goal) in addition to (Hypotheses ^ not Goal) to identify contradiction in hypotheses :");
checkDoubleEval = new Button(pageComponent, SWT.CHECK);
......@@ -163,6 +169,7 @@ public class DisproverPreferences extends PreferencePage implements
prefNode.putBoolean("clpfd", checkCLPFD.getSelection());
prefNode.putBoolean("chr", checkCHR.getSelection());
prefNode.putBoolean("cse", checkCSE.getSelection());
prefNode.putBoolean("smt", checkSMT.getSelection());
prefNode.putBoolean("doubleeval", checkDoubleEval.getSelection());
try {
prefNode.flush();
......
de.prob.eventb.disprover.ui/src/de/prob/eventb/disprover/ui/DisproverTacticProvider.java
+ 0
− 5
View file @ 7b6c193c
......@@ -17,11 +17,6 @@ import de.prob.eventb.disprover.core.Disprover;
import de.prob.eventb.disprover.core.DisproverReasonerInput;
public class DisproverTacticProvider extends DefaultTacticProvider {
protected boolean useContexts() {
return false;
}
protected static class MyPredicateApplication implements
IPredicateApplication {
@Override
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment