Merge branch 'develop' into fregecspmparser

.bumpversion.cfg

@@ -0,0 +1,23 @@
+[bumpversion]
+current_version = 2.9.4-SNAPSHOT
+parse = (?P<major>\d+)\.(?P<minor>\d+)\.(?P<patch>\d+)(-(?P<release>\w+))?
+commit = False
+patch = True
+tag = False
+serialize =
+	{major}.{minor}.{patch}-{release}
+	{major}.{minor}.{patch}
+
+[bumpversion:file:build.gradle]
+
+[bumpversion:file:README.md]
+
+[bumpversion:file:src/main/resources/main.properties]
+
+[bumpversion:file:sonar-project.properties]
+
+[bumpversion:part:release]
+values =
+	SNAPSHOT
+	RC
+optional_value = RC

.gitignore

@@ -35,3 +35,11 @@ build.xml
 bparser/src/test/java/Testing.java
 build.properties
 .directory
+bparser-build.properties
+bparser/doc
+typechecker/doc
+translator/doc
+.rules-tags
+.rules-tags1
+.tags1
+.tags

.travis.yml

@@ -9,7 +9,7 @@ before_install:
 - openssl aes-256-cbc -pass pass:$ENCRYPTION_PASSWORD -in gradle.properties.enc -out
   gradle.properties -d
 addons:
-  sonarqube: 
+  sonarcloud:
     branches:
      - master
      - develop
@@ -18,10 +18,10 @@ install: /bin/true
 sudo: false
 
 script:
-  - TERM=dumb gradle clean deploy uploadArchives
-  - sonar-scanner -Dsonar.login=$SONAR_TOKEN
-
-after_success: curl -L $JENKINS_URL
+  - TERM=dumb ./gradlew clean deploy uploadArchives
+after_success:
+  - curl -L $JENKINS_URL
+  - TERM=dumb ./gradlew sonarqube --info --stacktrace
 env:
   global:
   - secure: laGlF46pirAFs3xrBTm+7AFi0CubtBj0PRLqhAe2q9wEhyUvU+LOhJZiqeyuc2FBzGOSlfevGhVOgmWxph6g2EP/bxhwiFywXD/CCzjDhca2JahMdYW925006jGIfh+QmWnxb7hoXUb+DvOoDQdHoiTPmVom2oTEGTctjLB4BhI=

README.md

@@ -1,19 +1,18 @@
 # ProB Parsers Library
 
 [![Build Status](https://travis-ci.org/bendisposto/probparsers.svg?branch=develop)](https://travis-ci.org/bendisposto/probparsers)
-[![SonarQube Tech Debt](https://img.shields.io/sonar/http/sonarqube.com/probparsers/tech_debt.svg?maxAge=2592000)](https://sonarqube.com/overview?id=probparsers)
 
 
 ## Using
 Releases are on [Maven Central](http://search.maven.org/#search%7Cga%7C1%7Cde.hhu.stups), Snapshots on https://oss.sonatype.org/content/repositories/snapshots/. You can include the B parser in a gradle build script like this:
 
 <pre>
-def parser_version = '2.9.0' // development version: 2.9.1-SNAPSHOT
+def parser_version = '2.9.9' // development version: 2.9.10-SNAPSHOT
 dependencies {
-	compile group: "de.hhu.stups", name: "bparser", version: parser_version 
-	compile group: "de.hhu.stups", name: "ltlparser", version: parser_version// optional 
-	compile group: "de.hhu.stups", name: "parserbase", version: parser_version 
-	compile group: "de.hhu.stups", name: "prologlib", version: parser_version 
+	compile group: "de.hhu.stups", name: "bparser", version: parser_version
+	compile group: "de.hhu.stups", name: "ltlparser", version: parser_version// optional
+	compile group: "de.hhu.stups", name: "parserbase", version: parser_version
+	compile group: "de.hhu.stups", name: "prologlib", version: parser_version
 }
 </pre>
 
@@ -23,20 +22,20 @@ The repository contains some additional parsers:
 * answerparser - Parses the answers sent by probcli
 * bparser	- Parser for classical B
 * cliparser	- Commandline interface for the classical B + LTL parser
-* eventbstruct	- Parser for the Camille structural syntax 
+* eventbstruct	- Parser for the Camille structural syntax
 * ltlparser	- Parser for LTL and CTL
-* parserbase	- Interface classes for the Parsers 
+* parserbase	- Interface classes for the Parsers
 * prologlib - Library to produce valid Prolog terms  
 * theorymapping	- Parser for Theory mapping files (translation of EventB operators to Prolog predicates)
-* translator - Translates B values into Java objects. 
-* unicode - Conversion of EventB Unicode Strings to ASCII and vice versa 
+* translator - Translates B values into Java objects.
+* unicode - Conversion of EventB Unicode Strings to ASCII and vice versa
 
 ## Building
-Run the 'deploy' target with gradle. 
+Run the 'deploy' target with gradle.
 
-On windows you need to install the program 'patch.exe'. 
+On windows you need to install the program 'patch.exe'.
 
-The artifacts are copied to the build folder. 
+The artifacts are copied to the build folder.
 
 # Bugs
 Please report bugs and feature requests at https://probjira.atlassian.net
@@ -45,11 +44,11 @@ Please report bugs and feature requests at https://probjira.atlassian.net
 ## Content
 
 - bparser - parser for classical B (more information in http://www.stups.uni-duesseldorf.de/w/An_Object_Oriented_Parser_For_B_Specifications)
-- prologlib - library to construct and manipulate well-formed prolog terms 
-- parserbase - library for uniform access to the formal language parsers (e.g. to embed a language into ltl) 
+- prologlib - library to construct and manipulate well-formed prolog terms
+- parserbase - library for uniform access to the formal language parsers (e.g. to embed a language into ltl)
 - ltlparser - parser for LTL formulas - the parser delegates formulas in { } to a formalism specific parser (e.g. to the classical B parser).
               Also contains a parser for CTL
-- answerparser - parser to read answers from the ProB prolog core 
+- answerparser - parser to read answers from the ProB prolog core
 - unicode - lexer that transforms Event-B expressions and predicates from ASCII to Unicode syntax and vice3 versa (note: this is not extensible!)
 - cliparser - glue code for embedding the parser in the prolog core (deprecated!)
 - translator - translator for B expressions to java
@@ -58,9 +57,9 @@ Please report bugs and feature requests at https://probjira.atlassian.net
 The libraries contain contributions from (in alphabetical order)
 Jens Bendisposto, Marc Büngener, Fabian Fritz, Dominik Hansen, Sebastian Krings, Michael Leuschel, Daniel Plagge, David Schneider
 
-## Licence 
+## Licence
 
-The ProB Parser Library source code is distributed under the Eclipse Public License - v 1.0 (see epl-v10.html) 
+The ProB Parser Library source code is distributed under the Eclipse Public License - v 1.0 (see epl-v10.html)
 
 The Parser Library comes with ABSOLUTELY NO WARRANTY OF ANY KIND !
 This software is distributed in the hope that it will be useful

answerparser/build.gradle

@@ -55,7 +55,7 @@ jacocoTestReport {
   reports {
       xml.enabled false
       csv.enabled false
-      html.destination "${buildDir}/jacocoHtml"
+      html.destination file("${buildDir}/jacocoHtml")
   }
 
     afterEvaluate {

bparser/build.gradle

@@ -37,7 +37,7 @@ task createBuildConstants  {
     def buildconstants_class = """
 version=${project.version}
 git=${getCheckedOutGitCommitHash()}"""
-    File f = file("src/main/resources/build.properties")
+    File f = file("src/main/resources/bparser-build.properties")
     f.delete()
     f.getParentFile().mkdirs()
     f <<  buildconstants_class
@@ -97,7 +97,7 @@ jacocoTestReport {
   reports {
       xml.enabled false
       csv.enabled false
-      html.destination "${buildDir}/jacocoHtml"
+      html.destination file("${buildDir}/jacocoHtml")
   }
 
     afterEvaluate {

bparser/src/main/java/de/be4/classicalb/core/parser/BLexer.java

@@ -17,14 +17,14 @@ public class BLexer extends Lexer {
 	// PUSHBACK_BUFFER_SIZE should be more than the max length of any keyword
 	public static final int PUSHBACK_BUFFER_SIZE = 99;
 
-	private static Map<Class<? extends Token>, Map<Class<? extends Token>, String>> invalid = new HashMap<Class<? extends Token>, Map<Class<? extends Token>, String>>();
+	private static Map<Class<? extends Token>, Map<Class<? extends Token>, String>> invalid = new HashMap<>();
 	private static Set<Class<? extends Token>> clauseTokenClasses = new HashSet<>();
 	private static Map<Character, Character> stringReplacements = new HashMap<>();
 
 	private static void addInvalid(Class<? extends Token> f, Class<? extends Token> s, String message) {
 		Map<Class<? extends Token>, String> secs = invalid.get(f);
 		if (secs == null)
-			secs = new HashMap<Class<? extends Token>, String>();
+			secs = new HashMap<>();
 		secs.put(s, message);
 		invalid.put(f, secs);
 	}
@@ -44,6 +44,9 @@ private static void addInvalid(Class<? extends Token> f, Class<? extends Token>
 		addInvalid(TDoubleVerticalBar.class, TDoubleVerticalBar.class,
 				"|| || is not allowed (probably one || too many).");
 		addInvalid(TSetSubtraction.class, TEqual.class, "You need to use /= for inequality and not \\=.");
+		addInvalid(TSetSubtraction.class, TElementOf.class, "You need to use /: for not membership and not \\:.");
+		addInvalid(TSetSubtraction.class, TInclusion.class, "You need to use /<: for not subset and not \\<:.");
+		addInvalid(TSetSubtraction.class, TStrictInclusion.class, "You need to use /<<: for not strict subset and not \\<<:.");
 
 		clauseTokenClasses.add(TConstants.class);
 		clauseTokenClasses.add(TAssertions.class);
@@ -76,17 +79,9 @@ private static void addInvalid(Class<? extends Token> f, Class<? extends Token>
 
 	private final DefinitionTypes definitions;
 
-	// private final List<IToken> dotList = new ArrayList<IToken>();
-
 	public BLexer(final PushbackReader in, final DefinitionTypes definitions, final int tokenCountPrediction) {
 		super(in);
 		this.definitions = definitions;
-
-		// if (tokenCountPrediction > 10) {
-		// tokenList = new ArrayList<Token>(tokenCountPrediction);
-		// } else {
-		// tokenList = new ArrayList<Token>();
-		// }
 	}
 
 	public BLexer(final PushbackReader in, final DefinitionTypes definitions) {
@@ -129,8 +124,8 @@ private void checkForInvalidCombinations(Class<? extends Token> lastTokenClass,
 	}
 
 	private void applyGrammarExtension() {
-		if (parseOptions != null && this.parseOptions.grammar.containsAlternativeDefinitionForToken(token)) {
-			token = this.parseOptions.grammar.createNewToken(token);
+		if (parseOptions != null && this.parseOptions.getGrammar().containsAlternativeDefinitionForToken(token)) {
+			token = this.parseOptions.getGrammar().createNewToken(token);
 		}
 	}
 
@@ -154,36 +149,7 @@ protected void filter() throws LexerException, IOException {
 		}
 
 		if (token instanceof TStringLiteral || token instanceof TMultilineStringContent) {
-			// google for howto-unescape-a-java-string-literal-in-java
-			// quickfix: we do nothing just strip off the "
-			String literal = token.getText();
-
-			/*
-			 * Note, the text of a TMultilineString token does not start with
-			 * ''' because the ''' are contained in the TMultilineStringStartEnd
-			 * token
-			 */
-			if (literal.startsWith("\"")) {
-				/// "foo"
-				literal = literal.substring(1, literal.length() - 1);
-			}
-
-			boolean backslashFound = false;
-			StringBuffer buffer = new StringBuffer();
-			for (int i = 0; i < literal.length(); i++) {
-				char c = literal.charAt(i);
-				if (backslashFound && stringReplacements.containsKey(c)) {
-					buffer.setLength(buffer.length() - 1);
-					buffer.append(stringReplacements.get(c));
-					backslashFound = false;
-					continue;
-				}
-				if (c == '\\') {
-					backslashFound = true;
-				}
-				buffer.append(c);
-			}
-			token.setText(buffer.toString());
+			handleStringToken(token);
 		}
 
 		if (token instanceof THexLiteral) {
@@ -201,6 +167,38 @@ protected void filter() throws LexerException, IOException {
 		}
 	}
 
+	private void handleStringToken(Token token) {
+		// google for howto-unescape-a-java-string-literal-in-java
+		// quickfix: we do nothing just strip off the "
+		String literal = token.getText();
+
+		/*
+		 * Note, the text of a TMultilineString token does not start with '''
+		 * because the ''' are contained in the TMultilineStringStartEnd token
+		 */
+		if (literal.startsWith("\"")) {
+			/// "foo"
+			literal = literal.substring(1, literal.length() - 1);
+		}
+
+		boolean backslashFound = false;
+		StringBuilder sb = new StringBuilder();
+		for (int i = 0; i < literal.length(); i++) {
+			char c = literal.charAt(i);
+			if (backslashFound && stringReplacements.containsKey(c)) {
+				sb.setLength(sb.length() - 1);
+				sb.append(stringReplacements.get(c));
+				backslashFound = false;
+				continue;
+			}
+			if (c == '\\') {
+				backslashFound = true;
+			}
+			sb.append(c);
+		}
+		token.setText(sb.toString());
+	}
+
 	private void replaceDefTokens() {
 		if (token instanceof TIdentifierLiteral) {
 			final Definitions.Type type = definitions.getType(token.getText());
@@ -250,8 +248,7 @@ private void collectComment() throws LexerException, IOException {
 			// final int line = token.getLine() - 1;
 			// final int pos = token.getPos() - 1;
 			final String text = token.getText();
-			throw new BLexerException(comment, "Comment not closed.", text.toString(), comment.getLine(),
-					comment.getPos());
+			throw new BLexerException(comment, "Comment not closed.", text, comment.getLine(), comment.getPos());
 		}
 
 		// starting a new comment