Skip to content
Snippets Groups Projects
Commit b450e1a5 authored by hansen's avatar hansen
Browse files

Refactoring

parent 926f3d5a
No related branches found
No related tags found
No related merge requests found
Showing
with 74 additions and 59 deletions
...@@ -6,7 +6,7 @@ apply plugin: 'jacoco' ...@@ -6,7 +6,7 @@ apply plugin: 'jacoco'
project.version = '1.0.0-SNAPSHOT' project.version = '1.0.0-SNAPSHOT'
project.group = 'de.prob' project.group = 'de.prob'
sourceCompatibility = 1.5 //sourceCompatibility = 1.5
repositories { repositories {
mavenCentral() mavenCentral()
...@@ -38,7 +38,7 @@ dependencies { ...@@ -38,7 +38,7 @@ dependencies {
testCompile (group: 'junit', name: 'junit', version: '4.7') testCompile (group: 'junit', name: 'junit', version: '4.11')
testCompile (group: 'de.prob', name: 'tla2bAST', version: '1.0.5-SNAPSHOT') testCompile (group: 'de.prob', name: 'tla2bAST', version: '1.0.5-SNAPSHOT')
releaseJars (group: 'de.tla', name: 'tlatools', version: '1.0.0-SNAPSHOT') releaseJars (group: 'de.tla', name: 'tlatools', version: '1.0.0-SNAPSHOT')
...@@ -49,8 +49,8 @@ dependencies { ...@@ -49,8 +49,8 @@ dependencies {
} }
jacoco { jacoco {
toolVersion = "0.6.2.201302030002" toolVersion = "0.7.1.201405082137"
reportsDir = file("$buildDir/customJacocoReportDir") reportsDir = file("$buildDir/JacocoReports")
} }
jacocoTestReport { jacocoTestReport {
...@@ -69,13 +69,20 @@ test { ...@@ -69,13 +69,20 @@ test {
} }
task integrationtests(type: Test){ task integrationTests(type: Test){
doFirst{ println("Running integration tests") } doFirst{ println("Running integration tests") }
scanForTestClasses = true scanForTestClasses = true
//include('de/tlc4b/tlc/integration/probprivate/**') //include('de/tlc4b/tlc/integration/probprivate/**')
include('de/tlc4b/**') include('de/tlc4b/**')
} }
// type 'gradle integrationTests jacocoIntegrationTestReport' in order to run the jacoco code coverage analysis
task jacocoIntegrationTestReport(type: JacocoReport) {
sourceSets sourceSets.main
//executionData files('build/jacoco/integrationTests.exec')
executionData fileTree(project.rootDir.absolutePath).include("**/build/jacoco/*.exec")
}
jar { from sourceSets.main.allJava } jar { from sourceSets.main.allJava }
jar { jar {
from configurations.releaseJars.collect { it.isDirectory() ? it : zipTree(it) } from configurations.releaseJars.collect { it.isDirectory() ? it : zipTree(it) }
......
...@@ -10,11 +10,8 @@ import java.io.InputStream; ...@@ -10,11 +10,8 @@ import java.io.InputStream;
import java.io.OutputStreamWriter; import java.io.OutputStreamWriter;
import java.io.UnsupportedEncodingException; import java.io.UnsupportedEncodingException;
import java.util.LinkedHashMap; import java.util.LinkedHashMap;
import java.util.Map;
import java.util.Set;
import java.util.Map.Entry; import java.util.Map.Entry;
import tlc2.TLCGlobals;
import de.be4.classicalb.core.parser.exceptions.BException; import de.be4.classicalb.core.parser.exceptions.BException;
import de.tlc4b.TLC4BGlobals; import de.tlc4b.TLC4BGlobals;
import de.tlc4b.analysis.UsedStandardModules.STANDARD_MODULES; import de.tlc4b.analysis.UsedStandardModules.STANDARD_MODULES;
...@@ -45,7 +42,7 @@ public class TLC4B { ...@@ -45,7 +42,7 @@ public class TLC4B {
// windows // windows
TLC4B tlc4b = new TLC4B(); TLC4B tlc4b = new TLC4B();
try { try {
tlc4b.progress(args); tlc4b.process(args);
} catch (BException e) { } catch (BException e) {
System.err.println("***** Parsing Error *****"); System.err.println("***** Parsing Error *****");
System.err.println(e.getMessage()); System.err.println(e.getMessage());
...@@ -159,7 +156,7 @@ public class TLC4B { ...@@ -159,7 +156,7 @@ public class TLC4B {
// B2TLAGlobals.setCleanup(true); // B2TLAGlobals.setCleanup(true);
TLC4B tlc4b = new TLC4B(); TLC4B tlc4b = new TLC4B();
try { try {
tlc4b.progress(args); tlc4b.process(args);
} catch (Exception e) { } catch (Exception e) {
e.printStackTrace(); e.printStackTrace();
System.err.println(e.getMessage()); System.err.println(e.getMessage());
...@@ -272,7 +269,7 @@ public class TLC4B { ...@@ -272,7 +269,7 @@ public class TLC4B {
} }
} }
public void progress(String[] args) throws IOException, BException { public void process(String[] args) throws IOException, BException {
handleParameter(args); handleParameter(args);
System.out.print("Arguments: "); System.out.print("Arguments: ");
......
...@@ -110,6 +110,10 @@ public class TLCRunner { ...@@ -110,6 +110,10 @@ public class TLCRunner {
list.add("" + 60); list.add("" + 60);
} }
list.add("-maxSetSize");
list.add("100000000");
// list.add("-config"); // list.add("-config");
// list.add(machineName + ".cfg"); // list.add(machineName + ".cfg");
list.add(machineName); list.add(machineName);
......
...@@ -7,11 +7,9 @@ import java.util.Iterator; ...@@ -7,11 +7,9 @@ import java.util.Iterator;
import java.util.LinkedList; import java.util.LinkedList;
import java.util.List; import java.util.List;
import tlc2.TLCGlobals;
import de.be4.classicalb.core.parser.Utils; import de.be4.classicalb.core.parser.Utils;
import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter; import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
import de.be4.classicalb.core.parser.node.*; import de.be4.classicalb.core.parser.node.*;
import de.tlc4b.TLC4B;
import de.tlc4b.TLC4BGlobals; import de.tlc4b.TLC4BGlobals;
import de.tlc4b.analysis.MachineContext; import de.tlc4b.analysis.MachineContext;
import de.tlc4b.analysis.PrecedenceCollector; import de.tlc4b.analysis.PrecedenceCollector;
......
...@@ -12,8 +12,6 @@ import de.tlc4b.analysis.Typechecker; ...@@ -12,8 +12,6 @@ import de.tlc4b.analysis.Typechecker;
import de.tlc4b.btypes.BType; import de.tlc4b.btypes.BType;
import de.tlc4b.tla.ConfigFile; import de.tlc4b.tla.ConfigFile;
import de.tlc4b.tla.TLAModule; import de.tlc4b.tla.TLAModule;
import de.tlc4b.tla.config.ConfigFileAssignment;
import de.tlc4b.tla.config.ModelValueAssignment;
public class TLCOutputInfo { public class TLCOutputInfo {
......
...@@ -233,14 +233,6 @@ public class TLCResults implements ToolGlobals { ...@@ -233,14 +233,6 @@ public class TLCResults implements ToolGlobals {
} }
private void evalErrorMessage(Message m) { private void evalErrorMessage(Message m) {
// System.out.println(------------------);
// System.out.print(m.getMessageCode() + " " +
// m.getParameters().length);
// for (int i = 0; i < m.getParameters().length; i++) {
// System.out.print(" " + m.getParameters()[i]);
// }
// System.out.println();
switch (m.getMessageCode()) { switch (m.getMessageCode()) {
case EC.TLC_INVARIANT_VIOLATED_INITIAL: case EC.TLC_INVARIANT_VIOLATED_INITIAL:
case EC.TLC_INVARIANT_VIOLATED_BEHAVIOR: case EC.TLC_INVARIANT_VIOLATED_BEHAVIOR:
...@@ -306,6 +298,8 @@ public class TLCResults implements ToolGlobals { ...@@ -306,6 +298,8 @@ public class TLCResults implements ToolGlobals {
} }
private TLCResult evaluatingParameter(String[] params) { private TLCResult evaluatingParameter(String[] params) {
System.out.println(params.length);
System.out.println(params[0]);
for (int i = 0; i < params.length; i++) { for (int i = 0; i < params.length; i++) {
String s = params[i]; String s = params[i];
if (s.contains("not enumerable")) { if (s.contains("not enumerable")) {
...@@ -319,11 +313,13 @@ public class TLCResults implements ToolGlobals { ...@@ -319,11 +313,13 @@ public class TLCResults implements ToolGlobals {
} else if (s.contains("which is not in the domain of the function")) { } else if (s.contains("which is not in the domain of the function")) {
return WellDefinednessError; return WellDefinednessError;
} else if (s.contains("tlc2.module.TLC.Assert")) { } else if (s.contains("tlc2.module.TLC.Assert")) {
return tlcResult = WellDefinednessError; return WellDefinednessError;
} else if (s } else if (s
.contains("CHOOSE x \\in S: P, but no element of S satisfied P") .contains("CHOOSE x \\in S: P, but no element of S satisfied P")
&& s.contains("module FunctionsAsRelations")) { && s.contains("module FunctionsAsRelations")) {
return tlcResult = WellDefinednessError; return tlcResult = WellDefinednessError;
} else if (s.contains("The property of ASSERT_LTL")) {
return TemporalPropertyViolation;
} }
} }
......
...@@ -14,7 +14,7 @@ import de.tlc4b.exceptions.ScopeException; ...@@ -14,7 +14,7 @@ import de.tlc4b.exceptions.ScopeException;
import de.tlc4b.exceptions.TypeErrorException; import de.tlc4b.exceptions.TypeErrorException;
public class LtlFormulaTest { public class LTLFormulaTest {
@BeforeClass @BeforeClass
public static void setUp(){ public static void setUp(){
......
...@@ -4,8 +4,6 @@ import static de.tlc4b.util.TestUtil.compare; ...@@ -4,8 +4,6 @@ import static de.tlc4b.util.TestUtil.compare;
import org.junit.Test; import org.junit.Test;
import de.tlc4b.TLC4BGlobals;
public class NumbersTest { public class NumbersTest {
......
package de.tlc4b.tlc.integration; package de.tlc4b.tlc.integration;
/**
* If the result is not correctly detected in the TLC output, @see de.tlc4b.tlc.TLCResult .
* */
import static org.junit.Assert.assertEquals; import static org.junit.Assert.assertEquals;
import org.junit.BeforeClass; import org.junit.BeforeClass;
...@@ -52,4 +54,10 @@ public class LTLTest { ...@@ -52,4 +54,10 @@ public class LTLTest {
assertEquals(NoError, test(a)); assertEquals(NoError, test(a));
} }
@Test
public void testLTLStatePropertyViolation() throws Exception{
String[] a = new String[] { ".\\src\\test\\resources\\ltl\\StatePropertyViolation.mch" };
assertEquals(TemporalPropertyViolation, test(a));
}
} }
...@@ -208,7 +208,7 @@ public class TestUtil { ...@@ -208,7 +208,7 @@ public class TestUtil {
// B2TLAGlobals.setCleanup(true); // B2TLAGlobals.setCleanup(true);
TLC4B tlc4b = new TLC4B(); TLC4B tlc4b = new TLC4B();
try { try {
tlc4b.progress(args); tlc4b.process(args);
} catch (Exception e) { } catch (Exception e) {
e.printStackTrace(); e.printStackTrace();
System.err.println(e.getMessage()); System.err.println(e.getMessage());
......
package testing; package testing;
import java.io.File; import java.io.File;
import java.io.IOException; import java.io.IOException;
import java.util.ArrayList; import java.util.ArrayList;
import java.util.Hashtable;
import java.util.List; import java.util.List;
import java.util.Map; import java.util.Map;
import org.junit.Ignore; import org.junit.Ignore;
import org.junit.Test; import org.junit.Test;
import de.be4.classicalb.core.parser.BParser; import de.be4.classicalb.core.parser.BParser;
import de.be4.classicalb.core.parser.analysis.pragma.Pragma; import de.be4.classicalb.core.parser.analysis.pragma.Pragma;
import de.be4.classicalb.core.parser.analysis.prolog.RecursiveMachineLoader; import de.be4.classicalb.core.parser.analysis.prolog.RecursiveMachineLoader;
import de.be4.classicalb.core.parser.exceptions.BException; import de.be4.classicalb.core.parser.exceptions.BException;
import de.be4.classicalb.core.parser.node.Start; import de.be4.classicalb.core.parser.node.Start;
import de.tlc4b.analysis.MachineContext;
import de.tlc4b.util.Ast2String; import de.tlc4b.util.Ast2String;
public class CompoundScopeTest { public class CompoundScopeTest {
...@@ -39,20 +32,22 @@ public class CompoundScopeTest { ...@@ -39,20 +32,22 @@ public class CompoundScopeTest {
BParser parser = new BParser(filename); BParser parser = new BParser(filename);
Start tree = parser.parseFile(machineFile, false); Start tree = parser.parseFile(machineFile, false);
RecursiveMachineLoader r = new RecursiveMachineLoader(machineFile.getParent(), parser.getContentProvider()); RecursiveMachineLoader r = new RecursiveMachineLoader(
machineFile.getParent(), parser.getContentProvider());
List<Pragma> pragmas = new ArrayList<Pragma>(); List<Pragma> pragmas = new ArrayList<Pragma>();
pragmas.addAll(parser.getPragmas()); pragmas.addAll(parser.getPragmas());
r.loadAllMachines(machineFile, tree, parser.getSourcePositions(), parser.getDefinitions(), pragmas); r.loadAllMachines(machineFile, tree, parser.getSourcePositions(),
parser.getDefinitions(), pragmas);
// r.printAsProlog(new PrintWriter(System.out), false); // r.printAsProlog(new PrintWriter(System.out), false);
Map<String, Start> map = r.getParsedMachines(); Map<String, Start> map = r.getParsedMachines();
ArrayList<String> list = new ArrayList<String>(map.keySet()); ArrayList<String> list = new ArrayList<String>(map.keySet());
// Hashtable<String, MachineContext> machineContextsTable = new
//Hashtable<String, MachineContext> machineContextsTable = new Hashtable<String, MachineContext>(); // Hashtable<String, MachineContext>();
//Hashtable<String, Typechecker> typecheckerTable = new Hashtable<String, Typechecker>(); // Hashtable<String, Typechecker> typecheckerTable = new
// Hashtable<String, Typechecker>();
for (int i = 0; i < list.size(); i++) { for (int i = 0; i < list.size(); i++) {
String name = list.get(i); String name = list.get(i);
// System.out.println(name); // System.out.println(name);
...@@ -61,11 +56,11 @@ public class CompoundScopeTest { ...@@ -61,11 +56,11 @@ public class CompoundScopeTest {
start.apply(ast2String2); start.apply(ast2String2);
System.out.println(ast2String2.toString()); System.out.println(ast2String2.toString());
//MachineContext c = new MachineContext(start, machineContextsTable); // MachineContext c = new MachineContext(start,
// machineContextsTable);
// machineContextsTable.put(name, c); // machineContextsTable.put(name, c);
} }
} }
} }
...@@ -2,7 +2,6 @@ package testing; ...@@ -2,7 +2,6 @@ package testing;
import java.io.File; import java.io.File;
import java.io.IOException; import java.io.IOException;
import java.io.PrintWriter;
import java.util.ArrayList; import java.util.ArrayList;
import java.util.List; import java.util.List;
......
MACHINE CounterLTL MACHINE CounterError
DEFINITIONS DEFINITIONS
ASSERT_LTL_1 == "F {x = 12}" ASSERT_LTL_1 == "F {x = 12}"
VARIABLES x VARIABLES x
......
MACHINE StatePropertyViolation
DEFINITIONS
ASSERT_LTL_1 == "!a.({a:ID} => {1=2})"
SETS
ID={aa,bb}
CONSTANTS iv
PROPERTIES
iv:ID
VARIABLES xx
INVARIANT
xx:POW(ID)
INITIALISATION xx:={}
OPERATIONS
Set(yy) = SELECT yy:ID & yy /:xx THEN xx:= xx \/ {yy} END
END
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment