Code Monkey home page Code Monkey logo

ltlverif's People

Contributors

mondokm avatar radl97 avatar

Forkers

radl97 ripplb

ltlverif's Issues

Multiedge CFA - name collision in generated locations

If you define an edge with multiple stmts, the CFA is split in CfaEdgeDefinition.java, but the intermediate generated locations all have a name of empty string.
This can collide later as something asserts that location names are unique. I've found the bug using this project, but maybe the error is not here.

I have a test that fails without this patch, but runs fine when applied:

diff --git a/subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/dsl/CfaEdgeDefinition.java b/subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/dsl/CfaEdgeDefinition.java
index e1551039a..cff703735 100644
--- a/subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/dsl/CfaEdgeDefinition.java
+++ b/subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/dsl/CfaEdgeDefinition.java
@@ -49,6 +49,8 @@ final class CfaEdgeDefinition {

        ////

+       private static int counter = 0;
+
        public List<Edge> instantiate(final CFA.Builder cfa, final Env env) {
                final CfaLocationSymbol sourceSymbol = (CfaLocationSymbol) scope.resolve(source).get();
                final CfaLocationSymbol targetSymbol = (CfaLocationSymbol) scope.resolve(target).get();
@@ -63,7 +65,7 @@ final class CfaEdgeDefinition {
                final List<Loc> locs = new ArrayList<>(stmts.size() + 1);
                locs.add(sourceLoc);
                for (int i = 0; i < stmts.size() - 1; ++i) {
-                       locs.add(cfa.createLoc(""));
+                       locs.add(cfa.createLoc("Lgen" + ++counter));
                }
                locs.add(targetLoc);

Do you know anything in this lib that asserts location name uniqueness? @mondokm
If not, I'll move the discussion to the theta :)

Bad result

Note: the code has changed, that might be one source of the issue! The question is more of a "is the LTL in bad format?"

LTL: neither "FG (not err)" nor "XG (not err)" work as expected: both return "LTL Expression holds" for both CFAs below:

CFA files:
(changed from counter5_true.cfa)

main process cfa {
    var x : int
    var err : bool

    init loc IL1
    loc L0
    loc L1
    loc L2
    loc L3
    final loc END
    loc ERR
    error loc ERR1

    IL1 -> L0 { err := false }
    L0 -> L1 { x := 0 }
    L1 -> L2 { assume x < 5 }
    L1 -> L3 { assume not (x < 5) }
    L2 -> L1 { x := x + 1 }
    L3 -> END { assume x <= 5 }
    L3 -> ERR { assume not (x <= 5) }
    ERR -> ERR1 { err := true }
}

(changed from counter5_false.cfa)

main process cfa {
    var x : int
    var err : bool

    loc L0
    init loc IL1
    loc L1
    loc L2
    loc L3
    final loc END
    loc ERR
    error loc ERR1

    IL1 -> L0 { err := false }
    L0 -> L1 { x := 0 }
    L1 -> L2 { assume x < 5 }
    L1 -> L3 { assume not (x < 5) }
    L2 -> L1 { x := x + 1 }
    L3 -> END { assume x <= 5 }
    L3 -> ERR { assume not (x <= 5) }
    ERR -> ERR1 { err := true }
}

Workaround for Antlr bug

Antlr issue: antlr/antlr4#2016

Work around is a small patch to the grammar:

binaryLtlExpr:
    ltlExpr |
    op1=binaryLtlExpr type=binaryLtlOp op2=binaryLtlExpr;

from the original one:

binaryLtlExpr:
    ltlExpr |
    ops+=binaryLtlExpr type=binaryLtlOp ops+=binaryLtlExpr;

The visitor must be patched too: ctx.ops.get(0) will become ctx.op1 in ToStringVisitor.java. Same goes for ctx.ops.get(1).

Recommend Projects

  • React photo React

    A declarative, efficient, and flexible JavaScript library for building user interfaces.

  • Vue.js photo Vue.js

    🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.

  • Typescript photo Typescript

    TypeScript is a superset of JavaScript that compiles to clean JavaScript output.

  • TensorFlow photo TensorFlow

    An Open Source Machine Learning Framework for Everyone

  • Django photo Django

    The Web framework for perfectionists with deadlines.

  • D3 photo D3

    Bring data to life with SVG, Canvas and HTML. 📊📈🎉

Recommend Topics

  • javascript

    JavaScript (JS) is a lightweight interpreted programming language with first-class functions.

  • web

    Some thing interesting about web. New door for the world.

  • server

    A server is a program made to process requests and deliver data to clients.

  • Machine learning

    Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.

  • Game

    Some thing interesting about game, make everyone happy.

Recommend Org

  • Facebook photo Facebook

    We are working to build community through open source technology. NB: members must have two-factor auth.

  • Microsoft photo Microsoft

    Open source projects and samples from Microsoft.

  • Google photo Google

    Google ❤️ Open Source for everyone.

  • D3 photo D3

    Data-Driven Documents codes.