Skip to content

Commit

Permalink
Merge pull request #311 from RipplB/ltl2
Browse files Browse the repository at this point in the history 
LTL checking
  • Loading branch information
@mondokm
mondokm authored Jan 23, 2025
2 parents bd69e1c + c99d115 commit b513261
Show file tree
Hide file tree
Showing 1,667 changed files with 29,320 additions and 20,408 deletions.
4 changes: 2 additions & 2 deletions build.gradle.kts
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
/*
* Copyright 2024 Budapest University of Technology and Economics
* Copyright 2025 Budapest University of Technology and Economics
*
* Licensed under the Apache License, Version 2.0 (the "License");
* you may not use this file except in compliance with the License.
Expand Down Expand Up @@ -29,7 +29,7 @@ buildscript {

allprojects {
group = "hu.bme.mit.theta"
version = "6.8.6"
version = "6.9.0"

apply(from = rootDir.resolve("gradle/shared-with-buildSrc/mirrors.gradle.kts"))
}
Expand Down
2 changes: 1 addition & 1 deletion buildSrc/build.gradle.kts
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
/*
* Copyright 2024 Budapest University of Technology and Economics
* Copyright 2025 Budapest University of Technology and Economics
*
* Licensed under the Apache License, Version 2.0 (the "License");
* you may not use this file except in compliance with the License.
Expand Down
7 changes: 4 additions & 3 deletions buildSrc/gradle.properties
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
#
# Copyright 2024 Budapest University of Technology and Economics
# Copyright 2025 Budapest University of Technology and Economics
#
# Licensed under the Apache License, Version 2.0 (the "License");
# you may not use this file except in compliance with the License.
Expand All @@ -17,7 +17,7 @@
javaVersion=17
kotlinVersion=1.9.25
shadowVersion=7.1.2
antlrVersion=4.9.2
antlrVersion=4.12.0
guavaVersion=31.1-jre
jcommanderVersion=1.72
z3Version=4.5.0
Expand All @@ -41,4 +41,5 @@ javasmtVersion=4.1.1
sosylabVersion=0.3000-569-g89796f98
cliktVersion=4.4.0
spotlessVersion=6.25.0
kamlVersion=0.59.0
kamlVersion=0.59.0
nuprocessVersion=2.0.6
2 changes: 1 addition & 1 deletion buildSrc/settings.gradle.kts
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
/*
* Copyright 2024 Budapest University of Technology and Economics
* Copyright 2025 Budapest University of Technology and Economics
*
* Licensed under the Apache License, Version 2.0 (the "License");
* you may not use this file except in compliance with the License.
Expand Down
4 changes: 3 additions & 1 deletion buildSrc/src/main/kotlin/Deps.kt
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
/*
* Copyright 2024 Budapest University of Technology and Economics
* Copyright 2025 Budapest University of Technology and Economics
*
* Licensed under the Apache License, Version 2.0 (the "License");
* you may not use this file except in compliance with the License.
Expand Down Expand Up @@ -81,4 +81,6 @@ object Deps {
val clikt = "com.github.ajalt.clikt:clikt:${Versions.clikt}"

val kaml = "com.charleskorn.kaml:kaml:${Versions.kaml}"

val nuprocess = "com.zaxxer:nuprocess:${Versions.nuprocess}"
}
2 changes: 1 addition & 1 deletion buildSrc/src/main/kotlin/antlr-grammar.gradle.kts
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
/*
* Copyright 2024 Budapest University of Technology and Economics
* Copyright 2025 Budapest University of Technology and Economics
*
* Licensed under the Apache License, Version 2.0 (the "License");
* you may not use this file except in compliance with the License.
Expand Down
2 changes: 1 addition & 1 deletion buildSrc/src/main/kotlin/cli-tool.gradle.kts
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
/*
* Copyright 2024 Budapest University of Technology and Economics
* Copyright 2025 Budapest University of Technology and Economics
*
* Licensed under the Apache License, Version 2.0 (the "License");
* you may not use this file except in compliance with the License.
Expand Down
2 changes: 1 addition & 1 deletion buildSrc/src/main/kotlin/jacoco-common.gradle.kts
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
/*
* Copyright 2024 Budapest University of Technology and Economics
* Copyright 2025 Budapest University of Technology and Economics
*
* Licensed under the Apache License, Version 2.0 (the "License");
* you may not use this file except in compliance with the License.
Expand Down
2 changes: 1 addition & 1 deletion buildSrc/src/main/kotlin/java-common.gradle.kts
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
/*
* Copyright 2024 Budapest University of Technology and Economics
* Copyright 2025 Budapest University of Technology and Economics
*
* Licensed under the Apache License, Version 2.0 (the "License");
* you may not use this file except in compliance with the License.
Expand Down
4 changes: 2 additions & 2 deletions buildSrc/src/main/kotlin/kaml-serialization.gradle.kts
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
/*
* Copyright 2024 Budapest University of Technology and Economics
* Copyright 2025 Budapest University of Technology and Economics
*
* Licensed under the Apache License, Version 2.0 (the "License");
* you may not use this file except in compliance with the License.
Expand All @@ -17,7 +17,7 @@
import gradle.kotlin.dsl.accessors._07de9d51edfbede3e6fa517ade9dcf20.implementation

/*
* Copyright 2024 Budapest University of Technology and Economics
* Copyright 2025 Budapest University of Technology and Economics
*
* Licensed under the Apache License, Version 2.0 (the "License");
* you may not use this file except in compliance with the License.
Expand Down
2 changes: 1 addition & 1 deletion buildSrc/src/main/kotlin/kotlin-common.gradle.kts
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
/*
* Copyright 2024 Budapest University of Technology and Economics
* Copyright 2025 Budapest University of Technology and Economics
*
* Licensed under the Apache License, Version 2.0 (the "License");
* you may not use this file except in compliance with the License.
Expand Down
2 changes: 1 addition & 1 deletion buildSrc/src/main/kotlin/maven-artifact.gradle.kts
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
/*
* Copyright 2024 Budapest University of Technology and Economics
* Copyright 2025 Budapest University of Technology and Economics
*
* Licensed under the Apache License, Version 2.0 (the "License");
* you may not use this file except in compliance with the License.
Expand Down
2 changes: 1 addition & 1 deletion buildSrc/src/main/kotlin/tool-common.gradle.kts
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
/*
* Copyright 2024 Budapest University of Technology and Economics
* Copyright 2025 Budapest University of Technology and Economics
*
* Licensed under the Apache License, Version 2.0 (the "License");
* you may not use this file except in compliance with the License.
Expand Down
2 changes: 1 addition & 1 deletion gradle/shared-with-buildSrc/mirrors.gradle.kts
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
/*
* Copyright 2024 Budapest University of Technology and Economics
* Copyright 2025 Budapest University of Technology and Economics
*
* Licensed under the Apache License, Version 2.0 (the "License");
* you may not use this file except in compliance with the License.
Expand Down
Binary file added lib/jhoafparser-1.1.1.jar
View file
Binary file not shown.
2 changes: 1 addition & 1 deletion scripts/complex.kts
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
/*
* Copyright 2024 Budapest University of Technology and Economics
* Copyright 2025 Budapest University of Technology and Economics
*
* Licensed under the Apache License, Version 2.0 (the "License");
* you may not use this file except in compliance with the License.
Expand Down
2 changes: 1 addition & 1 deletion scripts/simple.kts
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
/*
* Copyright 2024 Budapest University of Technology and Economics
* Copyright 2025 Budapest University of Technology and Economics
*
* Licensed under the Apache License, Version 2.0 (the "License");
* you may not use this file except in compliance with the License.
Expand Down
4 changes: 3 additions & 1 deletion settings.gradle.kts
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
/*
* Copyright 2024 Budapest University of Technology and Economics
* Copyright 2025 Budapest University of Technology and Economics
*
* Licensed under the Apache License, Version 2.0 (the "License");
* you may not use this file except in compliance with the License.
Expand All @@ -21,6 +21,8 @@ include(
"common/core",
"common/grammar",
"common/multi-tests",
"common/ltl",
"common/ltl-cli",

"frontends/c-frontend",
"frontends/petrinet-frontend/petrinet-model",
Expand Down
2 changes: 1 addition & 1 deletion subprojects/cfa/cfa-analysis/build.gradle.kts
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
/*
* Copyright 2024 Budapest University of Technology and Economics
* Copyright 2025 Budapest University of Technology and Economics
*
* Licensed under the Apache License, Version 2.0 (the "License");
* you may not use this file except in compliance with the License.
Expand Down
14 changes: 7 additions & 7 deletions subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/CfaAction.java
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
/*
* Copyright 2024 Budapest University of Technology and Economics
* Copyright 2025 Budapest University of Technology and Economics
*
* Licensed under the Apache License, Version 2.0 (the "License");
* you may not use this file except in compliance with the License.
Expand All @@ -15,19 +15,18 @@
*/
package hu.bme.mit.theta.cfa.analysis;

import static com.google.common.base.Preconditions.checkArgument;
import static com.google.common.base.Preconditions.checkNotNull;

import hu.bme.mit.theta.analysis.expr.StmtAction;
import hu.bme.mit.theta.cfa.CFA.Edge;
import hu.bme.mit.theta.cfa.CFA.Loc;
import hu.bme.mit.theta.common.Utils;
import hu.bme.mit.theta.core.stmt.Stmt;

import java.util.Collections;
import java.util.List;
import java.util.stream.Collectors;

import static com.google.common.base.Preconditions.checkArgument;
import static com.google.common.base.Preconditions.checkNotNull;

public final class CfaAction extends StmtAction {

private final List<Edge> edges;
Expand All @@ -39,8 +38,9 @@ private CfaAction(final Loc source, final Loc target, final List<Edge> edges) {
this.source = checkNotNull(source);
this.target = checkNotNull(target);
this.edges = Collections.unmodifiableList(checkNotNull(edges));
this.stmts = Collections.unmodifiableList(
edges.stream().map(Edge::getStmt).collect(Collectors.toList()));
this.stmts =
Collections.unmodifiableList(
edges.stream().map(Edge::getStmt).collect(Collectors.toList()));
}

public static CfaAction create(final Edge edge) {
Expand Down
13 changes: 6 additions & 7 deletions subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/CfaAnalysis.java
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
/*
* Copyright 2024 Budapest University of Technology and Economics
* Copyright 2025 Budapest University of Technology and Economics
*
* Licensed under the Apache License, Version 2.0 (the "License");
* you may not use this file except in compliance with the License.
Expand All @@ -18,8 +18,8 @@
import static com.google.common.base.Preconditions.checkNotNull;

import hu.bme.mit.theta.analysis.Analysis;
import hu.bme.mit.theta.analysis.PartialOrd;
import hu.bme.mit.theta.analysis.InitFunc;
import hu.bme.mit.theta.analysis.PartialOrd;
import hu.bme.mit.theta.analysis.Prec;
import hu.bme.mit.theta.analysis.TransFunc;
import hu.bme.mit.theta.analysis.expr.ExprState;
Expand All @@ -32,17 +32,17 @@ public final class CfaAnalysis<S extends ExprState, P extends Prec>
private final InitFunc<CfaState<S>, CfaPrec<P>> initFunc;
private final TransFunc<CfaState<S>, CfaAction, CfaPrec<P>> transFunc;

private CfaAnalysis(final Loc initLoc,
final Analysis<S, ? super CfaAction, ? super P> analysis) {
private CfaAnalysis(
final Loc initLoc, final Analysis<S, ? super CfaAction, ? super P> analysis) {
checkNotNull(initLoc);
checkNotNull(analysis);
partialOrd = CfaOrd.create(analysis.getPartialOrd());
initFunc = CfaInitFunc.create(initLoc, analysis.getInitFunc());
transFunc = CfaTransFunc.create(analysis.getTransFunc());
}

public static <S extends ExprState, P extends Prec> CfaAnalysis<S, P> create(final Loc initLoc,
final Analysis<S, ? super CfaAction, ? super P> analysis) {
public static <S extends ExprState, P extends Prec> CfaAnalysis<S, P> create(
final Loc initLoc, final Analysis<S, ? super CfaAction, ? super P> analysis) {
return new CfaAnalysis<>(initLoc, analysis);
}

Expand All @@ -60,5 +60,4 @@ public InitFunc<CfaState<S>, CfaPrec<P>> getInitFunc() {
public TransFunc<CfaState<S>, CfaAction, CfaPrec<P>> getTransFunc() {
return transFunc;
}

}
16 changes: 7 additions & 9 deletions subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/CfaInitFunc.java
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
/*
* Copyright 2024 Budapest University of Technology and Economics
* Copyright 2025 Budapest University of Technology and Economics
*
* Licensed under the Apache License, Version 2.0 (the "License");
* you may not use this file except in compliance with the License.
Expand All @@ -15,18 +15,17 @@
*/
package hu.bme.mit.theta.cfa.analysis;

import static com.google.common.base.Preconditions.checkNotNull;

import hu.bme.mit.theta.analysis.InitFunc;
import hu.bme.mit.theta.analysis.Prec;
import hu.bme.mit.theta.analysis.expr.ExprState;
import hu.bme.mit.theta.cfa.CFA.Loc;

import java.util.ArrayList;
import java.util.Collection;

import static com.google.common.base.Preconditions.checkNotNull;

public final class CfaInitFunc<S extends ExprState, P extends Prec> implements
InitFunc<CfaState<S>, CfaPrec<P>> {
public final class CfaInitFunc<S extends ExprState, P extends Prec>
implements InitFunc<CfaState<S>, CfaPrec<P>> {

private final Loc initLoc;
private final InitFunc<S, ? super P> initFunc;
Expand All @@ -36,8 +35,8 @@ private CfaInitFunc(final Loc initLoc, final InitFunc<S, ? super P> initFunc) {
this.initFunc = checkNotNull(initFunc);
}

public static <S extends ExprState, P extends Prec> CfaInitFunc<S, P> create(final Loc initLoc,
final InitFunc<S, ? super P> initFunc) {
public static <S extends ExprState, P extends Prec> CfaInitFunc<S, P> create(
final Loc initLoc, final InitFunc<S, ? super P> initFunc) {
return new CfaInitFunc<>(initLoc, initFunc);
}

Expand All @@ -54,5 +53,4 @@ public Collection<CfaState<S>> getInitStates(final CfaPrec<P> prec) {
}
return initStates;
}

}
9 changes: 3 additions & 6 deletions subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/CfaInitPrecs.java
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
/*
* Copyright 2024 Budapest University of Technology and Economics
* Copyright 2025 Budapest University of Technology and Economics
*
* Licensed under the Apache License, Version 2.0 (the "License");
* you may not use this file except in compliance with the License.
Expand All @@ -20,20 +20,17 @@
import hu.bme.mit.theta.cfa.analysis.prec.GlobalCfaPrec;
import hu.bme.mit.theta.cfa.analysis.prec.LocalCfaPrec;
import hu.bme.mit.theta.common.Utils;
import hu.bme.mit.theta.common.container.Containers;
import hu.bme.mit.theta.core.stmt.AssumeStmt;
import hu.bme.mit.theta.core.type.Expr;
import hu.bme.mit.theta.core.type.booltype.BoolType;
import hu.bme.mit.theta.core.utils.ExprUtils;

import hu.bme.mit.theta.common.container.Containers;

import java.util.Map;
import java.util.Set;

public final class CfaInitPrecs {

private CfaInitPrecs() {
}
private CfaInitPrecs() {}

public static LocalCfaPrec<PredPrec> collectAssumesLocal(CFA cfa) {
Map<CFA.Loc, PredPrec> precs = Containers.createMap();
Expand Down
7 changes: 3 additions & 4 deletions subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/CfaOrd.java
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
/*
* Copyright 2024 Budapest University of Technology and Economics
* Copyright 2025 Budapest University of Technology and Economics
*
* Licensed under the Apache License, Version 2.0 (the "License");
* you may not use this file except in compliance with the License.
Expand Down Expand Up @@ -34,8 +34,7 @@ public static <S extends ExprState> CfaOrd<S> create(final PartialOrd<S> partial

@Override
public boolean isLeq(final CfaState<S> state1, final CfaState<S> state2) {
return state1.getLoc().equals(state2.getLoc()) && partialOrd.isLeq(state1.getState(),
state2.getState());
return state1.getLoc().equals(state2.getLoc())
&& partialOrd.isLeq(state1.getState(), state2.getState());
}

}
2 changes: 1 addition & 1 deletion subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/CfaPrec.java
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
/*
* Copyright 2024 Budapest University of Technology and Economics
* Copyright 2025 Budapest University of Technology and Economics
*
* Licensed under the Apache License, Version 2.0 (the "License");
* you may not use this file except in compliance with the License.
Expand Down
Loading

0 comments on commit b513261

Please sign in to comment.