Skip to content

Commit

Permalink
Control flow splitting for Timed XSTS
Browse files Browse the repository at this point in the history
  • Loading branch information
DoriCz committed Dec 18, 2023
1 parent 79ecd0d commit 3b96563
Show file tree
Hide file tree
Showing 50 changed files with 4,746 additions and 18 deletions.
Original file line number Diff line number Diff line change
@@ -0,0 +1,47 @@
package hu.bme.mit.theta.analysis.expl;

import hu.bme.mit.theta.analysis.utils.ValuationExtractor;
import hu.bme.mit.theta.core.decl.Decl;
import hu.bme.mit.theta.core.decl.VarDecl;
import hu.bme.mit.theta.core.model.ImmutableValuation;
import hu.bme.mit.theta.core.model.Valuation;
import hu.bme.mit.theta.core.type.LitExpr;

import java.util.Collection;
import java.util.Map;

public final class ExplStateValuationExtractor implements ValuationExtractor<ExplState> {

private static final class LazyHolder {
private static final ExplStateValuationExtractor INSTANCE = new ExplStateValuationExtractor();
}

private ExplStateValuationExtractor() {
}

public static ExplStateValuationExtractor getInstance() {
return ExplStateValuationExtractor.LazyHolder.INSTANCE;
}

@Override
public Valuation extractValuation(ExplState state) {
return state.getVal();
}

@Override
public Valuation extractValuationForVars(ExplState state, Collection<VarDecl<?>> vars) {

final ImmutableValuation.Builder builder = ImmutableValuation.builder();

final Map<Decl<?>, LitExpr<?>> varToValue = state.getVal().toMap();

for (final VarDecl<?> varDecl : vars) {
final LitExpr<?> value = varToValue.get(varDecl);
if (value != null) {
builder.put(varDecl, value);
}
}

return builder.build();
}
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,33 @@
package hu.bme.mit.theta.analysis.pred;

import hu.bme.mit.theta.analysis.utils.ValuationExtractor;
import hu.bme.mit.theta.core.decl.VarDecl;
import hu.bme.mit.theta.core.model.ImmutableValuation;
import hu.bme.mit.theta.core.model.Valuation;

import java.util.Collection;

public final class PredStateValuationExtractor implements ValuationExtractor<PredState> {

private static final class LazyHolder {
private static final PredStateValuationExtractor INSTANCE = new PredStateValuationExtractor();
}

private PredStateValuationExtractor() {
}

public static PredStateValuationExtractor getInstance() {
return PredStateValuationExtractor.LazyHolder.INSTANCE;
}


@Override
public Valuation extractValuation(PredState state) {
return ImmutableValuation.empty();
}

@Override
public Valuation extractValuationForVars(PredState state, Collection<VarDecl<?>> vars) {
return ImmutableValuation.empty();
}
}
Original file line number Diff line number Diff line change
Expand Up @@ -26,7 +26,7 @@
import hu.bme.mit.theta.analysis.State;
import hu.bme.mit.theta.analysis.TransFunc;

final class Prod2TransFunc<S1 extends State, S2 extends State, A extends Action, P1 extends Prec, P2 extends Prec>
public final class Prod2TransFunc<S1 extends State, S2 extends State, A extends Action, P1 extends Prec, P2 extends Prec>
implements TransFunc<Prod2State<S1, S2>, A, Prod2Prec<P1, P2>> {

private final TransFunc<S1, ? super A, P1> transFunc1;
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,36 @@
package hu.bme.mit.theta.analysis.prod2.prod2explpred;

import hu.bme.mit.theta.analysis.expl.ExplState;
import hu.bme.mit.theta.analysis.expl.ExplStateValuationExtractor;
import hu.bme.mit.theta.analysis.pred.PredState;
import hu.bme.mit.theta.analysis.prod2.Prod2State;
import hu.bme.mit.theta.analysis.utils.ValuationExtractor;
import hu.bme.mit.theta.core.decl.VarDecl;
import hu.bme.mit.theta.core.model.Valuation;

import java.util.Collection;

public class Prod2ExplPredStateValuationExtractor implements ValuationExtractor<Prod2State<ExplState, PredState>> {

private final ExplStateValuationExtractor explValExtractor;

private Prod2ExplPredStateValuationExtractor(final ExplStateValuationExtractor explValExtractor) {
this.explValExtractor = explValExtractor;
}

public static Prod2ExplPredStateValuationExtractor create(final ExplStateValuationExtractor explStateValExtractor) {
return new Prod2ExplPredStateValuationExtractor(explStateValExtractor);
}

@Override
public Valuation extractValuation(Prod2State<ExplState, PredState> state) {
final ExplState explState = state.getState1();
return explValExtractor.extractValuation(explState);
}

@Override
public Valuation extractValuationForVars(Prod2State<ExplState, PredState> state, Collection<VarDecl<?>> vars) {
final ExplState explState = state.getState1();
return explValExtractor.extractValuationForVars(explState, vars);
}
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
package hu.bme.mit.theta.analysis.utils;

import hu.bme.mit.theta.analysis.State;
import hu.bme.mit.theta.core.decl.VarDecl;
import hu.bme.mit.theta.core.model.Valuation;

import java.util.Collection;

public interface ValuationExtractor <S extends State> {

Valuation extractValuation(final S state);

Valuation extractValuationForVars(final S state, final Collection<VarDecl<?>> vars);
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,26 @@
package hu.bme.mit.theta.analysis.zone;

import hu.bme.mit.theta.analysis.InitFunc;

import java.util.Collection;
import java.util.Collections;

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

public class ZoneInitFunc implements InitFunc<ZoneState, ZonePrec> {

private static final ZoneInitFunc INSTANCE = new ZoneInitFunc();

private ZoneInitFunc() {
}

public static ZoneInitFunc getInstance() {
return INSTANCE;
}

@Override
public Collection<? extends ZoneState> getInitStates(ZonePrec prec) {
checkNotNull(prec);
return Collections.singleton(ZoneState.zero(prec.getVars()).transform().up().build());
}
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,41 @@
package hu.bme.mit.theta.analysis.zone;

import hu.bme.mit.theta.analysis.Analysis;
import hu.bme.mit.theta.analysis.InitFunc;
import hu.bme.mit.theta.analysis.PartialOrd;
import hu.bme.mit.theta.analysis.TransFunc;
import hu.bme.mit.theta.analysis.expr.StmtAction;

public class ZoneStmtAnalysis implements Analysis<ZoneState, StmtAction, ZonePrec> {

private static final ZoneStmtAnalysis INSTANCE = new ZoneStmtAnalysis();

private final PartialOrd<ZoneState> partialOrd;
private final InitFunc<ZoneState, ZonePrec> initFunc;
private final TransFunc<ZoneState, StmtAction, ZonePrec> transFunc;

private ZoneStmtAnalysis() {
this.partialOrd = ZoneOrd.getInstance();
this.initFunc = ZoneInitFunc.getInstance();
this.transFunc = ZoneStmtTransFunc.getInstance();
}

public static ZoneStmtAnalysis getInstance() {
return INSTANCE;
}

@Override
public PartialOrd<ZoneState> getPartialOrd() {
return partialOrd;
}

@Override
public InitFunc<ZoneState, ZonePrec> getInitFunc() {
return initFunc;
}

@Override
public TransFunc<ZoneState, StmtAction, ZonePrec> getTransFunc() {
return transFunc;
}
}
Loading

0 comments on commit 3b96563

Please sign in to comment.