From af2672b3c9a3ab9f63799cf45932f3766c0e89cd Mon Sep 17 00:00:00 2001 From: RipplB Date: Thu, 22 Feb 2024 22:23:39 +0100 Subject: [PATCH] Added multi formalism to create product of arbitrary number of formalisms --- .../analysis/multi/ExprMultiAnalysis.java | 53 ++++++++ .../theta/analysis/multi/ExprMultiLts.java | 49 +++++++ .../theta/analysis/multi/ExprMultiState.java | 50 ++++++++ .../mit/theta/analysis/multi/MultiAction.java | 25 ++++ .../theta/analysis/multi/MultiAnalysis.java | 120 ++++++++++++++++++ .../multi/MultiAnalysisBuilderFunc.java | 37 ++++++ .../theta/analysis/multi/MultiBuilder.java | 95 ++++++++++++++ .../mit/theta/analysis/multi/MultiLts.java | 68 ++++++++++ .../analysis/multi/MultiLtsBuilderFunc.java | 34 +++++ .../mit/theta/analysis/multi/MultiPrec.java | 37 ++++++ .../theta/analysis/multi/MultiSourceSide.java | 20 +++ .../mit/theta/analysis/multi/MultiState.java | 95 ++++++++++++++ .../theta/analysis/multi/RefToMultiPrec.java | 38 ++++++ .../theta/analysis/multi/StmtMultiAction.java | 66 ++++++++++ 14 files changed, 787 insertions(+) create mode 100644 subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/ExprMultiAnalysis.java create mode 100644 subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/ExprMultiLts.java create mode 100644 subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/ExprMultiState.java create mode 100644 subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiAction.java create mode 100644 subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiAnalysis.java create mode 100644 subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiAnalysisBuilderFunc.java create mode 100644 subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiBuilder.java create mode 100644 subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiLts.java create mode 100644 subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiLtsBuilderFunc.java create mode 100644 subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiPrec.java create mode 100644 subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiSourceSide.java create mode 100644 subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiState.java create mode 100644 subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/RefToMultiPrec.java create mode 100644 subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/StmtMultiAction.java diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/ExprMultiAnalysis.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/ExprMultiAnalysis.java new file mode 100644 index 0000000000..e3f574019c --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/ExprMultiAnalysis.java @@ -0,0 +1,53 @@ +/* + * Copyright 2024 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. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package hu.bme.mit.theta.analysis.multi; + +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.analysis.expr.StmtAction; + +import java.util.function.Function; + +public final class ExprMultiAnalysis + extends MultiAnalysis, StmtMultiAction> { + + private ExprMultiAnalysis(Function, MultiSourceSide> defineNextSide, Side leftSide, Side rightSide, InitFunc dataInitFunc) { + super(defineNextSide, leftSide, rightSide, dataInitFunc); + } + + public static + ExprMultiAnalysis + of(Side leftSide, Side rightSide, + Function, MultiSourceSide> defineNextSide, + InitFunc dataInitFunc) { + return new ExprMultiAnalysis<>(defineNextSide, leftSide, rightSide, dataInitFunc); + } + + @Override + ExprMultiState createInitialState(LBlank leftState, RBlank rightState, DataState dataState) { + return ExprMultiState.createInitial(leftState, rightState, dataState); + } + + @Override + ExprMultiState createState(LBlank leftState, RBlank rightState, DataState dataState, MultiSourceSide sourceSide) { + return ExprMultiState.create(leftState, rightState, dataState, sourceSide, true); + } +} diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/ExprMultiLts.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/ExprMultiLts.java new file mode 100644 index 0000000000..b6228dfe24 --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/ExprMultiLts.java @@ -0,0 +1,49 @@ +/* + * Copyright 2024 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. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package hu.bme.mit.theta.analysis.multi; + +import hu.bme.mit.theta.analysis.LTS; +import hu.bme.mit.theta.analysis.expr.ExprState; +import hu.bme.mit.theta.analysis.expr.StmtAction; + +import java.util.function.BiFunction; +import java.util.function.Function; + +public final class ExprMultiLts + extends MultiLts, StmtMultiAction> { + + private ExprMultiLts(Function, MultiSourceSide> defineNextSide, Side left, Side right) { + super(defineNextSide, left, right); + } + + public static + ExprMultiLts of( + LTS leftLts, BiFunction wrapLeftState, + LTS rightLts, BiFunction wrapRightState, + Function, MultiSourceSide> defineNextSide) { + return new ExprMultiLts<>(defineNextSide, new Side<>(leftLts, wrapLeftState), new Side<>(rightLts, wrapRightState)); + } + + @Override + StmtMultiAction wrapLeftAction(LAction action) { + return StmtMultiAction.ofLeftStmtAction(action); + } + + @Override + StmtMultiAction wrapRightAction(RAction action) { + return StmtMultiAction.ofRightStmtAction(action); + } +} diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/ExprMultiState.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/ExprMultiState.java new file mode 100644 index 0000000000..86bb87be05 --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/ExprMultiState.java @@ -0,0 +1,50 @@ +/* + * Copyright 2024 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. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package hu.bme.mit.theta.analysis.multi; + +import hu.bme.mit.theta.analysis.expr.ExprState; +import hu.bme.mit.theta.core.type.Expr; +import hu.bme.mit.theta.core.type.booltype.BoolType; + +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.And; + +public final class ExprMultiState extends MultiState implements ExprState { + + private ExprMultiState(L ls, R rs, D data, MultiSourceSide sourceSide, boolean sourceMattersInEquality) { + super(ls, rs, data, sourceSide, sourceMattersInEquality); + } + + public static ExprMultiState create(L ls, R rs, D d, MultiSourceSide sourceSide, boolean sourceMattersInEquality) { + return new ExprMultiState<>(ls, rs, d, sourceSide, sourceMattersInEquality); + } + + public static ExprMultiState create(L ls, R rs, D d, MultiSourceSide sourceSide) { + return create(ls, rs, d, sourceSide, true); + } + + public static ExprMultiState createInitial(L ls, R rs, D d, boolean sourceMattersInEquality) { + return create(ls, rs, d, null, sourceMattersInEquality); + } + + public static ExprMultiState createInitial(L ls, R rs, D d) { + return createInitial(ls, rs, d, true); + } + + @Override + public Expr toExpr() { + return And(And(getLeftState().toExpr(), getRightState().toExpr()), getDataState().toExpr()); + } +} diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiAction.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiAction.java new file mode 100644 index 0000000000..74d9c52188 --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiAction.java @@ -0,0 +1,25 @@ +/* + * Copyright 2024 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. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package hu.bme.mit.theta.analysis.multi; + + +import hu.bme.mit.theta.analysis.Action; + +public interface MultiAction extends Action { + L getLeftAction(); + + R getRightAction(); +} diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiAnalysis.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiAnalysis.java new file mode 100644 index 0000000000..2fb9277978 --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiAnalysis.java @@ -0,0 +1,120 @@ +/* + * Copyright 2024 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. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package hu.bme.mit.theta.analysis.multi; + +import hu.bme.mit.theta.analysis.Action; +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.Prec; +import hu.bme.mit.theta.analysis.State; +import hu.bme.mit.theta.analysis.TransFunc; + +import java.util.Collection; +import java.util.HashSet; +import java.util.function.BiFunction; +import java.util.function.Function; +import java.util.stream.Collectors; +import java.util.stream.Stream; + +/** + * @param Type of combined (with data) state of left formalism + * @param Type of combined (with data) state of right formalism + * @param Type of data state + * @param Type of blank state from left formalism + * @param Type of blank state from right formalism + * @param Type of action from left formalism + * @param Type of action from right formalism + * @param Type of precision of left formalism + * @param Type of precision of right formalism + * @param Type of data precision (formalism independent) + */ +public abstract class MultiAnalysis, MAction extends MultiAction> + implements Analysis> { + + private final Function defineNextSide; + + private final Side leftSide; + private final Side rightSide; + + private final InitFunc dataInitFunc; + + protected MultiAnalysis(Function defineNextSide, Side leftSide, Side rightSide, InitFunc dataInitFunc) { + this.defineNextSide = defineNextSide; + this.leftSide = leftSide; + this.rightSide = rightSide; + this.dataInitFunc = dataInitFunc; + } + + abstract MState createInitialState(LBlank leftState, RBlank rightState, DataState dataState); + + abstract MState createState(LBlank leftState, RBlank rightState, DataState dataState, MultiSourceSide sourceSide); + + @Override + public PartialOrd getPartialOrd() { + return ((state1, state2) -> leftSide.analysis.getPartialOrd().isLeq(leftSide.combineStates.apply(state1.getLeftState(), state1.getDataState()), leftSide.combineStates.apply(state2.getLeftState(), state2.getDataState())) + && rightSide.analysis.getPartialOrd().isLeq(rightSide.combineStates.apply(state1.getRightState(), state1.getDataState()), rightSide.combineStates.apply(state2.getRightState(), state2.getDataState())) + && ((!state1.getSourceMattersInEquality() && !state2.getSourceMattersInEquality()) || (state1.getSourceSide() == state2.getSourceSide()))); + } + + @Override + public InitFunc> getInitFunc() { + return (prec -> { + LBlankPrec leftInitPrec = leftSide.stripDataFromPrec.apply(prec.leftPrec()); + RBlankPrec rightInitPrec = rightSide.stripDataFromPrec.apply(prec.rightPrec()); + Collection leftInitStates = new HashSet<>(leftSide.initFunc.getInitStates(leftInitPrec)); + Collection rightInitStates = new HashSet<>(rightSide.initFunc.getInitStates(rightInitPrec)); + Collection dataInitStates = dataInitFunc.getInitStates(prec.dataPrec()); + Collection resultSet = new HashSet<>(); + for (LBlank leftInitState : + leftInitStates) { + for (RBlank rightInitState : + rightInitStates) { + for (DataState dataInitState : + dataInitStates) { + resultSet.add(createInitialState(leftInitState, rightInitState, dataInitState)); + } + } + } + return resultSet; + }); + } + + @Override + public TransFunc> getTransFunc() { + return ((state, action, prec) -> switch (defineNextSide.apply(state)) { + case LEFT -> { + final var succStates = leftSide.analysis.getTransFunc().getSuccStates(leftSide.combineStates().apply(state.getLeftState(), state.getDataState()), action.getLeftAction(), prec.leftPrec()); + final Stream multiStateStream = succStates.stream().map(s -> createState(leftSide.stripDataFromState().apply(s), state.getRightState(), leftSide.extractDataFromState.apply(s), MultiSourceSide.LEFT)); + yield multiStateStream.collect(Collectors.toSet()); + } + case RIGHT -> { + final var succStates = rightSide.analysis.getTransFunc().getSuccStates(rightSide.combineStates.apply(state.getRightState(), state.getDataState()), action.getRightAction(), prec.rightPrec()); + final Stream multiStateStream = succStates.stream().map(s -> createState(state.getLeftState(), rightSide.stripDataFromState.apply(s), rightSide.extractDataFromState.apply(s), MultiSourceSide.RIGHT)); + yield multiStateStream.collect(Collectors.toSet()); + } + }); + } + + public record Side + (Analysis analysis, InitFunc initFunc, + BiFunction combineStates, Function stripDataFromState, + Function extractDataFromState, Function stripDataFromPrec) { + } +} diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiAnalysisBuilderFunc.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiAnalysisBuilderFunc.java new file mode 100644 index 0000000000..82c1f08ba8 --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiAnalysisBuilderFunc.java @@ -0,0 +1,37 @@ +/* + * Copyright 2024 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. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package hu.bme.mit.theta.analysis.multi; + +import hu.bme.mit.theta.analysis.Action; +import hu.bme.mit.theta.analysis.InitFunc; +import hu.bme.mit.theta.analysis.Prec; +import hu.bme.mit.theta.analysis.State; + +import java.util.function.Function; + +@FunctionalInterface +public interface MultiAnalysisBuilderFunc, MAction extends MultiAction, + MAnalysis extends MultiAnalysis> { + + MAnalysis build(MultiAnalysis.Side leftSide, + MultiAnalysis.Side rightSide, + Function defineNextSide, + InitFunc dataInitFunc); + +} diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiBuilder.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiBuilder.java new file mode 100644 index 0000000000..7e5e6d1d16 --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiBuilder.java @@ -0,0 +1,95 @@ +/* + * Copyright 2024 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. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package hu.bme.mit.theta.analysis.multi; + +import hu.bme.mit.theta.analysis.Action; +import hu.bme.mit.theta.analysis.Analysis; +import hu.bme.mit.theta.analysis.InitFunc; +import hu.bme.mit.theta.analysis.LTS; +import hu.bme.mit.theta.analysis.Prec; +import hu.bme.mit.theta.analysis.State; + +import java.util.function.BiFunction; +import java.util.function.Function; + +public final class MultiBuilder { + + public static + LeftSideAdded initWithLeftSide( + Analysis analysis, BiFunction combineStates, Function stripDataFromState, Function extractDataFromState, LTS lts, InitFunc initFunc, Function stripDataFromPrec + ) { + return new LeftSideAdded<>(analysis, combineStates, stripDataFromState, extractDataFromState, lts, initFunc, stripDataFromPrec); + } + + public record Result, MAction extends MultiAction> + (MultiAnalysis analysis, + MultiLts lts) { + } + + public static class LeftSideAdded { + private final MultiAnalysis.Side side; + private final LTS lts; + + LeftSideAdded(Analysis analysis, BiFunction combineStates, Function stripDataFromState, + Function extractDataFromState, LTS lts, InitFunc initFunc, Function stripDataFromPrec) { + this.lts = lts; + this.side = new MultiAnalysis.Side<>(analysis, initFunc, combineStates, stripDataFromState, extractDataFromState, stripDataFromPrec); + } + + public + BothSidesDone + addRightSide(Analysis analysis, LTS rightLts, + BiFunction combineStates, Function stripDataFromState, Function extractDataFromState, + InitFunc initFunc, Function stripDataFromPrec) { + MultiAnalysis.Side rightSide = new MultiAnalysis.Side<>(analysis, initFunc, combineStates, stripDataFromState, extractDataFromState, stripDataFromPrec); + return new BothSidesDone<>(side, lts, rightSide, rightLts); + } + + } + + public static class BothSidesDone { + private final MultiAnalysis.Side leftSide; + private final LTS leftLts; + private final MultiAnalysis.Side rightSide; + private final LTS rightLts; + + BothSidesDone(MultiAnalysis.Side leftSide, LTS leftLts, MultiAnalysis.Side rightSide, LTS rightLts) { + this.leftSide = leftSide; + this.leftLts = leftLts; + this.rightSide = rightSide; + this.rightLts = rightLts; + } + + public , MAction extends MultiAction> + Result + build(Function defineNextSide, InitFunc dataInitFunc, + MultiAnalysisBuilderFunc> analysisBuilderFunc, + MultiLtsBuilderFunc> ltsBuilderFunc) { + return new Result<>( + analysisBuilderFunc.build(leftSide, rightSide, defineNextSide, dataInitFunc), + ltsBuilderFunc.build(leftLts, leftSide.combineStates(), rightLts, rightSide.combineStates(), defineNextSide) + ); + } + + } + +} diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiLts.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiLts.java new file mode 100644 index 0000000000..de3354c9d0 --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiLts.java @@ -0,0 +1,68 @@ +/* + * Copyright 2024 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. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package hu.bme.mit.theta.analysis.multi; + +import hu.bme.mit.theta.analysis.Action; +import hu.bme.mit.theta.analysis.LTS; +import hu.bme.mit.theta.analysis.State; + +import java.util.Collection; +import java.util.function.BiFunction; +import java.util.function.Function; +import java.util.stream.Stream; + +public abstract class MultiLts, MAction extends MultiAction> + implements LTS { + + private final Function defineNextSide; + private final Side left; + private final Side right; + + protected MultiLts(Function defineNextSide, Side left, Side right) { + this.defineNextSide = defineNextSide; + this.left = left; + this.right = right; + } + + abstract MAction wrapLeftAction(LAction action); + + abstract MAction wrapRightAction(RAction action); + + @Override + public Collection getEnabledActionsFor(MState state) { + return switch (defineNextSide.apply(state)) { + case LEFT -> { + Stream actionStream = left.lts.getEnabledActionsFor(left.combineStates.apply(state.getLeftState(), state.getDataState())).stream(); + Stream multiActionStream = actionStream.map(this::wrapLeftAction); + yield multiActionStream.toList(); + } + case RIGHT -> { + Stream actionStream = right.lts.getEnabledActionsFor(right.combineStates.apply(state.getRightState(), state.getDataState())).stream(); + Stream multiActionStream = actionStream.map(this::wrapRightAction); + yield multiActionStream.toList(); + } + }; + } + + public Function getDefineNextSide() { + return defineNextSide; + } + + protected record Side( + LTS lts, BiFunction combineStates) { + } + +} diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiLtsBuilderFunc.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiLtsBuilderFunc.java new file mode 100644 index 0000000000..b9153c6226 --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiLtsBuilderFunc.java @@ -0,0 +1,34 @@ +/* + * Copyright 2024 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. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package hu.bme.mit.theta.analysis.multi; + +import hu.bme.mit.theta.analysis.Action; +import hu.bme.mit.theta.analysis.LTS; +import hu.bme.mit.theta.analysis.State; + +import java.util.function.BiFunction; +import java.util.function.Function; + +@FunctionalInterface +public interface MultiLtsBuilderFunc, MAction extends MultiAction, + MLts extends MultiLts> { + + MLts build(LTS leftLts, BiFunction combineLeftState, + LTS rightLts, BiFunction combineRightState, + Function defineNextSide); + +} diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiPrec.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiPrec.java new file mode 100644 index 0000000000..b6a85ea69d --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiPrec.java @@ -0,0 +1,37 @@ +/* + * Copyright 2024 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. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package hu.bme.mit.theta.analysis.multi; + +import hu.bme.mit.theta.analysis.Prec; +import hu.bme.mit.theta.core.decl.VarDecl; + +import java.util.Collection; + +public record MultiPrec( + LPrec leftPrec, RPrec rightPrec, DataPrec dataPrec) implements Prec { + + @Override + public Collection> getUsedVars() { + return dataPrec.getUsedVars(); + } + + @Override + public String toString() { + return "MultiPrec{" + + "dataPrec=" + dataPrec + + '}'; + } +} diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiSourceSide.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiSourceSide.java new file mode 100644 index 0000000000..dd4d8cd02e --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiSourceSide.java @@ -0,0 +1,20 @@ +/* + * Copyright 2024 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. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package hu.bme.mit.theta.analysis.multi; + +public enum MultiSourceSide { + LEFT, RIGHT +} diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiState.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiState.java new file mode 100644 index 0000000000..72f65ad2ab --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiState.java @@ -0,0 +1,95 @@ +/* + * Copyright 2024 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. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package hu.bme.mit.theta.analysis.multi; + +import com.google.common.base.Objects; +import hu.bme.mit.theta.analysis.State; + +public abstract class MultiState implements State { + + private final LState leftState; + private final RState rightState; + private final DataState dataState; + + /** + * Denotes whether this state derived from an action that considered the left state of the previous multi state. + * Can be null. Is always null for initial states. + */ + private final MultiSourceSide sourceSide; + + /** + * Flag whether to include {@link hu.bme.mit.theta.analysis.multi.MultiState#sourceSide} in {@link hu.bme.mit.theta.analysis.multi.MultiState#equals(Object)} + */ + private final boolean sourceMattersInEquality; + + protected MultiState(LState ls, RState rs, DataState data, MultiSourceSide sourceSide, boolean sourceMattersInEquality) { + leftState = ls; + rightState = rs; + dataState = data; + this.sourceSide = sourceSide; + this.sourceMattersInEquality = sourceMattersInEquality; + } + + public MultiSourceSide getSourceSide() { + return sourceSide; + } + + @Override + public boolean isBottom() { + return dataState.isBottom() || leftState.isBottom() || rightState.isBottom(); + } + + @Override + public boolean equals(Object o) { + if (this == o) return true; + if (o == null || getClass() != o.getClass()) return false; + MultiState that = (MultiState) o; + if ((sourceMattersInEquality || that.sourceMattersInEquality) && sourceSide != that.sourceSide) + return false; + return Objects.equal(leftState, that.leftState) && Objects.equal(rightState, that.rightState) && Objects.equal(dataState, that.dataState); + } + + @Override + public int hashCode() { + return Objects.hashCode(leftState, rightState, dataState, sourceSide, sourceMattersInEquality); + } + + + public LState getLeftState() { + return leftState; + } + + public RState getRightState() { + return rightState; + } + + public DataState getDataState() { + return dataState; + } + + public boolean getSourceMattersInEquality() { + return sourceMattersInEquality; + } + + @Override + public String toString() { + return "MultiState{" + + "leftState=" + leftState + + ", rightState=" + rightState + + ", dataState=" + dataState + + '}'; + } +} diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/RefToMultiPrec.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/RefToMultiPrec.java new file mode 100644 index 0000000000..c913f6374e --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/RefToMultiPrec.java @@ -0,0 +1,38 @@ +/* + * Copyright 2024 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. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package hu.bme.mit.theta.analysis.multi; + +import hu.bme.mit.theta.analysis.Prec; +import hu.bme.mit.theta.analysis.expr.refinement.Refutation; +import hu.bme.mit.theta.analysis.expr.refinement.RefutationToPrec; + +public record RefToMultiPrec( + RefutationToPrec leftRefToPrec, + RefutationToPrec rightRefToPrec, + RefutationToPrec dataRefToPrec +) + implements RefutationToPrec, R> { + + @Override + public MultiPrec toPrec(R refutation, int index) { + return new MultiPrec<>(leftRefToPrec.toPrec(refutation, index), rightRefToPrec().toPrec(refutation, index), dataRefToPrec().toPrec(refutation, index)); + } + + @Override + public MultiPrec join(MultiPrec prec1, MultiPrec prec2) { + return new MultiPrec<>(leftRefToPrec.join(prec1.leftPrec(), prec2.leftPrec()), rightRefToPrec.join(prec1.rightPrec(), prec2.rightPrec()), dataRefToPrec.join(prec1.dataPrec(), prec2.dataPrec())); + } +} diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/StmtMultiAction.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/StmtMultiAction.java new file mode 100644 index 0000000000..f781e4633d --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/StmtMultiAction.java @@ -0,0 +1,66 @@ +/* + * Copyright 2024 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. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package hu.bme.mit.theta.analysis.multi; + +import hu.bme.mit.theta.analysis.expr.StmtAction; +import hu.bme.mit.theta.core.stmt.Stmt; + +import java.util.List; + +public final class StmtMultiAction extends StmtAction implements MultiAction { + private final L leftAction; + private final R rightAction; + + private StmtMultiAction(L lAction, R rAction) { + leftAction = lAction; + rightAction = rAction; + } + + public static StmtMultiAction ofLeftStmtAction(L action) { + return new StmtMultiAction<>(action, null); + } + + public static StmtMultiAction ofRightStmtAction(R action) { + return new StmtMultiAction<>(null, action); + } + + public StmtAction getAction() { + return getLeftAction() == null ? getRightAction() : getLeftAction(); + } + + @Override + public String toString() { + return "ExprMultiAction{" + + "leftAction=" + leftAction + + ", rightAction=" + rightAction + + '}'; + } + + @Override + public List getStmts() { + return getAction().getStmts(); + } + + @Override + public L getLeftAction() { + return leftAction; + } + + @Override + public R getRightAction() { + return rightAction; + } +}