04.07., 9:00 - 11:00: Due to updates GitLab will be unavailable for some minutes between 09:00 and 11:00.

Commit 27517e53 authored by Salomon Sickert's avatar Salomon Sickert

Remove TLSF support.

parent 9c953acb
# 2019.06 (unreleased)
Translations:
Modules:
* Implemented all LICS'18 translations for LTL fragments. Including a symbolic
successor / edge computation. The translations can be found in the canonical
package and are exposed via `ltl2da` and `ltl2na`.
* Removed TLSF support. Ensuring the correct implementation of the TLSF
specification posed a too large maintenance burden. Users of the TLSF format
can use Syfco (https://github.com/reactive-systems/syfco) to translate it to
a basic LTL formula.
API:
* Overhaul of the symbolic successor computation
......
......@@ -34,8 +34,8 @@ SRELEASE : 'M';
// MISC
LPAREN : '(';
RPAREN : ')';
LDQUOTE : '"' -> mode(DOUBLE_QUOTED);
LSQUOTE : '\'' -> mode(SINGLE_QUOTED);
LDQUOTE : '"' -> mode(DOUBLE_QUOTED);
LSQUOTE : '\'' -> mode(SINGLE_QUOTED);
LCPAREN : '{' -> mode(FREQUENCY_SPEC);
......
lexer grammar TLSFLexer;
@lexer::header {
package owl.grammar;
}
fragment
LCPAR : '{';
fragment
RCPAR : '}';
fragment
SEMIC : ';';
fragment
WS : [ \t\r\f\n]+;
fragment
LINE_COMMENT : '//' ~[\r\n]*;
SKIP_DEF : (WS | LINE_COMMENT) -> skip;
INFO : 'INFO' -> pushMode(MODE_INFO);
MAIN : 'MAIN' -> pushMode(MODE_MAIN);
mode MODE_INFO;
SKIP_INFO : (WS | LINE_COMMENT) -> skip;
INFO_START : '{';
TITLE : 'TITLE:';
DESCRIPTION : 'DESCRIPTION:';
SEMANTICS : 'SEMANTICS:';
TARGET : 'TARGET:';
TAGS : 'TAGS: ';
INFO_STRING : '"' (~'"'*) '"';
MEALY : 'Mealy';
MOORE : 'Moore';
MEALY_STRICT : 'Mealy,Strict';
MOORE_STRICT : 'Moore,Strict';
INFO_END : RCPAR -> popMode;
mode MODE_MAIN;
MAIN_START : LCPAR;
SKIP_MAIN : (WS | LINE_COMMENT) -> skip;
INPUTS : 'INPUTS' -> pushMode(MODE_IO);
OUTPUTS : 'OUTPUTS' -> pushMode(MODE_IO);
INITIALLY : 'INITIALLY' -> pushMode(MODE_SPEC);
PRESET : 'PRESET' -> pushMode(MODE_SPEC);
REQUIRE : 'REQUIRE' -> pushMode(MODE_SPEC);
ASSERT : ('ASSERT' | 'INVARIANTS') -> pushMode(MODE_SPEC);
ASSUME : ('ASSUME' | 'ASSUMPTIONS') -> pushMode(MODE_SPEC);
GUARANTEE : ('GUARANTEE' | 'GUARANTEES') -> pushMode(MODE_SPEC);
MAIN_END : RCPAR -> popMode;
mode MODE_IO;
SKIP_IO : (WS | LINE_COMMENT) -> skip;
IO_START : LCPAR;
VAR_ID : [a-zA-Z_@][a-zA-Z0-9_@']*;
ID_SEP : SEMIC;
IO_END : RCPAR -> popMode;
mode MODE_SPEC;
fragment
LTL_TOKEN : [a-zA-Z0-9\-_&|<>!()];
SPEC_START : LCPAR;
SPEC_END : RCPAR -> popMode;
SPEC_LTL : LTL_TOKEN (LTL_TOKEN | WS)* SEMIC;
SKIP_SPEC : (WS | LINE_COMMENT) -> skip;
\ No newline at end of file
parser grammar TLSFParser;
options {
language = Java;
tokenVocab = TLSFLexer;
}
@header {
package owl.grammar;
}
tlsf :
INFO INFO_START
TITLE title=INFO_STRING
DESCRIPTION description=INFO_STRING
SEMANTICS semantics
TARGET target
INFO_END
MAIN MAIN_START
input
output
specification+
MAIN_END
EOF
;
semantics
: MEALY | MOORE | MEALY_STRICT | MOORE_STRICT
;
target
: MEALY | MOORE
;
input
: INPUTS IO_START (in=VAR_ID ID_SEP)* IO_END
;
output
: OUTPUTS IO_START (out=VAR_ID ID_SEP)* IO_END
;
specification
: (INITIALLY | PRESET | REQUIRE | ASSERT | ASSUME | GUARANTEE)
SPEC_START formula=SPEC_LTL+ SPEC_END
;
......@@ -39,7 +39,6 @@ namespace owl {
bind_static(MOperator, "owl/ltl/MOperator", of, binarySignature);
bind_static_method(env, "owl/ltl/parser/LtlParser", "syntax", "(Ljava/lang/String;Ljava/util/List;)Lowl/ltl/Formula;", ltlParser, ltlParseID);
bind_static_method(env, "owl/ltl/parser/TlsfParser", "parse", "(Ljava/lang/String;)Lowl/ltl/tlsf/Tlsf;", tlsfParser, tlsfParseID);
}
FormulaFactory::~FormulaFactory() {
......@@ -124,18 +123,4 @@ namespace owl {
deref(env, string, mapping);
return formula;
}
Formula FormulaFactory::parseTlsf(const std::string &tlsf_string, std::vector<std::string> &apMapping,
int &numberOfInputVariables) {
jstring string = copy_to_java(env, tlsf_string);
auto tlsf = call_static_method<jobject, jstring>(env, tlsfParser, tlsfParseID, string);
auto labelled_formula = call_method<jobject>(env, tlsf, "toFormula", "()Lowl/ltl/LabelledFormula;");
auto formula = get_object_field<jobject>(env, labelled_formula, "formula", "Lowl/ltl/Formula;");
apMapping = copy_from_java(env, get_object_field<jobject>(env, labelled_formula, "variables", "Lcom/google/common/collect/ImmutableList;"));
numberOfInputVariables = call_int_method<>(env, tlsf, "numberOfInputs", "()I");
deref(env, tlsf, labelled_formula);
return copy_from_java(env, formula);
}
}
\ No newline at end of file
......@@ -46,9 +46,7 @@ namespace owl {
jclass classes[MOperator + 1];
jmethodID methodIDs[MOperator + 1];
jclass ltlParser;
jclass tlsfParser;
jmethodID ltlParseID;
jmethodID tlsfParseID;
void bind_static(int index, const char *className, const char *methodName, const char *signature);
......@@ -77,7 +75,6 @@ namespace owl {
Formula createNegation(const Formula& formula);
Formula createBiimplication(const Formula &left, const Formula &right);
Formula parse(const std::string& formula, const std::vector<std::string>& apMapping);
Formula parseTlsf(const std::string& tlsf, std::vector<std::string>& apMapping, int &numberOfInputVariables);
template<typename... Args>
Formula createConjunction(const Formula& left, const Formula& right, Args... args) {
......
/*
* Copyright (C) 2016 - 2018 (See AUTHORS)
*
* This file is part of Owl.
*
* This program is free software: you can redistribute it and/or modify
* it under the terms of the GNU General Public License as published by
* the Free Software Foundation, either version 3 of the License, or
* (at your option) any later version.
*
* This program is distributed in the hope that it will be useful,
* but WITHOUT ANY WARRANTY; without even the implied warranty of
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
* GNU General Public License for more details.
*
* You should have received a copy of the GNU General Public License
* along with this program. If not, see <http://www.gnu.org/licenses/>.
*/
package owl.ltl.parser;
import java.io.IOException;
import java.io.InputStream;
import java.io.Reader;
import java.nio.charset.Charset;
import java.util.ArrayList;
import java.util.BitSet;
import java.util.List;
import org.antlr.v4.runtime.BailErrorStrategy;
import org.antlr.v4.runtime.CharStream;
import org.antlr.v4.runtime.CharStreams;
import org.antlr.v4.runtime.CommonTokenStream;
import org.antlr.v4.runtime.ConsoleErrorListener;
import org.antlr.v4.runtime.misc.ParseCancellationException;
import org.antlr.v4.runtime.tree.ParseTree;
import org.antlr.v4.runtime.tree.TerminalNode;
import owl.grammar.TLSFLexer;
import owl.grammar.TLSFParser;
import owl.grammar.TLSFParser.SemanticsContext;
import owl.grammar.TLSFParser.SpecificationContext;
import owl.grammar.TLSFParser.TargetContext;
import owl.grammar.TLSFParser.TlsfContext;
import owl.ltl.Conjunction;
import owl.ltl.Formula;
import owl.ltl.tlsf.ImmutableTlsf;
import owl.ltl.tlsf.ImmutableTlsf.Builder;
import owl.ltl.tlsf.Tlsf;
import owl.ltl.tlsf.Tlsf.Semantics;
import owl.util.annotation.CEntryPoint;
public final class TlsfParser {
private TlsfParser() {}
@CEntryPoint
public static Tlsf parse(String input) {
return parse(CharStreams.fromString(input));
}
private static Tlsf parse(CharStream stream) {
TLSFLexer lexer = new TLSFLexer(stream);
lexer.removeErrorListener(ConsoleErrorListener.INSTANCE);
CommonTokenStream tokens = new CommonTokenStream(lexer);
TLSFParser parser = new TLSFParser(tokens);
parser.setErrorHandler(new BailErrorStrategy());
TlsfContext tree = parser.tlsf();
Builder builder = ImmutableTlsf.builder();
// Info
builder.title(tree.title.getText());
builder.description(tree.description.getText());
SemanticsContext semantics = tree.semantics();
if (semantics.MEALY() != null) {
builder.semantics(Semantics.MEALY);
} else if (semantics.MOORE() != null) {
builder.semantics(Semantics.MOORE);
} else if (semantics.MEALY_STRICT() != null) {
builder.semantics(Semantics.MEALY_STRICT);
} else if (semantics.MOORE_STRICT() != null) {
builder.semantics(Semantics.MOORE_STRICT);
} else {
throw new ParseCancellationException("Unknown semantics");
}
TargetContext target = tree.target();
if (target.MEALY() != null) {
builder.target(Semantics.MEALY);
} else if (target.MOORE() != null) {
builder.target(Semantics.MOORE);
} else {
throw new ParseCancellationException("Unknown semantics");
}
// Input / output
List<String> variables = new ArrayList<>();
List<String> lowercaseVariables = new ArrayList<>();
BitSet inputs = new BitSet();
for (TerminalNode variableNode : tree.input().VAR_ID()) {
String variableName = variableNode.getText();
if (lowercaseVariables.contains(variableName.toLowerCase())) {
throw new ParseCancellationException("Duplicate variable definition: " + variableName);
}
inputs.set(variables.size());
variables.add(variableName);
lowercaseVariables.add(variableName.toLowerCase());
}
BitSet outputs = new BitSet();
for (TerminalNode variableNode : tree.output().VAR_ID()) {
String variableName = variableNode.getText();
if (lowercaseVariables.contains(variableName.toLowerCase())) {
throw new ParseCancellationException("Duplicate variable definition: " + variableName);
}
outputs.set(variables.size());
variables.add(variableName);
lowercaseVariables.add(variableName.toLowerCase());
}
builder.inputs(inputs);
builder.outputs(outputs);
builder.variables(List.copyOf(variables));
// Specifications
List<Formula> initial = new ArrayList<>();
List<Formula> preset = new ArrayList<>();
List<Formula> require = new ArrayList<>();
List<Formula> assert_ = new ArrayList<>();
List<Formula> assume = new ArrayList<>();
List<Formula> guarantee = new ArrayList<>();
for (SpecificationContext specificationContext : tree.specification()) {
int children = specificationContext.children.size();
for (ParseTree child : specificationContext.children.subList(2, children - 1)) {
String formulaString = child.getText();
assert !formulaString.isEmpty();
// Strip trailing ;
String sanitizedFormula = formulaString.substring(0, formulaString.length() - 1).trim();
// Map arbitrary variable names to lowercase variables
for (int i = 0; i < variables.size(); i++) {
String variableName = variables.get(i);
for (int j = 0; j < i; j++) {
variableName = variableName.replace(variables.get(j), lowercaseVariables.get(j));
}
sanitizedFormula = sanitizedFormula.replace(variableName, lowercaseVariables.get(i));
}
Formula formula = LtlParser.syntax(sanitizedFormula, lowercaseVariables);
if (specificationContext.INITIALLY() != null) {
initial.add(formula);
} else if (specificationContext.PRESET() != null) {
preset.add(formula);
} else if (specificationContext.REQUIRE() != null) {
require.add(formula);
} else if (specificationContext.ASSERT() != null) {
assert_.add(formula);
} else if (specificationContext.ASSUME() != null) {
assume.add(formula);
} else if (specificationContext.GUARANTEE() != null) {
guarantee.add(formula);
} else {
throw new ParseCancellationException("Unknown specification type");
}
}
}
builder.initially(Conjunction.of(initial));
builder.preset(Conjunction.of(preset));
builder.require(Conjunction.of(require));
builder.assume(Conjunction.of(assume));
builder.assert_(List.copyOf(assert_));
builder.guarantee(List.copyOf(guarantee));
return builder.build();
}
public static Tlsf parse(InputStream input, Charset charset) throws IOException {
return parse(CharStreams.fromStream(input, charset));
}
public static Tlsf parse(Reader input) throws IOException {
return parse(CharStreams.fromReader(input));
}
}
/*
* Copyright (C) 2016 - 2018 (See AUTHORS)
*
* This file is part of Owl.
*
* This program is free software: you can redistribute it and/or modify
* it under the terms of the GNU General Public License as published by
* the Free Software Foundation, either version 3 of the License, or
* (at your option) any later version.
*
* This program is distributed in the hope that it will be useful,
* but WITHOUT ANY WARRANTY; without even the implied warranty of
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
* GNU General Public License for more details.
*
* You should have received a copy of the GNU General Public License
* along with this program. If not, see <http://www.gnu.org/licenses/>.
*/
package owl.ltl.tlsf;
import com.google.common.base.Preconditions;
import java.util.ArrayList;
import java.util.BitSet;
import java.util.List;
import org.immutables.value.Value;
import owl.ltl.BooleanConstant;
import owl.ltl.Conjunction;
import owl.ltl.Disjunction;
import owl.ltl.FOperator;
import owl.ltl.Formula;
import owl.ltl.GOperator;
import owl.ltl.LabelledFormula;
import owl.ltl.Literal;
import owl.ltl.SyntacticFragment;
import owl.ltl.WOperator;
import owl.ltl.XOperator;
import owl.ltl.visitors.Converter;
@SuppressWarnings("ReferenceEquality")
@Value.Immutable
public abstract class Tlsf {
@Value.Default
@SuppressWarnings("PMD.MethodNamingConventions")
public List<Formula> assert_() {
return List.of();
}
@Value.Default
public Formula assume() {
return BooleanConstant.TRUE;
}
private Formula convert(Formula formula) {
if (semantics().isMealy() && target().isMoore()) {
return formula.accept(new MealyToMooreConverter());
}
if (semantics().isMoore() && target().isMealy()) {
return formula.accept(new MooreToMealyConverter());
}
return formula;
}
public abstract String description();
@Value.Default
public List<Formula> guarantee() {
return List.of();
}
@Value.Default
public Formula initially() {
return BooleanConstant.TRUE;
}
// Main / Body
public abstract BitSet inputs();
public abstract BitSet outputs();
public abstract List<String> variables();
@Value.Default
public Formula preset() {
return BooleanConstant.TRUE;
}
@Value.Default
public Formula require() {
return BooleanConstant.TRUE;
}
public abstract Semantics semantics();
public abstract Semantics target();
// Info Header
public abstract String title();
@Value.Derived
public int numberOfInputs() {
return inputs().cardinality();
}
@Value.Derived
public LabelledFormula toFormula() {
return toFormula(Conjunction.of(assert_()), Conjunction.of(guarantee()));
}
private LabelledFormula toFormula(Formula assert_, Formula guarantee) {
Formula formula = Disjunction.of(FOperator.of(require().not()), assume().not(),
Conjunction.of(GOperator.of(assert_), guarantee));
if (semantics().isStrict()) {
formula = Conjunction.of(preset(), formula, WOperator.of(assert_, require().not()));
} else {
formula = Conjunction.of(preset(), formula);
}
Formula result = convert(Disjunction.of(initially().not(), formula));
return LabelledFormula.of(result, variables(), inputs());
}
@Value.Derived
public List<LabelledFormula> toAssertGuaranteeConjuncts() {
List<LabelledFormula> conjuncts = new ArrayList<>();
assert_().forEach(x -> conjuncts.add(toFormula(x, BooleanConstant.TRUE)));
guarantee().forEach(x -> conjuncts.add(toFormula(BooleanConstant.TRUE, x)));
return conjuncts;
}
public enum Semantics {
MEALY, MEALY_STRICT, MOORE, MOORE_STRICT;
public boolean isMealy() {
return this == Semantics.MEALY || this == Semantics.MEALY_STRICT;
}
public boolean isMoore() {
return !isMealy();
}
public boolean isStrict() {
switch (this) {
case MEALY_STRICT:
case MOORE_STRICT:
return true;
default:
return false;
}
}
}
@Value.Check
protected void check() {
boolean outputs = false;
for (int i = 0; i < variables().size(); i++) {
Preconditions.checkState(inputs().get(i) ^ outputs().get(i),
"'inputs' and 'outputs' must use distinct ids.");
if (outputs().get(i)) {
outputs = true;
}
if (outputs) {
Preconditions.checkState(!inputs().get(i), "'inputs' should use lower numbers.");
}
}
}
private final class MealyToMooreConverter extends Converter {
private MealyToMooreConverter() {
super(SyntacticFragment.ALL);
}
@Override
public Formula visit(Literal literal) {
if (outputs().get(literal.getAtom())) {
return XOperator.of(literal);
}
return literal;
}
}
private final class MooreToMealyConverter extends Converter {
private MooreToMealyConverter() {
super(SyntacticFragment.ALL);
}
@Override
public Formula visit(Literal literal) {
if (inputs().get(literal.getAtom())) {
return XOperator.of(literal);
}
return literal;
}
}
}
/*
* Copyright (C) 2016 - 2018 (See AUTHORS)
*
* This file is part of Owl.
*
* This program is free software: you can redistribute it and/or modify
* it under the terms of the GNU General Public License as published by
* the Free Software Foundation, either version 3 of the License, or
* (at your option) any later version.
*
* This program is distributed in the hope that it will be useful,
* but WITHOUT ANY WARRANTY; without even the implied warranty of
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
* GNU General Public License for more details.
*
* You should have received a copy of the GNU General Public License
* along with this program. If not, see <http://www.gnu.org/licenses/>.
*/
@EverythingIsNonnullByDefault
package owl.ltl.tlsf;
import owl.util.annotation.EverythingIsNonnullByDefault;
......@@ -31,8 +31,6 @@ import org.antlr.v4.runtime.misc.ParseCancellationException;
import owl.automaton.AutomatonReader;
import owl.ltl.LabelledFormula;
import owl.ltl.parser.LtlParser;
import owl.ltl.parser.TlsfParser;
import owl.ltl.tlsf.Tlsf;
import owl.run.PipelineException;
import owl.run.modules.OwlModuleParser.ReaderParser;
......@@ -53,17 +51,6 @@ public final class InputReaders {
+ "acceptance if necessary")
.parser(settings -> HOA).build();
public static final InputReader TLSF = (reader, env, callback) -> {
Tlsf tlsf = TlsfParser.parse(reader);
callback.accept(tlsf.toFormula());
};
public static final ReaderParser TLSF_CLI = ImmutableReaderParser.builder()
.key("tlsf")
.description("Parses a single TLSF instance and converts it to an LTL formula")
.parser(settings -> TLSF).build();
public static final InputReader LTL = (reader, env, callback) ->
CharStreams.readLines(reader, new LineProcessor<Void>() {
@Override
......
......@@ -82,7 +82,7 @@ public class OwlModuleRegistry {
DEFAULT_REGISTRY = new OwlModuleRegistry();
// I/O
DEFAULT_REGISTRY.register(InputReaders.LTL_CLI, InputReaders.HOA_CLI, InputReaders.TLSF_CLI,
DEFAULT_REGISTRY.register(InputReaders.LTL_CLI, InputReaders.HOA_CLI,
OutputWriters.TO_STRING_CLI, OutputWriters.AUTOMATON_STATS_CLI, OutputWriters.NULL_CLI,
OutputWriters.HOA_CLI, GameUtil.PG_SOLVER_CLI, RobustLtlInputReader.INSTANCE);
......
/*
* Copyright (C) 2016 - 2018 (See AUTHORS)
*
* This file is part of Owl.
*
* This program is free software: you can redistribute it and/or modify
* it under the terms of the GNU General Public License as published by
* the Free Software Foundation, either version 3 of the License, or
* (at your option) any later version.
*
* This program is distributed in the hope that it will be useful,
* but WITHOUT ANY WARRANTY; without even the implied warranty of
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
* GNU General Public License for more details.
*
* You should have received a copy of the GNU General Public License
* along with this program. If not, see <http://www.gnu.org/licenses/>.
*/
package owl.ltl.parser;
import static org.junit.jupiter.api.Assertions.assertEquals;
import static org.junit.jupiter.api.Assertions.assertThrows;
import java.util.List;
import java.util.Set;
import org.antlr.v4.runtime.misc.ParseCancellationException;
import org.junit.jupiter.api.Disabled;
import org.junit.jupiter.api.Test;
import owl.ltl.Formula;
import owl.ltl.LabelledFormula;
import owl.ltl.tlsf.Tlsf;
class TlsfParserTest {
private static final String TLSF1 = "INFO {\n"
+ " TITLE: \"LTL -> DBA - Example 12\"\n"
+ " DESCRIPTION: \"One of the Acacia+ example files\"\n"
+ " SEMANTICS: Moore\n"
+ " TARGET: Mealy\n"
+ "}\n"
+ "// TEST COMMENT\n"
+ "MAIN {\n"
+ "// TEST COMMENT\n"
+ " INPUTS {\n"
+ " p;\n"
+ " q;\n"
+ " }\n"
+ "// TEST COMMENT\n"
+ " OUTPUTS {\n"
+ " acc;\n"
+ " }\n"
+ "// TEST COMMENT\n"
+ " GUARANTEE {\n"
+ "// TEST COMMENT\n"
+ " (G p -> F q) && (G !p <-> F !q)\n"
+ " && G F acc;\n"
+ " }\n"