diff --git a/README.md b/README.md index 9479424..73e4713 100644 --- a/README.md +++ b/README.md @@ -1,23 +1,57 @@ -Simple Java CTL Parser. +Simple parser, normalizer and optimizer for CTL temporal logic formulas written in Kotlin. -###API +###Features + + - File includes + - References + - Full range of boolean and temporal operators + - Simple formula optimizer + - Normalizer into until normal form (EU, AU, EX, &&, ||, !) + +###Syntax + +Each CTL file contains zero or more include statements and zero or more assignment statements. Each statement is separated by a new line. Multi-line formulas are not supported, use references instead. + +Input statement has the following form: ```#include "string"``` where ```string``` is a path to a file (can be absolute or relative) that should be included. For now, escaping quotation marks is not allowed, so make sure your path does not contain any. Each file is included at most once, so you don't have to worry about multiple includes. + +Assignment statement has the form of ```identifier = formula```. ```identifier``` consists of numbers and upper/lowercase characters (has to start with a character). Formula can be + - identifier (reference to formula defined elsewhere) + - boolean constant (True/False/tt/ff) + - float proposition: ```id operator number``` where ```id``` is a name of the model property and operator is one of <, >, <=, >=, !=, ==. Numbers can't use scientific notation (1e10). + - direction proposition: ```id:direction facet```(space is not mandatory) where ```id``` is a name of the model property, direction is either in or our and facet can be positive(+) or negative(-). Example: ```val:in+``` + - another formula in parentheses + - Formula with unary operator applied. Unary operators: !, EX, AX, EF, AF, EG, AG + - Two formulas with binary operator applied (infix notation: ```f1 op f2```). Binary operators: &&, ||, =>, <=>, EU, AU + +Forward declaration, even accross files is supported, so that you can define your formulas in whatever order you choose. For obvious reasons, cyclic references are not allowed. + +Operator priority: In general, unary operators have higher priority than binary operators. Binary operators have following priority: && >> || >> => >> <=> >> EU >> AU -- FormulaParser - Parses a file or string into object representing a formula. -- FormulaNormalizer - Normalizes given formula to the form that can be used for model checking. +Also note that =>, EU and AU are right associative, so that ```a EU b EU c``` is parsed as ```a EU (b EU c)```, as expected. + +Example of usage: -###Input Syntax ``` -#define propositionName variableName <= floatValue -#property A ((True => AF proposotion) U EX False) + f = (AG (p1 EU a)) || (EG (p2 AU b)) + p1 = val > 3.14 + p2 = val2 < -44 + p2 = var:in+ && var:in- + a = EF (p1 && p2) + b = AF foo + #include "other/foo.ctl" ``` -- operators (temporal and boolean) should be separated by whitespace (wrong: AFEX, UEX, !AX) -- binary operators have to be enclosed in brackets: (f && g), (f => g), E(f U g), A(f U g) -- all standard boolean and CTL operators are supported except reversed implication (<=): -!, &&, ||, =>, <=>, AX, EX, AF, EF, AG, EG, AU, EU -- all standard float comparison operators are supported: <,>,<=,>=,==,!= -- boolean literals are accepted as proposition names: True, False -- variable and proposition names cannot contain digits +###Normalization and Optimization + +Currently you can transform formulas into normal form that supports only operators EX, EU, AU, &&, ||, !. Alternatively, you can provide our own normalization function map that will implement your own normal form (or modify current one). + +You can also automatically perform some simple formula optimizations (proposition negation, double negation removal, boolean propagation and some simplifications). Note that these optimizations expect the formula to be in until normal form. (Other formulas are also supported, but possible optimizations are limited) + +###API + +There are currently three main classes you can use ```Parser```, ```Normalizer```, ```Optimizer```. ```Parser``` provides methods that will parse a file, string or a single formula string (you don't have to perform an assignment). These methods automatically resolve all includes and references. + +For more complex usage example, see [IntegrationTest]{https://github.com/sybila/CTL-Parser/blob/new_parser/src/test/kotlin/cz/muni/fi/ctl/IntegrationTest.kt} ###Building and using diff --git a/build.gradle b/build.gradle index 4a65eec..a1686fd 100644 --- a/build.gradle +++ b/build.gradle @@ -1,22 +1,25 @@ //include antlr plugin buildscript { + ext.kotlin_version = '0.13.1513' repositories { maven { name 'JFrog OSS snapshot repo' url 'https://oss.jfrog.org/oss-snapshot-local/' } jcenter() + mavenCentral() } dependencies { classpath 'me.champeau.gradle:antlr4-gradle-plugin:0.1' + classpath "org.jetbrains.kotlin:kotlin-gradle-plugin:$kotlin_version" } } apply plugin: 'java' +apply plugin: 'kotlin' apply plugin: 'me.champeau.gradle.antlr4' -sourceCompatibility = 1.7 version = '1.0' //antlr config @@ -24,14 +27,14 @@ antlr4 { extraArgs=['-package', 'cz.muni.fi.ctl.antlr'] output=new File('src/main/gen/cz/muni/fi/ctl/antlr') visitor=false - listener=false + listener=true } // make the Java compile task depend on the antlr4 task compileJava.dependsOn antlr4 // add the generated source files to the list of java sources -sourceSets.main.java.srcDirs += antlr4.output +sourceSets.main.java.srcDirs += new File('src/main/gen') // add antlr4 to classpath configurations { @@ -45,6 +48,7 @@ repositories { dependencies { testCompile group: 'junit', name: 'junit', version: '4.11' compile 'com.intellij:annotations:5.1' + compile "org.jetbrains.kotlin:kotlin-stdlib:$kotlin_version" } //create a single Jar with all dependencies @@ -57,3 +61,7 @@ task fullJar(type: Jar) { from { configurations.compile.collect { it.isDirectory() ? it : zipTree(it) } } with jar } +sourceSets { + main.java.srcDirs += 'src/main/kotlin' + test.java.srcDirs += 'src/test/kotlin' +} diff --git a/src/main/antlr4/CTL.g4 b/src/main/antlr4/CTL.g4 index 40a19ba..3890b3d 100644 --- a/src/main/antlr4/CTL.g4 +++ b/src/main/antlr4/CTL.g4 @@ -1,129 +1,82 @@ -/* Grammar for CTL parser */ grammar CTL; -@header { -import cz.muni.fi.ctl.formula.Formula; -import cz.muni.fi.ctl.formula.FormulaImpl; -import cz.muni.fi.ctl.formula.operator.Operator; -import cz.muni.fi.ctl.formula.operator.BinaryOperator; -import cz.muni.fi.ctl.formula.operator.UnaryOperator; -import cz.muni.fi.ctl.formula.proposition.Contradiction; -import cz.muni.fi.ctl.formula.proposition.FloatProposition; -import cz.muni.fi.ctl.formula.proposition.Proposition; -import cz.muni.fi.ctl.formula.proposition.Tautology; - -import java.util.HashMap; -import java.util.List; -import java.util.Map; -} - -root locals [ - Map propositions = new HashMap<>(), - Formula result - ] : ctl; - -ctl : - define ctl - | property -; - -define : - DEF - VAR_NAME { String name = $VAR_NAME.text; } - VAR_NAME { String prop = $VAR_NAME.text; } - op_float - FLOAT_VAL - { - if ($root::propositions.containsKey(name)) { - throw new IllegalArgumentException("Redefinition of proposition "+name); - } - $root::propositions.put( name, - new FloatProposition( - Double.parseDouble($FLOAT_VAL.text), - prop, - $op_float.op - ) - ); - } -; - -property : PROP formula { $root::result = $property::formula().processed; }; - -formula returns [ Formula processed ] : - TRUE - { $processed = Tautology.INSTANCE; } - | FALSE - { $processed = Contradiction.INSTANCE; } - | VAR_NAME - { $processed = $root::propositions.get($VAR_NAME.text); - if ($processed == null) throw new IllegalArgumentException("Unknown proposition: "+$VAR_NAME.text); - } - | NEG formula - { $processed = new FormulaImpl(UnaryOperator.NEGATION, $formula.ctx.formula.processed ); } - | B_OPEN formula op_bool formula B_CLOSE - { $processed = new FormulaImpl($op_bool.op, $formula.ctx.formula(0).processed, $formula.ctx.formula(1).processed ); } - | EXISTS B_OPEN formula UNTIL formula B_CLOSE - { $processed = new FormulaImpl(BinaryOperator.EXISTS_UNTIL, $formula.ctx.formula(0).processed, $formula.ctx.formula(1).processed ); } - | ALL B_OPEN formula UNTIL formula B_CLOSE - { $processed = new FormulaImpl(BinaryOperator.ALL_UNTIL, $formula.ctx.formula(0).processed, $formula.ctx.formula(1).processed ); } - | temporal formula - { $processed = new FormulaImpl($temporal.op, $formula.ctx.formula(0).processed ); } +/* Main format structure */ + +root : fullStop? (statement fullStop)*; + +statement : '#include' STRING # include + | VAR_NAME '=' formula # assign + ; + +fullStop : NEWLINE+ | EOF; + +/* Formula and propositions */ + +formula : VAR_NAME #id + | (TRUE | FALSE) #bool + | VAR_NAME ':' (IN | OUT) (PLUS | MINUS) #direction + | VAR_NAME floatOp FLOAT_VAL #proposition + | '(' formula ')' #parenthesis + | unaryOp formula #unary + //we list operators explicitly, becuase writing them as a subrule broke operator priority + | formula CON formula #and + | formula DIS formula #or + | formula IMPL formula #implies + | formula EQIV formula #equal + | formula EU formula #EU + | formula AU formula #AU ; -temporal returns [ Operator op ] : - 'EX' { $op = UnaryOperator.EXISTS_NEXT; } - | 'AX' { $op = UnaryOperator.ALL_NEXT; } - | 'EF' { $op = UnaryOperator.EXISTS_FUTURE; } - | 'AF' { $op = UnaryOperator.ALL_FUTURE; } - | 'EG' { $op = UnaryOperator.EXISTS_GLOBAL; } - | 'AG' { $op = UnaryOperator.ALL_GLOBAL; } - ; - -op_bool returns [ Operator op ] : - AND { $op = BinaryOperator.AND; } - | OR { $op = BinaryOperator.OR; } - | IMPL { $op = BinaryOperator.IMPLICATION; } - | EQIV { $op = BinaryOperator.EQUIVALENCE; } -; - -op_float returns [ FloatProposition.Operator op ] : - EQ { $op = FloatProposition.Operator.EQ; } - | N_EQ { $op = FloatProposition.Operator.NEQ; } - | GT { $op = FloatProposition.Operator.GT; } - | LT { $op = FloatProposition.Operator.LT; } - | GT_EQ { $op = FloatProposition.Operator.GT_EQ; } - | LT_EQ { $op = FloatProposition.Operator.LT_EQ; } -; - -DEF : '#define'; -PROP : '#property'; - -/* Terminals: */ - bool : TRUE | FALSE ; - TRUE : 'True'; - FALSE : 'False'; - /* Boolean Operators */ - NEG : '!'; - AND : '&&'; - OR : '||'; - IMPL : '=>'; - EQIV : '<=>'; - /* Temporal Operators */ - ALL : 'A'; - EXISTS : 'E'; - UNTIL : 'U'; - /* Comparison operators */ - EQ : '=='; - N_EQ : '!='; - GT : '>'; - LT : '<'; - GT_EQ : '>='; - LT_EQ : '<='; - /* Brackets */ - B_OPEN : '('; - B_CLOSE : ')'; - /* Values */ - VAR_NAME : [a-zA-Z]+[a-zA-Z0-9]*; - FLOAT_VAL : [-]?[0-9]*[.]?[0-9]+; - WS : [ \t\n]+ -> skip ; // toss out whitespace \ No newline at end of file +/** Helper/Grouping parser rules **/ + +unaryOp : NEG | EX | EF | EG | AX | AF | AG; +floatOp : EQ | NEQ | | GT | LT | GTEQ | LTEQ; + +/** Terminals **/ + +TRUE : ([tT]'rue' | 'tt'); +FALSE : ([fF]'alse' | 'ff'); + +IN : 'in'; +OUT : 'out'; + +PLUS : '+'; +MINUS : '-'; + +/** Operators **/ + +EX : 'EX'; +EF : 'EF'; +EG : 'EG'; +AX : 'AX'; +AF : 'AF'; +AG : 'AG'; +EU : 'EU'; +AU : 'AU'; + +EQ : '=='; +NEQ : '!='; +GT : '>'; +LT : '<'; +GTEQ : '>='; +LTEQ : '<='; + +NEG : '!'; +CON : '&&'; +DIS : '||'; +IMPL : '=>'; +EQIV : '<=>'; + +/* Literals */ + +STRING : ["].+?["]; //non-greedy match till next quotation mark +VAR_NAME : [a-zA-Z]+[a-zA-Z0-9]*; +FLOAT_VAL : [-]?[0-9]*[.]?[0-9]+; + +NEWLINE : '\r'?'\n'; + +WS : [ \t\u]+ -> channel(HIDDEN) ; + +Block_comment : '/*' (Block_comment|.)*? '*/' -> channel(HIDDEN) ; // nesting allow +Line_comment : '//' .*? '\n' -> channel(HIDDEN) ; \ No newline at end of file diff --git a/src/main/java/cz/muni/fi/ctl/FormulaNormalizer.java b/src/main/java/cz/muni/fi/ctl/FormulaNormalizer.java deleted file mode 100644 index f873ece..0000000 --- a/src/main/java/cz/muni/fi/ctl/FormulaNormalizer.java +++ /dev/null @@ -1,87 +0,0 @@ -package cz.muni.fi.ctl; - -import cz.muni.fi.ctl.formula.Formula; -import cz.muni.fi.ctl.formula.FormulaImpl; -import cz.muni.fi.ctl.formula.operator.BinaryOperator; -import cz.muni.fi.ctl.formula.operator.Operator; -import cz.muni.fi.ctl.formula.operator.UnaryOperator; -import cz.muni.fi.ctl.formula.proposition.Proposition; -import cz.muni.fi.ctl.formula.proposition.Tautology; -import org.jetbrains.annotations.NotNull; - -/** - *

This class should transform formulas to normalized format processable by model checker.

- *

Note: only one normal form is currently supported.

- */ -public class FormulaNormalizer { - - @NotNull - public Formula normalize(@NotNull Formula formula) { - //leave propositions unchanged - if (formula instanceof Proposition) return formula; - @NotNull Operator operator = formula.getOperator(); - if (operator instanceof UnaryOperator) { - switch ((UnaryOperator) operator) { - case ALL_NEXT: - // AX p = !EX !p - return - new FormulaImpl(UnaryOperator.NEGATION, - new FormulaImpl(UnaryOperator.EXISTS_NEXT, - new FormulaImpl(UnaryOperator.NEGATION, - normalize(formula.getSubFormulaAt(0)) - ))); - case EXISTS_FUTURE: - // EF p = E [ true U p ] - return new FormulaImpl(BinaryOperator.EXISTS_UNTIL, Tautology.INSTANCE, - normalize(formula.getSubFormulaAt(0)) - ); - case ALL_FUTURE: - // AF p = A [ true U p ] - return - new FormulaImpl(BinaryOperator.ALL_UNTIL, Tautology.INSTANCE, - normalize(formula.getSubFormulaAt(0)) - ); - case EXISTS_GLOBAL: - // EG p = ! A [ true U ! p ] - return new FormulaImpl(UnaryOperator.NEGATION, - new FormulaImpl(BinaryOperator.ALL_UNTIL, Tautology.INSTANCE, - new FormulaImpl(UnaryOperator.NEGATION, - normalize(formula.getSubFormulaAt(0)) - ))); - case ALL_GLOBAL: - // AG p = ! E [ true U ! p ] - return - new FormulaImpl(UnaryOperator.NEGATION, - new FormulaImpl(BinaryOperator.EXISTS_UNTIL, Tautology.INSTANCE, - new FormulaImpl(UnaryOperator.NEGATION, - normalize(formula.getSubFormulaAt(0)) - ))); - default: - return new FormulaImpl(formula.getOperator(), normalize(formula.getSubFormulaAt(0))); - } - } else if (operator instanceof BinaryOperator) { - switch ((BinaryOperator) operator) { - case IMPLICATION: - // a => b = !a || b - return new FormulaImpl(BinaryOperator.OR, - new FormulaImpl(UnaryOperator.NEGATION, - normalize(formula.getSubFormulaAt(0))), - normalize(formula.getSubFormulaAt(1)) - ); - case EQUIVALENCE: - // a <=> b = (a && b) || (!a && !b) - return new FormulaImpl(BinaryOperator.OR, - new FormulaImpl(BinaryOperator.AND, formula.getSubFormulaAt(0), formula.getSubFormulaAt(1)), - new FormulaImpl(BinaryOperator.AND, - new FormulaImpl(UnaryOperator.NEGATION, formula.getSubFormulaAt(0)), - new FormulaImpl(UnaryOperator.NEGATION, formula.getSubFormulaAt(1)) - )); - default: - return new FormulaImpl(formula.getOperator(), normalize(formula.getSubFormulaAt(0)), normalize(formula.getSubFormulaAt(1))); - } - } else { - throw new IllegalArgumentException("Unsupported operator type: " + operator); - } - } - -} diff --git a/src/main/java/cz/muni/fi/ctl/FormulaParser.java b/src/main/java/cz/muni/fi/ctl/FormulaParser.java deleted file mode 100644 index 8e13ef3..0000000 --- a/src/main/java/cz/muni/fi/ctl/FormulaParser.java +++ /dev/null @@ -1,59 +0,0 @@ -package cz.muni.fi.ctl; - -import cz.muni.fi.ctl.antlr.CTLLexer; -import cz.muni.fi.ctl.antlr.CTLParser; -import cz.muni.fi.ctl.formula.Formula; -import cz.muni.fi.ctl.formula.proposition.Proposition; -import org.antlr.v4.runtime.ANTLRInputStream; -import org.antlr.v4.runtime.BufferedTokenStream; -import org.jetbrains.annotations.NotNull; -import org.jetbrains.annotations.Nullable; - -import java.io.File; -import java.io.FileInputStream; -import java.io.IOException; -import java.io.InputStream; -import java.util.Collection; - -public class FormulaParser { - - @NotNull - public Formula parse(@NotNull File input) throws IOException { - @Nullable InputStream inputStream = null; - try { - inputStream = new FileInputStream(input); - return parse(new ANTLRInputStream(inputStream)); - } finally { - if (inputStream != null) { - inputStream.close(); - } - } - } - - @NotNull - public Formula parse(@NotNull String input) throws IllegalStateException { - return parse(new ANTLRInputStream(input.toCharArray(), input.length())); - } - - private Formula parse(ANTLRInputStream is) { - CTLParser.RootContext root = new CTLParser(new BufferedTokenStream(new CTLLexer(is))).root(); - Collection propositions = root.propositions.values(); - Formula formula = root.result; - findUnusedPropositions(propositions, formula); - if (!propositions.isEmpty()) { - throw new IllegalArgumentException("Unused proposition: "+propositions.iterator().next().toString()); - } - return formula; - } - - private void findUnusedPropositions(Collection propositions, Formula formula) { - if (formula instanceof Proposition) { - propositions.remove(formula); - return; - } - for (Formula sub : formula.getSubFormulas()) { - findUnusedPropositions(propositions, sub); - } - } - -} diff --git a/src/main/java/cz/muni/fi/ctl/formula/Formula.java b/src/main/java/cz/muni/fi/ctl/formula/Formula.java deleted file mode 100644 index be73689..0000000 --- a/src/main/java/cz/muni/fi/ctl/formula/Formula.java +++ /dev/null @@ -1,23 +0,0 @@ -package cz.muni.fi.ctl.formula; - - -import cz.muni.fi.ctl.formula.operator.Operator; -import org.jetbrains.annotations.NotNull; - -import java.util.Collection; - -public interface Formula { - - /** Get number of sub formulas. **/ - public int getSubFormulaCount(); - - /** Get sub formula at specified index. **/ - public Formula getSubFormulaAt(int index); - - @NotNull - public Collection getSubFormulas(); - - @NotNull - public Operator getOperator(); - -} diff --git a/src/main/java/cz/muni/fi/ctl/formula/FormulaImpl.java b/src/main/java/cz/muni/fi/ctl/formula/FormulaImpl.java deleted file mode 100644 index 8964b2a..0000000 --- a/src/main/java/cz/muni/fi/ctl/formula/FormulaImpl.java +++ /dev/null @@ -1,81 +0,0 @@ -package cz.muni.fi.ctl.formula; - -import cz.muni.fi.ctl.formula.operator.NullaryOperator; -import cz.muni.fi.ctl.formula.operator.Operator; -import org.jetbrains.annotations.NotNull; - -import java.util.*; - -public class FormulaImpl implements Formula { - - @NotNull - private final Operator operator; - @NotNull - private final List formulas = new ArrayList<>(); - - /** - * Utility constructor for nullary formulas. - */ - public FormulaImpl() { - this.operator = NullaryOperator.INSTANCE; - } - - /** - * Universal constructor for creating formulas with any cardinality. - * @param operator N-ary operator. - * @param formulas List of N formulas (empty list for nullary operator). - */ - public FormulaImpl(@NotNull Operator operator, @NotNull Formula... formulas) { - this.operator = operator; - if (operator.getCardinality() != formulas.length) { - throw new IllegalArgumentException("Operator requires "+operator.getCardinality()+" subFormulas, "+formulas.length+" formulas provided"); - } - this.formulas.addAll(Arrays.asList(formulas)); - } - - @Override - public int getSubFormulaCount() { - return operator.getCardinality(); - } - - @Override - public Formula getSubFormulaAt(int index) { - return formulas.get(index); - } - - @NotNull - @Override - public Collection getSubFormulas() { - return Collections.unmodifiableCollection(formulas); - } - - @NotNull - @Override - public Operator getOperator() { - return operator; - } - - @NotNull - @Override - public String toString() { - return operator + ": " + Arrays.toString(formulas.toArray()); - } - - @Override - public boolean equals(Object o) { - if (this == o) return true; - if (!(o instanceof FormulaImpl)) return false; - - @NotNull FormulaImpl formula = (FormulaImpl) o; - - return formulas.equals(formula.formulas) && operator.equals(formula.operator); - - } - - @Override - public int hashCode() { - int result = operator.hashCode(); - result = 31 * result + formulas.hashCode(); - return result; - } -} diff --git a/src/main/java/cz/muni/fi/ctl/formula/operator/BinaryOperator.java b/src/main/java/cz/muni/fi/ctl/formula/operator/BinaryOperator.java deleted file mode 100644 index 527eb02..0000000 --- a/src/main/java/cz/muni/fi/ctl/formula/operator/BinaryOperator.java +++ /dev/null @@ -1,12 +0,0 @@ -package cz.muni.fi.ctl.formula.operator; - -public enum BinaryOperator implements Operator { - AND, OR, IMPLICATION, EQUIVALENCE, EXISTS_UNTIL, ALL_UNTIL - ; - - @Override - public int getCardinality() { - return 2; - } - -} diff --git a/src/main/java/cz/muni/fi/ctl/formula/operator/NullaryOperator.java b/src/main/java/cz/muni/fi/ctl/formula/operator/NullaryOperator.java deleted file mode 100644 index a1c022b..0000000 --- a/src/main/java/cz/muni/fi/ctl/formula/operator/NullaryOperator.java +++ /dev/null @@ -1,12 +0,0 @@ -package cz.muni.fi.ctl.formula.operator; - -public class NullaryOperator implements Operator { - public static final NullaryOperator INSTANCE = new NullaryOperator(); - - private NullaryOperator() {} - - @Override - public int getCardinality() { - return 0; - } -} diff --git a/src/main/java/cz/muni/fi/ctl/formula/operator/Operator.java b/src/main/java/cz/muni/fi/ctl/formula/operator/Operator.java deleted file mode 100644 index 7d4fb91..0000000 --- a/src/main/java/cz/muni/fi/ctl/formula/operator/Operator.java +++ /dev/null @@ -1,7 +0,0 @@ -package cz.muni.fi.ctl.formula.operator; - -public interface Operator { - - public int getCardinality(); - -} diff --git a/src/main/java/cz/muni/fi/ctl/formula/operator/UnaryOperator.java b/src/main/java/cz/muni/fi/ctl/formula/operator/UnaryOperator.java deleted file mode 100644 index 1ce45f4..0000000 --- a/src/main/java/cz/muni/fi/ctl/formula/operator/UnaryOperator.java +++ /dev/null @@ -1,12 +0,0 @@ -package cz.muni.fi.ctl.formula.operator; - -public enum UnaryOperator implements Operator { - NEGATION, EXISTS_NEXT, ALL_NEXT, EXISTS_FUTURE, ALL_FUTURE, EXISTS_GLOBAL, ALL_GLOBAL - ; - - @Override - public int getCardinality() { - return 1; - } - -} diff --git a/src/main/java/cz/muni/fi/ctl/formula/proposition/Contradiction.java b/src/main/java/cz/muni/fi/ctl/formula/proposition/Contradiction.java deleted file mode 100644 index ec64756..0000000 --- a/src/main/java/cz/muni/fi/ctl/formula/proposition/Contradiction.java +++ /dev/null @@ -1,22 +0,0 @@ -package cz.muni.fi.ctl.formula.proposition; - -import org.jetbrains.annotations.NotNull; - -public class Contradiction extends Proposition { - - public static final Contradiction INSTANCE = new Contradiction(); - - private Contradiction() {} - - @Override - public boolean evaluate(Object value) { - return false; - } - - @NotNull - @Override - public String toString() { - return "False"; - } - -} diff --git a/src/main/java/cz/muni/fi/ctl/formula/proposition/FloatProposition.java b/src/main/java/cz/muni/fi/ctl/formula/proposition/FloatProposition.java deleted file mode 100644 index c8ad358..0000000 --- a/src/main/java/cz/muni/fi/ctl/formula/proposition/FloatProposition.java +++ /dev/null @@ -1,94 +0,0 @@ -package cz.muni.fi.ctl.formula.proposition; - -import org.jetbrains.annotations.NotNull; - -public class FloatProposition extends Proposition { - - private final double value; - private final String variable; - private final Operator operator; - - public FloatProposition(double value, String variable, Operator operator) { - this.value = value; - this.operator = operator; - this.variable = variable; - } - - @Override - public boolean evaluate(Double value) { - switch (operator) { - case LT: - return value < this.value; - case LT_EQ: - return value <= this.value; - case GT: - return value > this.value; - case GT_EQ: - return value >= this.value; - case NEQ: - return value != this.value; - case EQ: - default: - return value == this.value; - } - } - - public Operator getFloatOperator() { - return operator; - } - - public double getThreshold() { - return value; - } - - public String getVariable() { - return variable; - } - - public static enum Operator { - EQ("==", -1), NEQ("!=", -1), GT(">", 0), GT_EQ(">=", 2), LT("<", 1), LT_EQ("<=", 3); - - private final String val; - //represents an integer passed to an enum inside a native library - private final int nativeIndex; - - Operator(String val, int nativeIndex) { - this.val = val; - this.nativeIndex = nativeIndex; - } - - @Override - public String toString() { - return val; - } - - public int getOperatorIndex() { - return nativeIndex; - } - } - - @NotNull - @Override - public String toString() { - return variable+" "+operator+" "+value; - } - - @Override - public boolean equals(Object o) { - if (this == o) return true; - if (!(o instanceof FloatProposition)) return false; - - @NotNull FloatProposition that = (FloatProposition) o; - - return Double.compare(that.value, value) == 0 && operator == that.operator && variable.equals(that.variable); - - } - - @Override - public int hashCode() { - long result = (value != +0.0f ? Double.doubleToLongBits(value) : 0); - result = 31 * result + variable.hashCode(); - result = 31 * result + operator.hashCode(); - return (int) result; - } -} diff --git a/src/main/java/cz/muni/fi/ctl/formula/proposition/Proposition.java b/src/main/java/cz/muni/fi/ctl/formula/proposition/Proposition.java deleted file mode 100644 index ba43736..0000000 --- a/src/main/java/cz/muni/fi/ctl/formula/proposition/Proposition.java +++ /dev/null @@ -1,37 +0,0 @@ -package cz.muni.fi.ctl.formula.proposition; - -import cz.muni.fi.ctl.formula.Formula; -import cz.muni.fi.ctl.formula.operator.NullaryOperator; -import cz.muni.fi.ctl.formula.operator.Operator; -import org.jetbrains.annotations.NotNull; - -import java.util.ArrayList; -import java.util.Collection; - -public abstract class Proposition implements Formula { - - public abstract boolean evaluate(T value); - - @Override - public int getSubFormulaCount() { - return 0; - } - - @NotNull - @Override - public Formula getSubFormulaAt(int index) { - throw new IndexOutOfBoundsException("Requested index "+index+", size 0"); - } - - @NotNull - @Override - public Collection getSubFormulas() { - return new ArrayList<>(); - } - - @NotNull - @Override - public Operator getOperator() { - return NullaryOperator.INSTANCE; - } -} diff --git a/src/main/java/cz/muni/fi/ctl/formula/proposition/Tautology.java b/src/main/java/cz/muni/fi/ctl/formula/proposition/Tautology.java deleted file mode 100644 index 9162b89..0000000 --- a/src/main/java/cz/muni/fi/ctl/formula/proposition/Tautology.java +++ /dev/null @@ -1,21 +0,0 @@ -package cz.muni.fi.ctl.formula.proposition; - -import org.jetbrains.annotations.NotNull; - -public class Tautology extends Proposition { - - public static final Tautology INSTANCE = new Tautology(); - - private Tautology() {} - - @Override - public boolean evaluate(Object value) { - return true; - } - - @NotNull - @Override - public String toString() { - return "True"; - } -} diff --git a/src/main/kotlin/cz/muni/fi/ctl/Formulas.kt b/src/main/kotlin/cz/muni/fi/ctl/Formulas.kt new file mode 100644 index 0000000..b4eb52a --- /dev/null +++ b/src/main/kotlin/cz/muni/fi/ctl/Formulas.kt @@ -0,0 +1,90 @@ +package cz.muni.fi.ctl + +//Formulas +public interface Formula { + val operator: Op + val subFormulas: List + + public fun get(i: Int): Formula = subFormulas[i] +} + +data class FormulaImpl ( + override val operator: Op = Op.ATOM, + override val subFormulas: List = listOf() +) : Formula { + + init { + if (subFormulas.size() != operator.cardinality) { + throw IllegalArgumentException( + "Operator cardinality(${operator.cardinality}) and " + + "number of sub formulas(${subFormulas.size()}) do not match") + } + } + + constructor(operator: Op, vararg formulas: Formula) : this(operator, formulas.toList()) + + override fun toString(): String = when (operator.cardinality) { + 1 -> "$operator ${subFormulas[0]}" + 2 -> "(${subFormulas[0]} $operator ${subFormulas[1]})" + else -> "$operator($subFormulas)" //this never happens + } + +} + +public open class Atom : Formula { + final override val operator = Op.ATOM + final override val subFormulas = listOf() +} + +//Boolean Atoms +public val True: Formula = object : Atom() { + override fun toString():String = "True" +} + +public val False: Formula = object : Atom() { + override fun toString():String = "False" +} + +//Float atoms +public data class FloatProposition ( + val variable: String, + val floatOp: FloatOp, + val value: Double +) : Atom() { + override fun toString(): String = "$variable $floatOp $value" +} + +//Direction atoms +public data class DirectionProposition ( + val variable: String, + val direction: Direction, + val facet: Facet +) : Atom() { + + override fun toString(): String = "$variable:$direction$facet" + +} + + +//Simplified builders +public fun not(f: Formula): Formula = FormulaImpl(Op.NEGATION, f) +public fun EX(f: Formula): Formula = FormulaImpl(Op.EXISTS_NEXT, f) +public fun AX(f: Formula): Formula = FormulaImpl(Op.ALL_NEXT, f) +public fun EF(f: Formula): Formula = FormulaImpl(Op.EXISTS_FUTURE, f) +public fun AF(f: Formula): Formula = FormulaImpl(Op.ALL_FUTURE, f) +public fun EG(f: Formula): Formula = FormulaImpl(Op.EXISTS_GLOBAL, f) +public fun AG(f: Formula): Formula = FormulaImpl(Op.ALL_GLOBAL, f) +public fun Formula.or(f2: Formula): Formula = FormulaImpl(Op.OR, this, f2) +public fun Formula.and(f2: Formula): Formula = FormulaImpl(Op.AND, this, f2) +public fun Formula.implies(f2: Formula): Formula = FormulaImpl(Op.IMPLICATION, this, f2) +public fun Formula.equal(f2: Formula): Formula = FormulaImpl(Op.EQUIVALENCE, this, f2) +public fun Formula.EU(f2: Formula): Formula = FormulaImpl(Op.EXISTS_UNTIL, this, f2) +public fun Formula.AU(f2: Formula): Formula = FormulaImpl(Op.ALL_UNTIL, this, f2) + +//this is not typical map semantics -> don't make it public +fun Formula.treeMap(x: (Formula) -> Formula) = + if (this.operator.cardinality == 0) { + this + } else { + FormulaImpl(this.operator, this.subFormulas.map(x)) + } diff --git a/src/main/kotlin/cz/muni/fi/ctl/Normalizer.kt b/src/main/kotlin/cz/muni/fi/ctl/Normalizer.kt new file mode 100644 index 0000000..efff5fb --- /dev/null +++ b/src/main/kotlin/cz/muni/fi/ctl/Normalizer.kt @@ -0,0 +1,47 @@ +package cz.muni.fi.ctl + +val untilNormalForm: Map Formula) -> Formula> = mapOf( + Op.ALL_NEXT to { + // AX p = !EX !p + f, x -> not( EX( not( x(f[0]) ) ) ) + }, + Op.EXISTS_FUTURE to { + // EF p = E [ true U p ] + f, x -> True EU x(f[0]) + }, + Op.ALL_FUTURE to { + // AF p = A [ true U p ] + f, x -> True AU x(f[0]) + }, + Op.EXISTS_GLOBAL to { + // EG p = ! A [ true U ! p ] + f, x -> not( True AU not( x(f[0]) ) ) + }, + Op.ALL_GLOBAL to { + // AG p = ! E [ true U ! p ] + f, x -> not( True EU not( x(f[0]) ) ) + }, + Op.IMPLICATION to { + // a => b = !a || b + f, x -> not(x(f[0])) or x(f[1]) + }, + Op.EQUIVALENCE to { + // a <=> b = (a && b) || (!a && !b) + f, x -> (x(f[0]) and x(f[1])) or (not(x(f[0])) and not(x(f[1]))) + } +) + +public class Normalizer( + normalForm: Map Formula) -> Formula> = untilNormalForm +) { + + private val normalForm = normalForm + + public fun normalize(f: Formula) : Formula { + + val normalize = { f: Formula -> normalize(f) } + + return normalForm[f.operator]?.invoke(f, normalize) ?: f.treeMap(normalize) + } + +} \ No newline at end of file diff --git a/src/main/kotlin/cz/muni/fi/ctl/Operators.kt b/src/main/kotlin/cz/muni/fi/ctl/Operators.kt new file mode 100644 index 0000000..d651b67 --- /dev/null +++ b/src/main/kotlin/cz/muni/fi/ctl/Operators.kt @@ -0,0 +1,50 @@ +package cz.muni.fi.ctl + +public enum class Op(val cardinality: Int, private val str: String) { + //nullary + ATOM(0,"null"), + //unary + NEGATION(1, "!"), + EXISTS_NEXT(1, "EX"), + ALL_NEXT(1, "AX"), + EXISTS_FUTURE(1, "EF"), + ALL_FUTURE(1, "AF"), + EXISTS_GLOBAL(1, "EG"), + ALL_GLOBAL(1, "AG"), + //binary + AND(2, "&&"), + OR(2, "||"), + IMPLICATION(2, "=>"), + EQUIVALENCE(2, "<=>"), + EXISTS_UNTIL(2, "EU"), + ALL_UNTIL(2, "AU"); + + override fun toString(): String = str +} + +public enum class FloatOp(private val str: String) { + EQ("=="), NEQ("!="), GT(">"), GT_EQ(">="), LT("<"), LT_EQ("<="); + + val neg: FloatOp + get() = when (this) { + EQ -> NEQ + NEQ -> EQ + GT -> LT_EQ + GT_EQ -> LT + LT -> GT_EQ + LT_EQ -> GT + } + + override fun toString(): String = str + +} + +public enum class Direction(private val str: String) { + IN("in"), OUT("out"); + override fun toString(): String = str +} + +public enum class Facet(private val str: String) { + POSITIVE("+"), NEGATIVE("-"); + override fun toString(): String = str +} \ No newline at end of file diff --git a/src/main/kotlin/cz/muni/fi/ctl/Optimizer.kt b/src/main/kotlin/cz/muni/fi/ctl/Optimizer.kt new file mode 100644 index 0000000..8ae9c99 --- /dev/null +++ b/src/main/kotlin/cz/muni/fi/ctl/Optimizer.kt @@ -0,0 +1,86 @@ +package cz.muni.fi.ctl + + +public class Optimizer { + + public fun optimize(f: Formula): Formula { + //it's hard to optimize while formula at once, so we just compute it as a fix point + var one = optimizeTree(f) + var two = optimizeTree(one) + while(two != one) { + one = two + two = optimizeTree(two) + } + return two + } + + private val optimize = { f: Formula -> optimizeTree(f) } + + private fun optimizeTree(f: Formula): Formula = when { + f.operator.cardinality == 0 -> f + f.operator == Op.NEGATION -> { + val child = f[0] + when { + // !True = False + child == True -> False + // !False = True + child == False -> True + // !a > 5 = a <= 5 + child is FloatProposition -> child.copy(floatOp = child.floatOp.neg) + // !!a = a + child.operator == Op.NEGATION -> optimizeTree(child[0]) + else -> f.treeMap(optimize) + } + } + f.operator == Op.AND -> + when { + // a && False = False + False in f.subFormulas -> False + // a && True = a + f[0] == True -> optimizeTree(f[1]) + f[1] == True -> optimizeTree(f[0]) + //!a && !b = !(a || b) + f[0].operator == Op.NEGATION && f[1].operator == Op.NEGATION -> + not(optimizeTree(f[0][0]) or optimizeTree(f[1][0])) + else -> f.treeMap(optimize) + } + f.operator == Op.OR -> + when { + // a || True = True + True in f.subFormulas -> True + // a || False = a + f[0] == False -> optimizeTree(f[1]) + f[1] == False -> optimizeTree(f[0]) + // !a || !b = !(a && b) + f[0].operator == Op.NEGATION && f[1].operator == Op.NEGATION -> + not(optimizeTree(f[0][0]) and optimizeTree(f[1][0])) + else -> f.treeMap(optimize) + } + f.operator == Op.EXISTS_UNTIL -> + when { + // E a U True = True + f[1] == True -> True + // E a U False = False + f[1] == False -> False + else -> f.treeMap(optimize) + } + f.operator == Op.ALL_UNTIL -> + when { + // A a U True = True + f[1] == True -> True + // A a U False = False + f[1] == False -> False + else -> f.treeMap(optimize) + } + f.operator == Op.EXISTS_NEXT -> + when { + // EX True = True + f[0] == True -> True + // EX False = False + f[0] == False -> False + else -> f.treeMap(optimize) + } + else -> + f.treeMap(optimize) + } +} \ No newline at end of file diff --git a/src/main/kotlin/cz/muni/fi/ctl/Parser.kt b/src/main/kotlin/cz/muni/fi/ctl/Parser.kt new file mode 100644 index 0000000..c5e4720 --- /dev/null +++ b/src/main/kotlin/cz/muni/fi/ctl/Parser.kt @@ -0,0 +1,233 @@ +package cz.muni.fi.ctl + +import cz.muni.fi.ctl.antlr.CTLBaseListener +import cz.muni.fi.ctl.antlr.CTLLexer +import cz.muni.fi.ctl.antlr.CTLParser +import org.antlr.v4.runtime.ANTLRInputStream +import org.antlr.v4.runtime.CommonTokenStream +import org.antlr.v4.runtime.tree.ParseTree +import org.antlr.v4.runtime.tree.ParseTreeProperty +import org.antlr.v4.runtime.tree.ParseTreeWalker +import java.io.File +import java.util.* + +/** + * Workflow: + * Antlr constructs a parse tree that is transformed into FileContext. + * File context is a direct representation of a file. + * Using FileParser, includes in the file context are resolved and merged into a ParserContext. + * Duplicate assignments are checked at this stage. + * Lastly, Parser resolves references in ParserContext (checking for undefined or cyclic references) + * and returns a final map of valid assignments + */ + +public class Parser { + + public fun formula(input: String): Formula = parse("val = $input").get("val")!! + + public fun parse(input: String): Map = process(FileParser().process(input)) + + public fun parse(input: File): Map = process(FileParser().process(input)) + + fun process(ctx: ParserContext): Map { + + val formulas = ctx.formulas + + // Resolve references + + val references = HashMap(formulas) //mutable copy + val replaced = Stack() //processing stack for cycle detection + + fun replace(f: Formula): Formula = when (f) { + is Reference -> when { + f.name !in references -> + throw IllegalStateException("Undefined reference: ${f.name}") + f.name in replaced -> + throw IllegalStateException("Cyclic reference: ${f.name}") + else -> { + replaced.push(f.name) + val result = references[f.name]!!.treeMap(::replace) + replaced.pop() + result + } + } + else -> f.treeMap(::replace) + } + + for ((name, formula) in formulas) { + references[name] = replace(formula) + } + + return references + } + +} + +class FileParser { + + private val processed = HashSet() + + fun process(input: String): ParserContext { + val ctx = processString(input) + return ctx.includes.map { process(it) }.fold(ctx.toParseContext(), ParserContext::plus) + } + + fun process(input: File): ParserContext { + val ctx = processFile(input) + processed.add(input) + return ctx.includes. + filter { it !in processed }. + map { process(it) }. + fold (ctx.toParseContext(), ParserContext::plus) + } + + private fun processString(input: String): FileContext = + processStream(ANTLRInputStream(input.toCharArray(), input.length()), "input string") + + private fun processFile(input: File): FileContext = + input.inputStream().use { processStream(ANTLRInputStream(it), input.absolutePath) } + + private fun processStream(input: ANTLRInputStream, location: String): FileContext { + val root = CTLParser(CommonTokenStream(CTLLexer(input))).root() + val context = FileContext(location) + ParseTreeWalker().walk(context, root) + return context + } + +} + +data class ParserContext( + val assignments: List +) { + + val formulas: Map + get() = assignments.toMap({ it.name }, { it.formula} ) + + /** + * Checks for duplicate assignments received from parser + */ + init { + for (one in assignments) { + for (two in assignments) { + if (one.name == two.name && (one.location != two.location || one.formula != two.formula)) { + throw IllegalStateException( + "Duplicate assignment for ${one.name} defined in ${one.location} and ${two.location}" + ) + } + } + } + } + + fun plus(ctx: ParserContext): ParserContext { + return ParserContext(assignments + ctx.assignments) + } + +} + +class FileContext(val location: String) : CTLBaseListener() { + + val includes = ArrayList() + val assignments = ArrayList() + + private val formulas = ParseTreeProperty() + + fun toParseContext() = ParserContext(assignments) + + override fun exitInclude(ctx: CTLParser.IncludeContext) { + val string = ctx.STRING().text!! + includes.add(File(string.substring(1, string.length() - 1))) //remove quotes + } + + override fun exitAssign(ctx: CTLParser.AssignContext) { + assignments.add(Assignment( + ctx.VAR_NAME().text!!, + formulas[ctx.formula()]!!, + location+":"+ctx.start.line + )) + } + + /** ------ Formula Parsing ------ **/ + + override fun exitId(ctx: CTLParser.IdContext) { + formulas[ctx] = Reference(ctx.text!!) + } + + override fun exitBool(ctx: CTLParser.BoolContext) { + formulas[ctx] = if (ctx.TRUE() != null) True else False + } + + override fun exitDirection(ctx: CTLParser.DirectionContext) { + formulas[ctx] = DirectionProposition( + variable = ctx.VAR_NAME().text!!, + direction = if (ctx.IN() != null) Direction.IN else Direction.OUT, + facet = if (ctx.PLUS() != null) Facet.POSITIVE else Facet.NEGATIVE + ) + } + + override fun exitProposition(ctx: CTLParser.PropositionContext) { + formulas[ctx] = FloatProposition( + variable = ctx.VAR_NAME().text!!, + floatOp = ctx.floatOp().toOperator(), + value = ctx.FLOAT_VAL().text.toDouble() + ) + } + + override fun exitParenthesis(ctx: CTLParser.ParenthesisContext) { + formulas[ctx] = formulas[ctx.formula()]!! + } + + override fun exitUnary(ctx: CTLParser.UnaryContext) { + formulas[ctx] = FormulaImpl(ctx.unaryOp().toOperator(), formulas[ctx.formula()]!!) + } + + override fun exitOr(ctx: CTLParser.OrContext) { + formulas[ctx] = formulas[ctx.formula(0)]!! or formulas[ctx.formula(1)]!! + } + + override fun exitAnd(ctx: CTLParser.AndContext) { + formulas[ctx] = formulas[ctx.formula(0)]!! and formulas[ctx.formula(1)]!! + } + + override fun exitImplies(ctx: CTLParser.ImpliesContext) { + formulas[ctx] = formulas[ctx.formula(0)]!! implies formulas[ctx.formula(1)]!! + } + + override fun exitEqual(ctx: CTLParser.EqualContext) { + formulas[ctx] = formulas[ctx.formula(0)]!! equal formulas[ctx.formula(1)]!! + } + + override fun exitEU(ctx: CTLParser.EUContext) { + formulas[ctx] = formulas[ctx.formula(0)]!! EU formulas[ctx.formula(1)]!! + } + + override fun exitAU(ctx: CTLParser.AUContext) { + formulas[ctx] = formulas[ctx.formula(0)]!! AU formulas[ctx.formula(1)]!! + } +} + +data class Assignment(val name: String, val formula: Formula, val location: String) + +data class Reference(val name: String) : Atom() + +//convenience methods + +fun CTLParser.UnaryOpContext.toOperator(): Op = when { + EX() != null -> Op.EXISTS_NEXT + AX() != null -> Op.ALL_NEXT + EF() != null -> Op.EXISTS_FUTURE + AF() != null -> Op.ALL_FUTURE + EG() != null -> Op.EXISTS_GLOBAL + AG() != null -> Op.ALL_GLOBAL + else -> Op.NEGATION +} + +fun CTLParser.FloatOpContext.toOperator(): FloatOp = when { + NEQ() != null -> FloatOp.NEQ + LT() != null -> FloatOp.LT + LTEQ() != null -> FloatOp.LT_EQ + GT() != null -> FloatOp.GT + GTEQ() != null -> FloatOp.GT_EQ + else -> FloatOp.EQ +} + +fun ParseTreeProperty.set(k: ParseTree, v: T) = this.put(k, v) diff --git a/src/test/java/FormulaNormalizerTest.java b/src/test/java/FormulaNormalizerTest.java deleted file mode 100644 index 31f5b08..0000000 --- a/src/test/java/FormulaNormalizerTest.java +++ /dev/null @@ -1,147 +0,0 @@ - -import cz.muni.fi.ctl.FormulaNormalizer; -import cz.muni.fi.ctl.formula.Formula; -import cz.muni.fi.ctl.formula.FormulaImpl; -import cz.muni.fi.ctl.formula.operator.BinaryOperator; -import cz.muni.fi.ctl.formula.operator.UnaryOperator; -import cz.muni.fi.ctl.formula.proposition.Contradiction; -import cz.muni.fi.ctl.formula.proposition.FloatProposition; -import cz.muni.fi.ctl.formula.proposition.Proposition; -import cz.muni.fi.ctl.formula.proposition.Tautology; -import org.junit.Test; - -import static org.junit.Assert.assertEquals; - -/** - * Tests for FormulaNormalizer - */ -public class FormulaNormalizerTest { - - @Test - public void propositionTest() { - FormulaNormalizer normalizer = new FormulaNormalizer(); - assertEquals(Tautology.INSTANCE, normalizer.normalize(Tautology.INSTANCE)); - assertEquals(Contradiction.INSTANCE, normalizer.normalize(Contradiction.INSTANCE)); - Proposition proposition = new FloatProposition(34.5, "aaa", FloatProposition.Operator.GT_EQ); - assertEquals(proposition, normalizer.normalize(proposition)); - } - - @Test - public void unchangedTest() { - FormulaNormalizer normalizer = new FormulaNormalizer(); - Formula ex = new FormulaImpl(UnaryOperator.EXISTS_NEXT, Tautology.INSTANCE); - assertEquals(ex, normalizer.normalize(ex)); - Formula eu = new FormulaImpl(BinaryOperator.EXISTS_UNTIL, Tautology.INSTANCE, Contradiction.INSTANCE); - assertEquals(eu, normalizer.normalize(eu)); - Formula au = new FormulaImpl(BinaryOperator.ALL_UNTIL, Tautology.INSTANCE, Contradiction.INSTANCE); - assertEquals(au, normalizer.normalize(au)); - Formula neg = new FormulaImpl(UnaryOperator.NEGATION, Tautology.INSTANCE); - assertEquals(neg, normalizer.normalize(neg)); - Formula and = new FormulaImpl(BinaryOperator.AND, Tautology.INSTANCE, Contradiction.INSTANCE); - assertEquals(and, normalizer.normalize(and)); - Formula or = new FormulaImpl(BinaryOperator.OR, Tautology.INSTANCE, Contradiction.INSTANCE); - assertEquals(or, normalizer.normalize(or)); - } - - @Test - public void allNextTest() { - FormulaNormalizer normalizer = new FormulaNormalizer(); - Formula norm = new FormulaImpl(UnaryOperator.NEGATION, - new FormulaImpl(UnaryOperator.EXISTS_NEXT, - new FormulaImpl(UnaryOperator.NEGATION, Tautology.INSTANCE))); - assertEquals(norm, normalizer.normalize(new FormulaImpl(UnaryOperator.ALL_NEXT, Tautology.INSTANCE))); - } - - - @Test - public void allFutureTest() { - FormulaNormalizer normalizer = new FormulaNormalizer(); - Formula norm = new FormulaImpl(BinaryOperator.ALL_UNTIL, Tautology.INSTANCE, Contradiction.INSTANCE); - assertEquals(norm, normalizer.normalize(new FormulaImpl(UnaryOperator.ALL_FUTURE, Contradiction.INSTANCE))); - } - - @Test - public void existsFutureTest() { - FormulaNormalizer normalizer = new FormulaNormalizer(); - Formula norm = new FormulaImpl(BinaryOperator.EXISTS_UNTIL, Tautology.INSTANCE, Contradiction.INSTANCE); - assertEquals(norm, normalizer.normalize(new FormulaImpl(UnaryOperator.EXISTS_FUTURE, Contradiction.INSTANCE))); - } - - @Test - public void allGlobalTest() { - FormulaNormalizer normalizer = new FormulaNormalizer(); - Formula norm = new FormulaImpl(UnaryOperator.NEGATION, - new FormulaImpl(BinaryOperator.EXISTS_UNTIL, Tautology.INSTANCE, - new FormulaImpl(UnaryOperator.NEGATION, Contradiction.INSTANCE))); - assertEquals(norm, normalizer.normalize(new FormulaImpl(UnaryOperator.ALL_GLOBAL, Contradiction.INSTANCE))); - } - - @Test - public void existsGlobalTest() { - FormulaNormalizer normalizer = new FormulaNormalizer(); - Formula norm = new FormulaImpl(UnaryOperator.NEGATION, - new FormulaImpl(BinaryOperator.ALL_UNTIL, Tautology.INSTANCE, - new FormulaImpl(UnaryOperator.NEGATION, Contradiction.INSTANCE))); - assertEquals(norm, normalizer.normalize(new FormulaImpl(UnaryOperator.EXISTS_GLOBAL, Contradiction.INSTANCE))); - } - - @Test - public void implicationTest() { - FormulaNormalizer normalizer = new FormulaNormalizer(); - Formula norm = new FormulaImpl(BinaryOperator.OR, new FormulaImpl(UnaryOperator.NEGATION, Contradiction.INSTANCE), Contradiction.INSTANCE); - assertEquals(norm, normalizer.normalize(new FormulaImpl(BinaryOperator.IMPLICATION, Contradiction.INSTANCE, Contradiction.INSTANCE))); - } - - @Test - public void equivalenceTest() { - FormulaNormalizer normalizer = new FormulaNormalizer(); - Formula norm = new FormulaImpl(BinaryOperator.OR, - new FormulaImpl(BinaryOperator.AND, Contradiction.INSTANCE, Contradiction.INSTANCE), - new FormulaImpl(BinaryOperator.AND, - new FormulaImpl(UnaryOperator.NEGATION, Contradiction.INSTANCE), - new FormulaImpl(UnaryOperator.NEGATION, Contradiction.INSTANCE) - )); - assertEquals(norm, normalizer.normalize(new FormulaImpl(BinaryOperator.EQUIVALENCE, Contradiction.INSTANCE, Contradiction.INSTANCE))); - } - - @Test - public void nestedUnchanged() { - FormulaNormalizer normalizer = new FormulaNormalizer(); - Formula sample = new FormulaImpl(BinaryOperator.AND, - new FormulaImpl(BinaryOperator.OR, - new FormulaImpl(BinaryOperator.ALL_UNTIL, - new FormulaImpl(UnaryOperator.EXISTS_NEXT, Tautology.INSTANCE), - new FormulaImpl(UnaryOperator.NEGATION, Tautology.INSTANCE) - ), - Contradiction.INSTANCE - ), - new FormulaImpl(BinaryOperator.EXISTS_UNTIL, - Tautology.INSTANCE, - Contradiction.INSTANCE - ) - ); - assertEquals(sample, normalizer.normalize(sample)); - } - - @Test - public void complexTest() { - FormulaNormalizer normalizer = new FormulaNormalizer(); - Formula sample = new FormulaImpl(BinaryOperator.AND, - new FormulaImpl(BinaryOperator.IMPLICATION, Contradiction.INSTANCE, Contradiction.INSTANCE), - new FormulaImpl(UnaryOperator.EXISTS_FUTURE, - new FormulaImpl(UnaryOperator.EXISTS_NEXT, - new FormulaImpl(UnaryOperator.ALL_GLOBAL, Contradiction.INSTANCE))) - ); - Formula expected = new FormulaImpl(BinaryOperator.AND, - new FormulaImpl(BinaryOperator.OR, - new FormulaImpl(UnaryOperator.NEGATION, Contradiction.INSTANCE), - Contradiction.INSTANCE), - new FormulaImpl(BinaryOperator.EXISTS_UNTIL, Tautology.INSTANCE, - new FormulaImpl(UnaryOperator.EXISTS_NEXT, - new FormulaImpl(UnaryOperator.NEGATION, - new FormulaImpl(BinaryOperator.EXISTS_UNTIL, Tautology.INSTANCE, - new FormulaImpl(UnaryOperator.NEGATION, Contradiction.INSTANCE))))) - ); - assertEquals(expected, normalizer.normalize(sample)); - } -} diff --git a/src/test/java/FormulaParserTest.java b/src/test/java/FormulaParserTest.java deleted file mode 100644 index e50ff7f..0000000 --- a/src/test/java/FormulaParserTest.java +++ /dev/null @@ -1,280 +0,0 @@ -import cz.muni.fi.ctl.FormulaParser; -import cz.muni.fi.ctl.formula.Formula; -import cz.muni.fi.ctl.formula.operator.BinaryOperator; -import cz.muni.fi.ctl.formula.operator.UnaryOperator; -import cz.muni.fi.ctl.formula.proposition.Contradiction; -import cz.muni.fi.ctl.formula.proposition.FloatProposition; -import cz.muni.fi.ctl.formula.proposition.Tautology; -import org.junit.Rule; -import org.junit.Test; -import org.junit.rules.ExpectedException; - -import static org.hamcrest.CoreMatchers.instanceOf; -import static org.junit.Assert.assertEquals; -import static org.junit.Assert.assertThat; - -/** - * Tests for FormulaParser - */ -public class FormulaParserTest { - - private static final float TOLERANCE = 0.0001f; - - @Rule - public final ExpectedException exception = ExpectedException.none(); - - @Test - public void propositionTest() { - FormulaParser parser = new FormulaParser(); - Formula formula = parser.parse("#define a B > 3.0 #property a"); - assertThat(formula, instanceOf(FloatProposition.class)); - FloatProposition proposition = (FloatProposition) formula; - assertEquals(proposition.getThreshold(), 3.0, TOLERANCE); - assertEquals(proposition.getVariable(), "B"); - //long names - formula = parser.parse("#define someLongName ANOTHERlongNAME > 1234.5678 #property someLongName"); - assertThat(formula, instanceOf(FloatProposition.class)); - proposition = (FloatProposition) formula; - assertEquals(proposition.getThreshold(), 1234.5678, TOLERANCE); - assertEquals(proposition.getVariable(), "ANOTHERlongNAME"); - //negative numbers - formula = parser.parse("#define a B > -23.4 #property a"); - assertThat(formula, instanceOf(FloatProposition.class)); - proposition = (FloatProposition) formula; - assertEquals(proposition.getThreshold(), -23.4, TOLERANCE); - assertEquals(proposition.getVariable(), "B"); - //unused propositions - //this should produce an exception - exception.expect(IllegalArgumentException.class); - parser.parse("#define a B > 3.0 #define c C <= 23.4 #define z Z > 4.0 #property c"); - //proposition redefinition - exception.expect(IllegalArgumentException.class); - parser.parse("#define a B > 3.0 #define a C <= 23.4 #define z Z > 4.0 #property c"); - //unknown proposition - exception.expect(IllegalArgumentException.class); - parser.parse("#define a B > 3.0 #define a C <= 23.4 #define z Z > 4.0 #property D"); - } - - @Test - public void floatValuesTest() { - FormulaParser parser = new FormulaParser(); - Formula formula = parser.parse("#define a B > 3 #property a"); - assertThat(formula, instanceOf(FloatProposition.class)); - FloatProposition proposition = (FloatProposition) formula; - assertEquals(proposition.getVariable(), "B"); - assertEquals(proposition.getThreshold(), 3, TOLERANCE); - formula = parser.parse("#define a B > -3 #property a"); - assertThat(formula, instanceOf(FloatProposition.class)); - proposition = (FloatProposition) formula; - assertEquals(proposition.getVariable(), "B"); - assertEquals(proposition.getThreshold(), -3, TOLERANCE); - formula = parser.parse("#define a B > 0.2 #property a"); - assertThat(formula, instanceOf(FloatProposition.class)); - proposition = (FloatProposition) formula; - assertEquals(proposition.getVariable(), "B"); - assertEquals(proposition.getThreshold(), 0.2, TOLERANCE); - formula = parser.parse("#define a B > -0.4 #property a"); - assertThat(formula, instanceOf(FloatProposition.class)); - proposition = (FloatProposition) formula; - assertEquals(proposition.getVariable(), "B"); - assertEquals(proposition.getThreshold(), -0.4, TOLERANCE); - formula = parser.parse("#define a B > .3 #property a"); - assertThat(formula, instanceOf(FloatProposition.class)); - proposition = (FloatProposition) formula; - assertEquals(proposition.getVariable(), "B"); - assertEquals(proposition.getThreshold(), 0.3, TOLERANCE); - formula = parser.parse("#define a B > -.9 #property a"); - assertThat(formula, instanceOf(FloatProposition.class)); - proposition = (FloatProposition) formula; - assertEquals(proposition.getVariable(), "B"); - assertEquals(proposition.getThreshold(), -0.9, TOLERANCE); - } - - @Test - public void booleanLiteralsTest() { - FormulaParser parser = new FormulaParser(); - Formula formula = parser.parse("#property True"); - assertThat(formula, instanceOf(Tautology.class)); - formula = parser.parse("#property False"); - assertThat(formula, instanceOf(Contradiction.class)); - } - - @Test - public void unaryTemporalOperatorTest() { - FormulaParser parser = new FormulaParser(); - Formula formula = parser.parse("#property EX False"); - assertEquals(formula.getSubFormulaCount(), 1); - assertThat(formula.getSubFormulaAt(0), instanceOf(Contradiction.class)); - assertThat(formula.getOperator(), instanceOf(UnaryOperator.class)); - assertEquals(formula.getOperator(), UnaryOperator.EXISTS_NEXT); - formula = parser.parse("#property AX False"); - assertEquals(formula.getSubFormulaCount(), 1); - assertThat(formula.getSubFormulaAt(0), instanceOf(Contradiction.class)); - assertThat(formula.getOperator(), instanceOf(UnaryOperator.class)); - assertEquals(formula.getOperator(), UnaryOperator.ALL_NEXT); - formula = parser.parse("#property EF False"); - assertEquals(formula.getSubFormulaCount(), 1); - assertThat(formula.getSubFormulaAt(0), instanceOf(Contradiction.class)); - assertThat(formula.getOperator(), instanceOf(UnaryOperator.class)); - assertEquals(formula.getOperator(), UnaryOperator.EXISTS_FUTURE); - formula = parser.parse("#property AF False"); - assertEquals(formula.getSubFormulaCount(), 1); - assertThat(formula.getSubFormulaAt(0), instanceOf(Contradiction.class)); - assertThat(formula.getOperator(), instanceOf(UnaryOperator.class)); - assertEquals(formula.getOperator(), UnaryOperator.ALL_FUTURE); - formula = parser.parse("#property EG False"); - assertEquals(formula.getSubFormulaCount(), 1); - assertThat(formula.getSubFormulaAt(0), instanceOf(Contradiction.class)); - assertThat(formula.getOperator(), instanceOf(UnaryOperator.class)); - assertEquals(formula.getOperator(), UnaryOperator.EXISTS_GLOBAL); - formula = parser.parse("#property AG False"); - assertEquals(formula.getSubFormulaCount(), 1); - assertThat(formula.getSubFormulaAt(0), instanceOf(Contradiction.class)); - assertThat(formula.getOperator(), instanceOf(UnaryOperator.class)); - assertEquals(formula.getOperator(), UnaryOperator.ALL_GLOBAL); - } - - @Test - public void binaryTemporalOperator() { - FormulaParser parser = new FormulaParser(); - Formula formula = parser.parse("#property E (True U False)"); - assertEquals(formula.getSubFormulaCount(), 2); - assertThat(formula.getSubFormulaAt(0), instanceOf(Tautology.class)); - assertThat(formula.getSubFormulaAt(1), instanceOf(Contradiction.class)); - assertThat(formula.getOperator(), instanceOf(BinaryOperator.class)); - assertEquals(formula.getOperator(), BinaryOperator.EXISTS_UNTIL); - formula = parser.parse("#property A (True U False)"); - assertEquals(formula.getSubFormulaCount(), 2); - assertThat(formula.getSubFormulaAt(0), instanceOf(Tautology.class)); - assertThat(formula.getSubFormulaAt(1), instanceOf(Contradiction.class)); - assertThat(formula.getOperator(), instanceOf(BinaryOperator.class)); - assertEquals(formula.getOperator(), BinaryOperator.ALL_UNTIL); - } - - @Test - public void booleanOperatorTest() { - FormulaParser parser = new FormulaParser(); - Formula formula = parser.parse("#property ! False"); - assertEquals(formula.getSubFormulaCount(), 1); - assertThat(formula.getSubFormulaAt(0), instanceOf(Contradiction.class)); - assertThat(formula.getOperator(), instanceOf(UnaryOperator.class)); - assertEquals(formula.getOperator(), UnaryOperator.NEGATION); - formula = parser.parse("#property (True && False)"); - assertEquals(formula.getSubFormulaCount(), 2); - assertThat(formula.getSubFormulaAt(0), instanceOf(Tautology.class)); - assertThat(formula.getSubFormulaAt(1), instanceOf(Contradiction.class)); - assertThat(formula.getOperator(), instanceOf(BinaryOperator.class)); - assertEquals(formula.getOperator(), BinaryOperator.AND); - formula = parser.parse("#property (True || False)"); - assertEquals(formula.getSubFormulaCount(), 2); - assertThat(formula.getSubFormulaAt(0), instanceOf(Tautology.class)); - assertThat(formula.getSubFormulaAt(1), instanceOf(Contradiction.class)); - assertThat(formula.getOperator(), instanceOf(BinaryOperator.class)); - assertEquals(formula.getOperator(), BinaryOperator.OR); - formula = parser.parse("#property (True => False)"); - assertEquals(formula.getSubFormulaCount(), 2); - assertThat(formula.getSubFormulaAt(0), instanceOf(Tautology.class)); - assertThat(formula.getSubFormulaAt(1), instanceOf(Contradiction.class)); - assertThat(formula.getOperator(), instanceOf(BinaryOperator.class)); - assertEquals(formula.getOperator(), BinaryOperator.IMPLICATION); - formula = parser.parse("#property (True <=> False)"); - assertEquals(formula.getSubFormulaCount(), 2); - assertThat(formula.getSubFormulaAt(0), instanceOf(Tautology.class)); - assertThat(formula.getSubFormulaAt(1), instanceOf(Contradiction.class)); - assertThat(formula.getOperator(), instanceOf(BinaryOperator.class)); - assertEquals(formula.getOperator(), BinaryOperator.EQUIVALENCE); - } - - @Test - public void complexTest() { - FormulaParser parser = new FormulaParser(); - Formula formula = parser.parse("" + - "#define first XY < 2.7 \n" + - "#define second aBx >= -0.01 \t \t \n" + - "#define Third zZ != 41234.45 \n" + - "#property E ( AF EX AG (first => True) U ( EF Third <=> A ( False U second ) ) ) "); - assertEquals(formula.getSubFormulaCount(), 2); - assertEquals(formula.getOperator(), BinaryOperator.EXISTS_UNTIL); - Formula af = formula.getSubFormulaAt(0); - assertEquals(af.getSubFormulaCount(), 1); - assertEquals(af.getOperator(), UnaryOperator.ALL_FUTURE); - Formula ex = af.getSubFormulaAt(0); - assertEquals(ex.getSubFormulaCount(), 1); - assertEquals(ex.getOperator(), UnaryOperator.EXISTS_NEXT); - Formula ag = ex.getSubFormulaAt(0); - assertEquals(ag.getSubFormulaCount(), 1); - assertEquals(ag.getOperator(), UnaryOperator.ALL_GLOBAL); - Formula impl = ag.getSubFormulaAt(0); - assertEquals(impl.getSubFormulaCount(), 2); - assertEquals(impl.getOperator(), BinaryOperator.IMPLICATION); - assertThat(impl.getSubFormulaAt(0), instanceOf(FloatProposition.class)); - assertThat(impl.getSubFormulaAt(1), instanceOf(Tautology.class)); - FloatProposition first = (FloatProposition) impl.getSubFormulaAt(0); - assertEquals(first.getVariable(), "XY"); - assertEquals(first.getThreshold(), 2.7, TOLERANCE); - Formula equiv = formula.getSubFormulaAt(1); - assertEquals(equiv.getSubFormulaCount(), 2); - assertEquals(equiv.getOperator(), BinaryOperator.EQUIVALENCE); - Formula ef = equiv.getSubFormulaAt(0); - assertEquals(ef.getSubFormulaCount(), 1); - assertEquals(ef.getOperator(), UnaryOperator.EXISTS_FUTURE); - assertThat(ef.getSubFormulaAt(0), instanceOf(FloatProposition.class)); - FloatProposition third = (FloatProposition) ef.getSubFormulaAt(0); - assertEquals(third.getVariable(), "zZ"); - assertEquals(third.getThreshold(), 41234.45, TOLERANCE); - Formula au = equiv.getSubFormulaAt(1); - assertEquals(au.getSubFormulaCount(), 2); - assertEquals(au.getOperator(), BinaryOperator.ALL_UNTIL); - assertThat(au.getSubFormulaAt(0), instanceOf(Contradiction.class)); - assertThat(au.getSubFormulaAt(1), instanceOf(FloatProposition.class)); - FloatProposition second = (FloatProposition) au.getSubFormulaAt(1); - assertEquals(second.getVariable(), "aBx"); - assertEquals(second.getThreshold(), -0.01, TOLERANCE); - } - - @Test - public void whitespaceTest() { - FormulaParser parser = new FormulaParser(); - Formula formula = parser.parse("\t \n \n#define\t\ta\nx < \t \n 1.0\n#define\n\n\nb x\t>2.0 #property \t\t E( a U \tb )\n\n\t"); - assertEquals(formula.getOperator(), BinaryOperator.EXISTS_UNTIL); - assertEquals(formula.getSubFormulaCount(), 2); - assertThat(formula.getSubFormulaAt(0), instanceOf(FloatProposition.class)); - assertThat(formula.getSubFormulaAt(1), instanceOf(FloatProposition.class)); - FloatProposition a = (FloatProposition) formula.getSubFormulaAt(0); - FloatProposition b = (FloatProposition) formula.getSubFormulaAt(1); - assertEquals(a.getVariable(), "x"); - assertEquals(b.getVariable(), "x"); - assertEquals(a.getThreshold(), 1.0, TOLERANCE); - assertEquals(b.getThreshold(), 2.0, TOLERANCE); - } - - @Test - public void realLifeTest() { - FormulaParser parser = new FormulaParser(); - Formula formula = parser.parse( "#define a x < 4.9 \n" + - "#define b x > 5.1 \n" + - "#property ( EF AG a && EF AG b )" - ); - assertEquals(formula.getSubFormulaCount(), 2); - assertEquals(formula.getOperator(), BinaryOperator.AND); - Formula ef1 = formula.getSubFormulaAt(0); - Formula ef2 = formula.getSubFormulaAt(1); - assertEquals(ef1.getOperator(), UnaryOperator.EXISTS_FUTURE); - assertEquals(ef2.getOperator(), UnaryOperator.EXISTS_FUTURE); - Formula ag1 = ef1.getSubFormulaAt(0); - Formula ag2 = ef2.getSubFormulaAt(0); - assertEquals(ag1.getOperator(), UnaryOperator.ALL_GLOBAL); - assertEquals(ag2.getOperator(), UnaryOperator.ALL_GLOBAL); - Formula aF = ag1.getSubFormulaAt(0); - Formula bF = ag2.getSubFormulaAt(0); - assertThat(aF, instanceOf(FloatProposition.class)); - assertThat(bF, instanceOf(FloatProposition.class)); - FloatProposition a = (FloatProposition) aF; - FloatProposition b = (FloatProposition) bF; - assertEquals(a.getVariable(), "x"); - assertEquals(b.getVariable(), "x"); - assertEquals(a.getThreshold(), 4.9, TOLERANCE); - assertEquals(b.getThreshold(), 5.1, TOLERANCE); - } - -} diff --git a/src/test/kotlin/cz/muni/fi/ctl/FormulasTest.kt b/src/test/kotlin/cz/muni/fi/ctl/FormulasTest.kt new file mode 100644 index 0000000..a1ea973 --- /dev/null +++ b/src/test/kotlin/cz/muni/fi/ctl/FormulasTest.kt @@ -0,0 +1,97 @@ +package cz.muni.fi.ctl + +import org.junit.Test +import kotlin.test.assertEquals +import kotlin.test.assertFailsWith + +class MapTest { + + val formula = EX( True EU ( + FloatProposition("var", FloatOp.EQ, 13.3) + or + DirectionProposition("val", Direction.IN, Facet.NEGATIVE) + ) + ) + + @Test fun treeMapId() { + + assertEquals(formula, formula.treeMap { it }) + + } + + @Test fun treeMapPropositions() { + + formula.treeMap { + if (it.operator.cardinality == 0) throw IllegalStateException("Executing tree map on a leaf") + else it + } + } + + @Test fun treeMapComplex() { + + fun transform(f: Formula): Formula = when(f.operator) { + Op.EXISTS_NEXT -> FormulaImpl(Op.ALL_NEXT, f.subFormulas.map(::transform)) + Op.EXISTS_UNTIL -> FormulaImpl(Op.ALL_UNTIL, f.subFormulas.map(::transform)) + Op.OR -> FormulaImpl(Op.AND, f.subFormulas.map(::transform)) + else -> f.treeMap(::transform) + } + + assertEquals( + AX( True AU ( + FloatProposition("var", FloatOp.EQ, 13.3) + and + DirectionProposition("val", Direction.IN, Facet.NEGATIVE) + ) + ), transform(formula)) + + } + +} + +class Misc { + + @Test fun booleanToString() { + assertEquals("True", True.toString()) + assertEquals("False", False.toString()) + } + + @Test fun formulaToString() { + assertEquals("(True && EX (False EU True))", (True and EX(False EU True)).toString()) + } + + @Test fun floatToString() { + assertEquals("prop > 5.3", FloatProposition("prop", FloatOp.GT, 5.3).toString()) + } + + @Test fun directionToString() { + assertEquals("prop:in+", DirectionProposition("prop", Direction.IN, Facet.POSITIVE).toString()) + } + + @Test fun emptyFormula() { + assertEquals("null([])",FormulaImpl().toString()) + } + + @Test fun notEnoughFormulas() { + assertFailsWith(IllegalArgumentException::class) { + FormulaImpl(Op.ALL_UNTIL, True) + } + } + + @Test fun tooManyFormulas() { + assertFailsWith(IllegalArgumentException::class) { + FormulaImpl(Op.ALL_UNTIL, True, False, Atom()) + } + } + + @Test fun get() { + val float = FloatProposition("val", FloatOp.GT, 34.12) + assertEquals("val", float.variable) + assertEquals(FloatOp.GT, float.floatOp) + assertEquals(34.12, float.value) + val dir = DirectionProposition("var", Direction.IN, Facet.NEGATIVE) + assertEquals("var", dir.variable) + assertEquals(Direction.IN, dir.direction) + assertEquals(Facet.NEGATIVE, dir.facet) + } + +} \ No newline at end of file diff --git a/src/test/kotlin/cz/muni/fi/ctl/IntegrationTest.kt b/src/test/kotlin/cz/muni/fi/ctl/IntegrationTest.kt new file mode 100644 index 0000000..ca318e1 --- /dev/null +++ b/src/test/kotlin/cz/muni/fi/ctl/IntegrationTest.kt @@ -0,0 +1,81 @@ +package cz.muni.fi.ctl + +import org.junit.Test +import java.io.File +import kotlin.test.assertEquals + +/** + * Consider this an example of usage + */ +class Integration { + + @Test fun test() { + + val f1 = File.createTempFile("file", ".ctl") + + val parser = Parser() + val normalizer = Normalizer() + val optimizer = Optimizer() + + f1.bufferedWriter().use { + it.write("c = p2 > 3.14 <=> False \n") + it.write("pop = True EU c EU a \n") + } + + val formulas = parser.parse( + "#include \"${ f1.absolutePath }\" \n" + + """ + a = True && p1:out+ + f = EF True && EG pop || AX a + """) + + val p1 = DirectionProposition("p1", Direction.OUT, Facet.POSITIVE) + val p2 = FloatProposition("p2", FloatOp.GT, 3.14) + val np2 = FloatProposition("p2", FloatOp.LT_EQ, 3.14) + + val a = True and p1 + val c = p2 equal False + val pop = True EU (c EU a) + val f = (EF(True) and EG(pop)) or AX(a) + + assertEquals(4, formulas.size()) + assertEquals(a, formulas["a"]) + assertEquals(c, formulas["c"]) + assertEquals(pop, formulas["pop"]) + assertEquals(f, formulas["f"]) + + val normalized = normalizer.normalize(f) + + assertEquals( + ( + (True EU True) //EF + and + not(True AU not( //EG + True + EU + ( + ((p2 and False) or (not(p2) and not(False))) //<=> + EU + (True and p1) + ) + )) + ) + or + not(EX(not(True and p1))), //AX + normalized + ) + + val optimized = optimizer.optimize(normalized) + + assertEquals( + not( + True AU not(True EU (np2 EU p1)) + and + EX(not(p1)) + ), + optimized + ) + + } + +} \ No newline at end of file diff --git a/src/test/kotlin/cz/muni/fi/ctl/NormalizerTest.kt b/src/test/kotlin/cz/muni/fi/ctl/NormalizerTest.kt new file mode 100644 index 0000000..bfddc0c --- /dev/null +++ b/src/test/kotlin/cz/muni/fi/ctl/NormalizerTest.kt @@ -0,0 +1,143 @@ +package cz.muni.fi.ctl + +import org.junit.Test +import kotlin.test.assertEquals + +class UntilNormalFormTest { + + val p1 = Reference("p1") + val p2 = Reference("p2") + val p3 = Reference("p3") + val p4 = Reference("p4") + + val normalizer = Normalizer() + + @Test fun complexTest() { + + val f1 = FloatProposition("var1", FloatOp.NEQ, 14.3) + val f2 = FloatProposition("var2", FloatOp.LT, -15.3) + val d1 = DirectionProposition("var1", Direction.IN, Facet.NEGATIVE) + val d2 = DirectionProposition("var2", Direction.OUT, Facet.POSITIVE) + + val prop = EF( AF((EX(f1) AU False) equal not(d2)) implies AX( EG(f2) EU AG(d1))) + assertEquals( + True EU + (not( True AU ((EX(f1) AU False and not(d2)) or (not(EX(f1) AU False) and not(not(d2))))) + or + not( EX( not( (not( True AU not(f2))) EU (not( True EU not(d1))) )))), + normalizer.normalize(prop) + ) + } + + @Test fun nestingNoPropositions() { + val prop = EF( p1 implies AX( EG(p2) EU AG(p1))) + assertEquals( + True EU (not(p1) or not( EX( not( (not( True AU not(p2))) EU (not( True EU not(p1))) )))), + normalizer.normalize(prop) + ) + } + + @Test fun nestingPreserve() { + val prop = (p1 and EX(not(p2))) EU ( not(p3) AU (p4 or p2)) + assertEquals(prop, normalizer.normalize(prop)) + } + + //trivial cases + + @Test fun equivChange() { + val prop = p1 equal p2 + val norm = normalizer.normalize(prop) + assertEquals( (p1 and p2) or (not(p1) and not(p2)), norm) + assertEquals(norm, normalizer.normalize(norm)) + } + + @Test fun implChange() { + val prop = p1 implies p2 + val norm = normalizer.normalize(prop) + assertEquals(not(p1) or p2, norm) + assertEquals(norm, normalizer.normalize(norm)) + } + + @Test fun agChange() { + val prop = AG(p1) + val norm = normalizer.normalize(prop) + assertEquals(not( True EU not(p1) ), norm) + assertEquals(norm, normalizer.normalize(norm)) + } + + @Test fun egChange() { + val prop = EG(p1) + val norm = normalizer.normalize(prop) + assertEquals(not( True AU not(p1) ), norm) + assertEquals(norm, normalizer.normalize(norm)) + } + + @Test fun afChange() { + val prop = AF(p1) + val norm = normalizer.normalize(prop) + assertEquals(True AU p1, norm) + assertEquals(norm, normalizer.normalize(norm)) + } + + @Test fun efChange() { + val prop = EF(p1) + val norm = normalizer.normalize(prop) + assertEquals(True EU p1, norm) + assertEquals(norm, normalizer.normalize(norm)) + } + + @Test fun axChange() { + val prop = AX(p1) + val norm = normalizer.normalize(prop) + assertEquals(not( EX( not(p1) ) ), norm) + assertEquals(norm, normalizer.normalize(norm)) + } + + @Test fun auPreserve() { + val prop = p1 AU p2 + assertEquals(prop, normalizer.normalize(prop)) + } + + @Test fun euPreserve() { + val prop = p1 EU p2 + assertEquals(prop, normalizer.normalize(prop)) + } + + @Test fun orPreserve() { + val prop = p1 or p2 + assertEquals(prop, normalizer.normalize(prop)) + } + + @Test fun andPreserve() { + val prop = p1 and p2 + assertEquals(prop, normalizer.normalize(prop)) + } + + @Test fun negPreserve() { + val prop = not(p1) + assertEquals(prop, normalizer.normalize(prop)) + } + + @Test fun exPreserve() { + val prop = EX(p1) + assertEquals(prop, normalizer.normalize(prop)) + } + + @Test fun floatPreserve() { + val prop = FloatProposition("val", FloatOp.GT_EQ, 32.2) + assertEquals(prop, normalizer.normalize(prop)) + } + + @Test fun booleanPreserve() { + assertEquals(True, normalizer.normalize(True)) + assertEquals(False, normalizer.normalize(False)) + } + + @Test fun directionPreserve() { + val prop = DirectionProposition("var", Direction.IN, Facet.POSITIVE) + assertEquals(prop, normalizer.normalize(prop)) + } + + + +} \ No newline at end of file diff --git a/src/test/kotlin/cz/muni/fi/ctl/OptimizerTest.kt b/src/test/kotlin/cz/muni/fi/ctl/OptimizerTest.kt new file mode 100644 index 0000000..2bbd484 --- /dev/null +++ b/src/test/kotlin/cz/muni/fi/ctl/OptimizerTest.kt @@ -0,0 +1,78 @@ +package cz.muni.fi.ctl + +import org.junit.Test +import kotlin.test.assertEquals + +class OptimizerTest { + + val p1 = Reference("p1") + val p2 = Reference("p2") + + val optimizer = Optimizer() + + @Test fun complexTest() { + val f1 = FloatProposition("var2", FloatOp.LT_EQ, -15.3) + val nf1 = FloatProposition("var2", FloatOp.GT, -15.3) + val d1 = DirectionProposition("var1", Direction.IN, Facet.NEGATIVE) + + val prop = p1 AU EX(not(f1) EU not(True and ( not(d1) or (p1 AU False)))) + val optimized = optimizer.optimize(prop) + + assertEquals(p1 AU EX(nf1 EU d1), optimized) + assertEquals(optimized, optimizer.optimize(optimized)) + } + + @Test fun orNegation() { + assertEquals(not(p1 and p2), optimizer.optimize(not(p1) or not(p2))) + } + + @Test fun andNegation() { + assertEquals(not(p1 or p2), optimizer.optimize(not(p1) and not(p2))) + } + + @Test fun floatNegation() { + assertEquals( + FloatProposition("val", FloatOp.NEQ, 13.2), + optimizer.optimize( + not(FloatProposition("val", FloatOp.EQ, 13.2)) + ) + ) + assertEquals( + FloatProposition("val", FloatOp.LT_EQ, 13.2), + optimizer.optimize( + not(FloatProposition("val", FloatOp.GT, 13.2)) + ) + ) + } + + @Test fun doubleNegation() { + assertEquals(p1, optimizer.optimize(not(not(p1)))) + assertEquals(not(p2), optimizer.optimize(not(not(not(p2))))) + } + + @Test fun booleanReduction() { + val prop = EX( not(False) and ( (True or False) EU (False AU True) )) + assertEquals(True, optimizer.optimize(prop)) + } + + @Test fun preserveUnsupported() { + val prop = AX(EG(p1 implies p2)) + assertEquals(prop, optimizer.optimize(prop)) + } + + @Test fun floatPreserve() { + val prop = FloatProposition("val", FloatOp.GT_EQ, 32.2) + assertEquals(prop, optimizer.optimize(prop)) + } + + @Test fun booleanPreserve() { + assertEquals(True, optimizer.optimize(True)) + assertEquals(False, optimizer.optimize(False)) + } + + @Test fun directionPreserve() { + val prop = DirectionProposition("var", Direction.IN, Facet.POSITIVE) + assertEquals(prop, optimizer.optimize(prop)) + } + +} \ No newline at end of file diff --git a/src/test/kotlin/cz/muni/fi/ctl/ParserBasicTest.kt b/src/test/kotlin/cz/muni/fi/ctl/ParserBasicTest.kt new file mode 100644 index 0000000..8dcb29b --- /dev/null +++ b/src/test/kotlin/cz/muni/fi/ctl/ParserBasicTest.kt @@ -0,0 +1,134 @@ +package cz.muni.fi.ctl + +import org.junit.Test +import kotlin.test.assertEquals + +class Basic { + + val parser = Parser() + + @Test fun parenthesis() { + assertEquals( + True, + parser.formula("(True)") + ) + } + + @Test fun binaryOps() { + assertEquals( + True EU False, + parser.formula("True EU False") + ) + assertEquals( + True AU False, + parser.formula("True AU False") + ) + assertEquals( + True and False, + parser.formula("True && False") + ) + assertEquals( + True or False, + parser.formula("True || False") + ) + assertEquals( + True implies False, + parser.formula("True => False") + ) + assertEquals( + True equal False, + parser.formula("True <=> False") + ) + } + + @Test fun unaryOps() { + assertEquals( + not(True), + parser.formula("!True") + ) + assertEquals( + EX(True), + parser.formula("EX True") + ) + assertEquals( + AX(True), + parser.formula("AX True") + ) + assertEquals( + EF(True), + parser.formula("EF True") + ) + assertEquals( + AF(True), + parser.formula("AF True") + ) + assertEquals( + EG(True), + parser.formula("EG True") + ) + assertEquals( + AG(True), + parser.formula("AG True") + ) + } + + @Test fun floats() { + assertEquals( + FloatProposition("var", FloatOp.EQ, 0.0), + parser.formula("var == 0") + ) + assertEquals( + FloatProposition("var", FloatOp.EQ, 1.0), + parser.formula("var == 1") + ) + assertEquals( + FloatProposition("var", FloatOp.NEQ, -1.0), + parser.formula("var != -1") + ) + assertEquals( + FloatProposition("var", FloatOp.GT, 0.158), + parser.formula("var > 0.158") + ) + assertEquals( + FloatProposition("var", FloatOp.GT_EQ, -0.9995), + parser.formula("var >= -0.9995") + ) + assertEquals( + FloatProposition("var", FloatOp.LT, 1040.58), + parser.formula("var < 1040.58") + ) + assertEquals( + FloatProposition("var", FloatOp.LT_EQ, -586.44), + parser.formula("var <= -586.44") + ) + } + + @Test fun directions() { + assertEquals( + DirectionProposition("var", Direction.IN, Facet.POSITIVE), + parser.formula("var:in+") + ) + assertEquals( + DirectionProposition("var", Direction.OUT, Facet.POSITIVE), + parser.formula("var:out+") + ) + assertEquals( + DirectionProposition("var", Direction.IN, Facet.NEGATIVE), + parser.formula("var:in-") + ) + assertEquals( + DirectionProposition("var", Direction.OUT, Facet.NEGATIVE), + parser.formula("var:out-") + ) + } + + @Test fun booleans() { + assertEquals(True, parser.formula("true")) + assertEquals(True, parser.formula("True")) + assertEquals(True, parser.formula("tt")) + assertEquals(False, parser.formula("false")) + assertEquals(False, parser.formula("False")) + assertEquals(False, parser.formula("ff")) + } + +} \ No newline at end of file diff --git a/src/test/kotlin/cz/muni/fi/ctl/ParserComplexTest.kt b/src/test/kotlin/cz/muni/fi/ctl/ParserComplexTest.kt new file mode 100644 index 0000000..45be4c4 --- /dev/null +++ b/src/test/kotlin/cz/muni/fi/ctl/ParserComplexTest.kt @@ -0,0 +1,131 @@ +package cz.muni.fi.ctl + +import org.junit.Test +import java.io.File +import kotlin.test.assertEquals + +class Complex { + + val parser = Parser() + + + val p1 = FloatProposition("p1", FloatOp.EQ, 4.0) + val p2 = DirectionProposition("p2", Direction.IN, Facet.NEGATIVE) + val p3 = FloatProposition("p3", FloatOp.LT, -3.14) + + @Test fun complexFiles() { + + val f1 = File.createTempFile("file", ".ctl") + val f2 = File.createTempFile("file2", ".ctl") + val f3 = File.createTempFile("file3", ".ctl") + + f1.bufferedWriter().use { + it.write("c = p2:in- || EX p3 < -3.14 EU a") + } + + f2.bufferedWriter().use { + it.write("#include \"${ f1.absolutePath }\" \n") + it.write("b = EX c <=> True \n") + it.write("d = e => e") + } + + f3.bufferedWriter().use { + it.write("a = ! p1 == 4 \n") + it.write("#include \"${ f2.absolutePath }\" \n") + it.write("e = True && c || c && False") + } + + val result = parser.parse(f3) + + val a = not(p1) + val c = (p2 or EX(p3)) EU a + val b = EX(c) equal True + val e = (True and c) or (c and False) + val d = e implies e + + assertEquals(5, result.size()) + assertEquals(a, result["a"]) + assertEquals(b, result["b"]) + assertEquals(c, result["c"]) + assertEquals(d, result["d"]) + assertEquals(e, result["e"]) + + f1.delete() + f2.delete() + f3.delete() + + } + + @Test fun complexString() { + + val result = parser.parse(""" + b = EX p3 < -3.14 EU a + a = (p1 == 4) && p2:in- + d = AG AX c + c = b <=> b + e = c && True || False && b + """) + + val a = p1 and p2 + val b = EX(p3) EU a + val c = b equal b + val d = AG(AX(c)) + val e = (c and True) or (False and b) + + assertEquals(5, result.size()) + assertEquals(a, result["a"]) + assertEquals(b, result["b"]) + assertEquals(c, result["c"]) + assertEquals(d, result["d"]) + assertEquals(e, result["e"]) + + } + + @Test fun operatorAssociativity() { + //These binary operators are by convention right-associative + //Other binary operators, such as &&, ||, <=> are associative, + //so it doesn't matter if we resolve them left to right or right to left + assertEquals( + True EU (False EU True), + parser.formula("True EU False EU True") + ) + assertEquals( + True AU (False AU True), + parser.formula("True AU False AU True") + ) + assertEquals( + True implies (False implies True), + parser.formula("True => False => True") + ) + } + + @Test fun operatorPriority() { + //we do not test every combination, since priority should be transitive + assertEquals( + not(False) and not(True), + parser.formula("!False && !True") + ) + assertEquals( + (True and False) or (False and True), + parser.formula("True && False || False && True") + ) + assertEquals( + (True or False) implies (False or True), + parser.formula("True || False => False || True") + ) + assertEquals( + (True implies False) equal (False implies True), + parser.formula("True => False <=> False => True") + ) + assertEquals( + (True equal False) EU (False equal True), + parser.formula("True <=> False EU False <=> True") + ) + assertEquals( + (True EU False) AU (False EU True), + parser.formula("True EU False AU False EU True") + ) + } + +} + diff --git a/src/test/kotlin/cz/muni/fi/ctl/ParserIncludeTest.kt b/src/test/kotlin/cz/muni/fi/ctl/ParserIncludeTest.kt new file mode 100644 index 0000000..2ae66c6 --- /dev/null +++ b/src/test/kotlin/cz/muni/fi/ctl/ParserIncludeTest.kt @@ -0,0 +1,110 @@ +package cz.muni.fi.ctl + +import org.junit.Test +import java.io.File +import java.io.FileNotFoundException +import kotlin.test.assertEquals +import kotlin.test.assertFailsWith + +class Includes { + + val parser = Parser() + + @Test fun invalidInclude() { + assertFailsWith(FileNotFoundException::class) { + parser.parse("#include \"bogus.foo\" ") + } + } + + @Test fun duplicateInclude() { + + val i1 = File.createTempFile("include1", ".ctl") + val i2 = File.createTempFile("include2", ".ctl") + + i1.bufferedWriter().use { + it.write("val = True \n") + it.write("#include \"${ i1.absolutePath }\"") + } + i2.bufferedWriter().use { + it.write("#include \"${ i1.absolutePath }\" \n") + it.write("#include \"${ i2.absolutePath }\" \n") + it.write("val2 = False") + } + + val result = parser.parse( + "#include \"${ i2.absolutePath }\" \n" + + "#include \"${ i1.absolutePath }\" " + ) + + assertEquals(2, result.size()) + assertEquals(True, result["val"]) + assertEquals(False, result["val2"]) + + i1.delete() + i2.delete() + + } + + @Test fun transitiveInclude() { + + val i1 = File.createTempFile("include1", ".ctl") + val i2 = File.createTempFile("include2", ".ctl") + + i1.bufferedWriter().use { + it.write("val = True") + } + i2.bufferedWriter().use { + it.write("#include \"${ i1.absolutePath }\"") + } + + val result = parser.parse("#include \"${ i2.absolutePath }\"") + + assertEquals(1, result.size()) + assertEquals(True, result["val"]) + + i1.delete() + i2.delete() + + } + + @Test fun simpleIncludeFromFile() { + + val include = File.createTempFile("simpleInclude", ".ctl") + + include.bufferedWriter().use { + it.write("val = True") + } + + val file = File.createTempFile("simpleFile", ".ctl") + file.bufferedWriter().use { + it.write("#include \"${ include.absolutePath }\"") + } + + val result = parser.parse(file) + + assertEquals(1, result.size()) + assertEquals(True, result["val"]) + + file.delete() + include.delete() + } + + @Test fun simpleIncludeFromString() { + + val file = File.createTempFile("simpleInclude", ".ctl") + + file.bufferedWriter().use { + it.write("val = True") + } + + val result = parser.parse( + "#include \"${ file.absolutePath }\"" + ) + + assertEquals(1, result.size()) + assertEquals(True, result["val"]) + + file.delete() + } + +} diff --git a/src/test/kotlin/cz/muni/fi/ctl/ParserReferencesTest.kt b/src/test/kotlin/cz/muni/fi/ctl/ParserReferencesTest.kt new file mode 100644 index 0000000..cc0f71f --- /dev/null +++ b/src/test/kotlin/cz/muni/fi/ctl/ParserReferencesTest.kt @@ -0,0 +1,171 @@ +package cz.muni.fi.ctl + +import org.junit.Test +import java.io.File +import kotlin.test.assertEquals +import kotlin.test.assertFailsWith + +class References { + + val parser = Parser() + + @Test fun cyclicReferenceThroughFiles() { + val file = File.createTempFile("file", ".ctx") + + file.bufferedWriter().use { + it.write("k = m") + } + + assertFailsWith(IllegalStateException::class) { + parser.parse(""" + m = !k + """) + } + file.delete() + } + + @Test fun transitiveCyclicReference() { + assertFailsWith(IllegalStateException::class) { + parser.parse(""" + k = EX l + l = AX m + m = ! k + """) + } + } + + @Test fun simpleCyclicReference() { + assertFailsWith(IllegalStateException::class) { + parser.parse("k = !k") + } + } + + @Test fun undefinedReference() { + assertFailsWith(IllegalStateException::class) { + parser.parse("k = EF m") + } + } + + @Test fun declarationOrderIndependence() { + + val result = parser.parse(""" + k = ! m + m = True + """) + + assertEquals(2, result.size()) + assertEquals(not(True), result["k"]) + assertEquals(True, result["m"]) + + } + + @Test fun duplicateDeclarationInFiles() { + + val i1 = File.createTempFile("include1", ".ctl") + + i1.bufferedWriter().use { + it.write("k = True") + } + + assertFailsWith(IllegalStateException::class) { + parser.parse( + "#include \"${ i1.absolutePath }\" \n" + + "k = False" + ) + } + + i1.delete() + } + + @Test fun duplicateDeclarationInString() { + assertFailsWith(IllegalStateException::class) { + parser.parse(""" + k = True + l = False + k = False + """) + } + } + + @Test fun transitiveResolveInFiles() { + + val i1 = File.createTempFile("include1", ".ctl") + val i2 = File.createTempFile("include2", ".ctl") + + i1.bufferedWriter().use { + it.write("k = True") + } + i2.bufferedWriter().use { + it.write("l = EF k") + } + + val result = parser.parse( + "m = !l \n" + + "#include \"${ i1.absolutePath }\" \n" + + "#include \"${ i2.absolutePath }\" \n" + ) + + assertEquals(3, result.size()) + assertEquals(True, result["k"]) + assertEquals(EF(True), result["l"]) + assertEquals(not(EF(True)), result["m"]) + + } + + @Test fun transitiveResolveInString() { + + val result = parser.parse(""" + k = True + l = EF k + m = !l + """) + + assertEquals(3, result.size()) + assertEquals(True, result["k"]) + assertEquals(EF(True), result["l"]) + assertEquals(not(EF(True)), result["m"]) + + } + + @Test fun simpleResolveInInclude() { + + val i = File.createTempFile("include", ".ctl") + + i.bufferedWriter().use { + it.write("val = False") + } + + val result = parser.parse( + "k = !val \n " + + "#include \"${ i.absolutePath }\" \n" + ) + + assertEquals(2, result.size()) + assertEquals(False, result["val"]) + assertEquals(not(False), result["k"]) + + i.delete() + + } + + @Test fun simpleResolveInString() { + val result = parser.parse(""" + k = True + l = !k + """) + assertEquals(2, result.size()) + assertEquals(True, result["k"]) + assertEquals(not(True), result["l"]) + } + + @Test fun aliasInString() { + val result = parser.parse(""" + k = True + l = k + """) + assertEquals(2, result.size()) + assertEquals(True, result["k"]) + assertEquals(True, result["l"]) + } + +} \ No newline at end of file