formatting stack abstraction files

subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/BasicAbstractor.java

@@ -50,7 +50,7 @@ public class BasicAbstractor<S extends State, A extends Action, P extends Prec>
     protected final Logger logger;
 
     protected BasicAbstractor(final ArgBuilder<S, A, P> argBuilder, final Function<? super S, ?> projection,
-                            final Waitlist<ArgNode<S, A>> waitlist, final StopCriterion<S, A> stopCriterion, final Logger logger) {
+                              final Waitlist<ArgNode<S, A>> waitlist, final StopCriterion<S, A> stopCriterion, final Logger logger) {
         this.argBuilder = checkNotNull(argBuilder);
         this.projection = checkNotNull(projection);
         this.waitlist = checkNotNull(waitlist);

subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/SingleExprTraceRefiner.java

@@ -45,8 +45,8 @@ public class SingleExprTraceRefiner<S extends ExprState, A extends ExprAction, P
     protected final Logger logger;
 
     protected SingleExprTraceRefiner(final ExprTraceChecker<R> exprTraceChecker,
-                                   final PrecRefiner<S, A, P, R> precRefiner,
-                                   final PruneStrategy pruneStrategy, final Logger logger) {
+                                     final PrecRefiner<S, A, P, R> precRefiner,
+                                     final PruneStrategy pruneStrategy, final Logger logger) {
         this.exprTraceChecker = checkNotNull(exprTraceChecker);
         this.precRefiner = checkNotNull(precRefiner);
         this.pruneStrategy = checkNotNull(pruneStrategy);
@@ -55,9 +55,9 @@ protected SingleExprTraceRefiner(final ExprTraceChecker<R> exprTraceChecker,
     }
 
     protected SingleExprTraceRefiner(final ExprTraceChecker<R> exprTraceChecker,
-                                   final PrecRefiner<S, A, P, R> precRefiner,
-                                   final PruneStrategy pruneStrategy, final Logger logger,
-                                   final NodePruner<S, A> nodePruner) {
+                                     final PrecRefiner<S, A, P, R> precRefiner,
+                                     final PruneStrategy pruneStrategy, final Logger logger,
+                                     final NodePruner<S, A> nodePruner) {
         this.exprTraceChecker = checkNotNull(exprTraceChecker);
         this.precRefiner = checkNotNull(precRefiner);
         this.pruneStrategy = checkNotNull(pruneStrategy);

subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/Utils.kt

@@ -44,11 +44,13 @@ internal fun <S : ExprState> XcfaState<S>.withGeneralizedVars(): S {
     return when (sGlobal) {
         is ExplState -> ExplState.of(sGlobal.getVal().changeVars(varLookup))
         is PredState -> PredState.of(sGlobal.preds.map { p -> p.changeVars(varLookup) })
-        else -> throw NotImplementedError("Generalizing variable instances is not implemented for data states that are not explicit or predicate.")
+        else -> throw NotImplementedError(
+            "Generalizing variable instances is not implemented for data states that are not explicit or predicate.")
     } as S
 }
 
 class LazyDelegate<T, P : Any>(val getProperty: T.() -> P) {
+
     private var calculated = false
     private lateinit var property: P
 
@@ -62,7 +64,11 @@ class LazyDelegate<T, P : Any>(val getProperty: T.() -> P) {
 }
 
 val XCFA.isInlined: Boolean by LazyDelegate {
-    !this.procedures.any { p -> p.edges.any { e -> e.getFlatLabels().any { l ->
-        l is InvokeLabel && this.procedures.any { it.name == l.name }
-    } } }
+    !this.procedures.any { p ->
+        p.edges.any { e ->
+            e.getFlatLabels().any { l ->
+                l is InvokeLabel && this.procedures.any { it.name == l.name }
+            }
+        }
+    }
 }

subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaAbstractor.kt

@@ -90,7 +90,6 @@ class XcfaAbstractor<S : State, A : Action, P : Prec>(
 
         waitlist.clear() // Optimization
 
-
         return if (arg.isSafe) {
             Preconditions.checkState(arg.isComplete, "Returning incomplete ARG as safe")
             AbstractorResult.safe()
@@ -120,14 +119,17 @@ class XcfaAbstractor<S : State, A : Action, P : Prec>(
         }
     }
 
-    companion object{
-        fun<S : State, A : Action, P : Prec> builder(argBuilder: ArgBuilder<S, A, P>): BasicAbstractor.Builder<S, A, P> {
+    companion object {
+
+        fun <S : State, A : Action, P : Prec> builder(
+            argBuilder: ArgBuilder<S, A, P>): BasicAbstractor.Builder<S, A, P> {
             return Builder(argBuilder)
         }
     }
 
     class Builder<S : State, A : Action, P : Prec>(argBuilder: ArgBuilder<S, A, P>)
         : BasicAbstractor.Builder<S, A, P>(argBuilder) {
+
         override fun build(): BasicAbstractor<S, A, P> {
             return XcfaAbstractor(argBuilder, projection, waitlist, stopCriterion, logger)
         }

subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaAnalysis.kt

@@ -169,10 +169,11 @@ fun getXcfaErrorPredicate(
 
 fun <S : ExprState> getPartialOrder(partialOrd: PartialOrd<S>) =
     PartialOrd<XcfaState<S>> { s1, s2 ->
-        s1.processes == s2.processes && s1.bottom == s2.bottom && s1.mutexes == s2.mutexes && partialOrd.isLeq(s1.sGlobal, s2.sGlobal)
+        s1.processes == s2.processes && s1.bottom == s2.bottom && s1.mutexes == s2.mutexes && partialOrd.isLeq(
+            s1.sGlobal, s2.sGlobal)
     }
 
-private fun<S : ExprState> stackIsLeq(s1: XcfaState<S>, s2: XcfaState<S>) = s2.processes.keys.all { pid ->
+private fun <S : ExprState> stackIsLeq(s1: XcfaState<S>, s2: XcfaState<S>) = s2.processes.keys.all { pid ->
     s1.processes[pid]?.let { ps1 ->
         val ps2 = s2.processes.getValue(pid)
         ps1.locs.peek() == ps2.locs.peek() && ps1.paramsInitialized && ps2.paramsInitialized
@@ -181,15 +182,16 @@ private fun<S : ExprState> stackIsLeq(s1: XcfaState<S>, s2: XcfaState<S>) = s2.p
 
 fun <S : ExprState> getStackPartialOrder(partialOrd: PartialOrd<S>) =
     PartialOrd<XcfaState<S>> { s1, s2 ->
-        s1.processes.size == s2.processes.size && stackIsLeq(s1, s2) && s1.bottom == s2.bottom && s1.mutexes == s2.mutexes
+        s1.processes.size == s2.processes.size && stackIsLeq(s1,
+            s2) && s1.bottom == s2.bottom && s1.mutexes == s2.mutexes
             && partialOrd.isLeq(s1.withGeneralizedVars(), s2.withGeneralizedVars())
     }
 
 private fun <S : XcfaState<out ExprState>, P : XcfaPrec<out Prec>> getXcfaArgBuilder(
     analysis: Analysis<S, XcfaAction, P>,
     lts: LTS<XcfaState<out ExprState>, XcfaAction>,
     errorDetection: ErrorDetection)
-        : ArgBuilder<S, XcfaAction, P> =
+    : ArgBuilder<S, XcfaAction, P> =
     ArgBuilder.create(
         lts,
         analysis,
@@ -216,7 +218,7 @@ fun <S : XcfaState<out ExprState>, P : XcfaPrec<out Prec>> getXcfaAbstractor(
 /// EXPL
 
 private fun getExplXcfaInitFunc(xcfa: XCFA,
-                                solver: Solver): (XcfaPrec<ExplPrec>) -> List<XcfaState<ExplState>> {
+    solver: Solver): (XcfaPrec<ExplPrec>) -> List<XcfaState<ExplState>> {
     val processInitState = xcfa.initProcedures.mapIndexed { i, it ->
         val initLocStack: LinkedList<XcfaLocation> = LinkedList()
         initLocStack.add(it.first.initLoc)
@@ -230,7 +232,7 @@ private fun getExplXcfaInitFunc(xcfa: XCFA,
 }
 
 private fun getExplXcfaTransFunc(solver: Solver,
-                                 maxEnum: Int): (XcfaState<ExplState>, XcfaAction, XcfaPrec<ExplPrec>) -> List<XcfaState<ExplState>> {
+    maxEnum: Int): (XcfaState<ExplState>, XcfaAction, XcfaPrec<ExplPrec>) -> List<XcfaState<ExplState>> {
     val explTransFunc = ExplStmtTransFunc.create(solver, maxEnum)
     return { s, a, p ->
         val (newSt, newAct) = s.apply(a)
@@ -241,7 +243,7 @@ private fun getExplXcfaTransFunc(solver: Solver,
 }
 
 class ExplXcfaAnalysis(xcfa: XCFA, solver: Solver, maxEnum: Int,
-                       partialOrd: PartialOrd<XcfaState<ExplState>>) : XcfaAnalysis<ExplState, ExplPrec>(
+    partialOrd: PartialOrd<XcfaState<ExplState>>) : XcfaAnalysis<ExplState, ExplPrec>(
     corePartialOrd = partialOrd,
     coreInitFunc = getExplXcfaInitFunc(xcfa, solver),
     coreTransFunc = getExplXcfaTransFunc(solver, maxEnum)
@@ -250,7 +252,7 @@ class ExplXcfaAnalysis(xcfa: XCFA, solver: Solver, maxEnum: Int,
 /// PRED
 
 private fun getPredXcfaInitFunc(xcfa: XCFA,
-                                predAbstractor: PredAbstractor): (XcfaPrec<PredPrec>) -> List<XcfaState<PredState>> {
+    predAbstractor: PredAbstractor): (XcfaPrec<PredPrec>) -> List<XcfaState<PredState>> {
     val processInitState = xcfa.initProcedures.mapIndexed { i, it ->
         val initLocStack: LinkedList<XcfaLocation> = LinkedList()
         initLocStack.add(it.first.initLoc)
@@ -275,7 +277,7 @@ private fun getPredXcfaTransFunc(
 }
 
 class PredXcfaAnalysis(xcfa: XCFA, solver: Solver, predAbstractor: PredAbstractor,
-                       partialOrd: PartialOrd<XcfaState<PredState>>) : XcfaAnalysis<PredState, PredPrec>(
+    partialOrd: PartialOrd<XcfaState<PredState>>) : XcfaAnalysis<PredState, PredPrec>(
     corePartialOrd = partialOrd,
     coreInitFunc = getPredXcfaInitFunc(xcfa, predAbstractor),
     coreTransFunc = getPredXcfaTransFunc(predAbstractor)

subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaSingeExprTraceRefiner.kt

@@ -29,6 +29,7 @@ import java.util.LinkedList
 
 class XcfaSingleExprTraceRefiner<S : ExprState, A : ExprAction, P : Prec, R : Refutation> :
     SingleExprTraceRefiner<S, A, P, R> {
+
     private constructor(
         exprTraceChecker: ExprTraceChecker<R>,
         precRefiner: PrecRefiner<S, A, P, R>,
@@ -47,14 +48,15 @@ class XcfaSingleExprTraceRefiner<S : ExprState, A : ExprAction, P : Prec, R : Re
     private fun findPoppedState(trace: Trace<S, A>): Pair<Int, XcfaState<S>>? {
         trace.states.forEachIndexed { i, s ->
             val state = s as XcfaState<S>
-            state.processes.entries.find { (_, processState) -> processState.popped != null }?.let { (pid, processState) ->
-                val stackBeforePop = LinkedList(processState.locs)
-                stackBeforePop.push(processState.popped)
-                val processesBeforePop = state.processes.toMutableMap()
-                processesBeforePop[pid] = processState.copy(locs = stackBeforePop)
-                val stateBeforePop = state.copy(processes = processesBeforePop)
-                return Pair(i, stateBeforePop)
-            }
+            state.processes.entries.find { (_, processState) -> processState.popped != null }
+                ?.let { (pid, processState) ->
+                    val stackBeforePop = LinkedList(processState.locs)
+                    stackBeforePop.push(processState.popped)
+                    val processesBeforePop = state.processes.toMutableMap()
+                    processesBeforePop[pid] = processState.copy(locs = stackBeforePop)
+                    val stateBeforePop = state.copy(processes = processesBeforePop)
+                    return Pair(i, stateBeforePop)
+                }
         }
         return null
     }
@@ -94,6 +96,7 @@ class XcfaSingleExprTraceRefiner<S : ExprState, A : ExprAction, P : Prec, R : Re
     }
 
     companion object {
+
         fun <S : ExprState, A : ExprAction, P : Prec, R : Refutation> create(
             exprTraceChecker: ExprTraceChecker<R>, precRefiner: PrecRefiner<S, A, P, R>,
             pruneStrategy: PruneStrategy, logger: Logger