Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Original file line number Diff line number Diff line change
@@ -0,0 +1,77 @@
/**
* *****************************************************************************
* Copyright (c) 2018 Fraunhofer IEM, Paderborn, Germany
* <p>
* This program and the accompanying materials are made available under the
* terms of the Eclipse Public License 2.0 which is available at
* http://www.eclipse.org/legal/epl-2.0.
* <p>
* SPDX-License-Identifier: EPL-2.0
* <p>
* Contributors:
* Johannes Spaeth - initial API and implementation
* *****************************************************************************
*/
package typestate;

import boomerang.scope.Statement;
import com.google.common.collect.ImmutableSet;
import com.google.common.collect.Multimap;
import java.util.Objects;
import java.util.Set;
import org.jspecify.annotations.NonNull;
import typestate.finiteautomata.Transition;

/**
* The result of combining transition functions with different state change statements. It keeps
* all of them so that {@link TransitionFunctionImpl#combineWith} stays commutative, while the
* common single-statement case in {@link TransitionFunctionImpl} does not pay for a set.
*/
final class CombinedTransitionFunctionImpl extends TransitionFunctionImpl {

@NonNull private final ImmutableSet<Statement> stateChangeStatements;

/**
* @param stateChangeStatements at least two statements; the first one is the one {@link
* #getStateChangeStatement()} returns
*/
CombinedTransitionFunctionImpl(
@NonNull Multimap<Transition, StatementSequence> transitionStatementSequences,
@NonNull Set<Statement> stateChangeStatements) {
super(transitionStatementSequences, stateChangeStatements.iterator().next());
if (stateChangeStatements.size() < 2) {
throw new IllegalArgumentException(
"A combined transition function needs at least two state change statements");
}
this.stateChangeStatements = ImmutableSet.copyOf(stateChangeStatements);
}

@NonNull
@Override
TransitionFunctionImpl withStateChangeSequences(
@NonNull Multimap<Transition, StatementSequence> transitionStatementSequences) {
return new CombinedTransitionFunctionImpl(transitionStatementSequences, stateChangeStatements);
}

@NonNull
@Override
Set<Statement> getStateChangeStatements() {
return stateChangeStatements;
}

@Override
public boolean equals(Object o) {
// not super.equals: that compares getStateChangeStatement(), which depends on the order in
// which the functions were combined
if (this == o) return true;
if (o == null || getClass() != o.getClass()) return false;
CombinedTransitionFunctionImpl that = (CombinedTransitionFunctionImpl) o;
return getStateChangeSequences().equals(that.getStateChangeSequences())
&& stateChangeStatements.equals(that.stateChangeStatements);
}

@Override
public int hashCode() {
return Objects.hash(getStateChangeSequences(), stateChangeStatements);
}
}
38 changes: 35 additions & 3 deletions idealPDS/src/main/java/typestate/TransitionFunctionImpl.java
Original file line number Diff line number Diff line change
Expand Up @@ -23,8 +23,11 @@
import com.google.common.collect.Multimap;
import java.util.ArrayList;
import java.util.Collection;
import java.util.Collections;
import java.util.LinkedHashSet;
import java.util.List;
import java.util.Objects;
import java.util.Set;
import java.util.stream.Collectors;
import org.jspecify.annotations.NonNull;
import typestate.finiteautomata.Transition;
Expand Down Expand Up @@ -66,6 +69,16 @@ public TransitionFunctionImpl(
this.stateChangeStatement = stateChangeStatement;
}

/**
* Returns a transition function with the given sequences and the state change statements of
* this function.
*/
@NonNull
TransitionFunctionImpl withStateChangeSequences(
@NonNull Multimap<Transition, StatementSequence> transitionStatementSequences) {
return new TransitionFunctionImpl(transitionStatementSequences, stateChangeStatement);
}

@NonNull
@Override
public Multimap<Transition, StatementSequence> getStateChangeSequences() {
Expand All @@ -76,6 +89,16 @@ public Statement getStateChangeStatement() {
return stateChangeStatement;
}

/**
* The statements whose state changes this function describes. A function built from a single
* statement returns just that one; a combination of functions returns the statements of all of
* them (see {@link CombinedTransitionFunctionImpl}).
*/
@NonNull
Set<Statement> getStateChangeStatements() {
return Collections.singleton(stateChangeStatement);
}

@NonNull
@Override
public Weight extendWith(@NonNull Weight other) {
Expand Down Expand Up @@ -122,7 +145,7 @@ public Weight extendWith(@NonNull Weight other) {
}
}
}
return new TransitionFunctionImpl(result, func.stateChangeStatement);
return new TransitionFunctionImpl(result, func.getStateChangeStatement());
}

@NonNull
Expand All @@ -146,7 +169,7 @@ public Weight combineWith(@NonNull Weight other) {
transitions.putAll(idTransition, statements);
}

return new TransitionFunctionImpl(transitions, this.stateChangeStatement);
return withStateChangeSequences(transitions);
}

TransitionFunctionImpl func = (TransitionFunctionImpl) other;
Expand All @@ -155,7 +178,16 @@ public Weight combineWith(@NonNull Weight other) {
sequences.putAll(stateChangeSequences);
sequences.putAll(func.stateChangeSequences);

return new TransitionFunctionImpl(sequences, func.stateChangeStatement);
// combineWith has to be commutative, so the result keeps the state change statements of both
// functions. Keeping only one of them makes PostStar.update and
// WeightedPAutomaton.addWeightForTransition replace each other's weights forever.
Set<Statement> mergedStateChangeStatements =
new LinkedHashSet<>(func.getStateChangeStatements());
mergedStateChangeStatements.addAll(getStateChangeStatements());
if (mergedStateChangeStatements.size() == 1) {
return new TransitionFunctionImpl(sequences, func.getStateChangeStatement());
}
return new CombinedTransitionFunctionImpl(sequences, mergedStateChangeStatements);
}

@Override
Expand Down
3 changes: 1 addition & 2 deletions idealPDS/src/main/java/typestate/TransitionFunctionOne.java
Original file line number Diff line number Diff line change
Expand Up @@ -68,8 +68,7 @@ public Weight combineWith(@NonNull Weight other) {
result.putAll(transition, statement);
}

return new TransitionFunctionImpl(
func.getStateChangeSequences(), func.getStateChangeStatement());
return func.withStateChangeSequences(func.getStateChangeSequences());
}

public String toString() {
Expand Down
91 changes: 91 additions & 0 deletions idealPDS/src/test/java/typestate/TransitionFunctionImplTest.java
Original file line number Diff line number Diff line change
@@ -0,0 +1,91 @@
/**
* *****************************************************************************
* Copyright (c) 2018 Fraunhofer IEM, Paderborn, Germany
* <p>
* This program and the accompanying materials are made available under the
* terms of the Eclipse Public License 2.0 which is available at
* http://www.eclipse.org/legal/epl-2.0.
* <p>
* SPDX-License-Identifier: EPL-2.0
* <p>
* Contributors:
* Johannes Spaeth - initial API and implementation
* *****************************************************************************
*/
package typestate;

import static org.junit.jupiter.api.Assertions.assertEquals;
import static org.junit.jupiter.api.Assertions.assertInstanceOf;
import static org.junit.jupiter.api.Assertions.assertNotEquals;

import boomerang.scope.Method;
import boomerang.scope.Statement;
import boomerang.utils.MethodWrapper;
import java.util.Collections;
import org.junit.jupiter.api.Test;
import test.TestingFramework;
import wpds.impl.Weight;

public class TransitionFunctionImplTest {

@Test
public void testCombineWithCommutative() {
TestingFramework testingFramework = new TestingFramework();
testingFramework.getFrameworkScope(
new MethodWrapper(getClass().getName(), "testCombineWithCommutative"));
Method method = testingFramework.getTestMethod();
Statement first = method.getStatements().get(0);
Statement second = method.getStatements().get(1);
assertNotEquals(first, second);
TransitionFunctionImpl firstTransitionFunction =
new TransitionFunctionImpl(Collections.emptySet(), first);
TransitionFunctionImpl secondTransitionFunction =
new TransitionFunctionImpl(Collections.emptySet(), second);
assertNotEquals(firstTransitionFunction, secondTransitionFunction);
Weight firstSecondResult = firstTransitionFunction.combineWith(secondTransitionFunction);
Weight secondFirstResult = secondTransitionFunction.combineWith(firstTransitionFunction);
assertEquals(firstSecondResult, secondFirstResult);
// ensure that the behavior of getChangeStatement() is as in the
// non-commutative implementation (whether this behavior is "meaningful" is
// debatable, though)
assertEquals(
secondTransitionFunction.getStateChangeStatement(),
((TransitionFunctionImpl) firstSecondResult).getStateChangeStatement());
assertEquals(
firstTransitionFunction.getStateChangeStatement(),
((TransitionFunctionImpl) secondFirstResult).getStateChangeStatement());
}

@Test
public void testCombineWithIdempotentAndCommutativeForMoreStatements() {
TestingFramework testingFramework = new TestingFramework();
testingFramework.getFrameworkScope(
new MethodWrapper(
getClass().getName(), "testCombineWithIdempotentAndCommutativeForMoreStatements"));
Method method = testingFramework.getTestMethod();
TransitionFunctionImpl first =
new TransitionFunctionImpl(Collections.emptySet(), method.getStatements().get(0));
TransitionFunctionImpl second =
new TransitionFunctionImpl(Collections.emptySet(), method.getStatements().get(1));
TransitionFunctionImpl third =
new TransitionFunctionImpl(Collections.emptySet(), method.getStatements().get(2));

// combining a function with itself must not change it, and in particular must not turn it
// into a combined function
Weight firstFirst = first.combineWith(first);
assertEquals(first, firstFirst);
assertInstanceOf(TransitionFunctionImpl.class, firstFirst);
assertNotEquals(CombinedTransitionFunctionImpl.class, firstFirst.getClass());

Weight firstSecond = first.combineWith(second);
assertInstanceOf(CombinedTransitionFunctionImpl.class, firstSecond);
assertEquals(firstSecond, firstSecond.combineWith(first));
assertEquals(firstSecond, firstSecond.combineWith(firstSecond));

Weight left = firstSecond.combineWith(third);
Weight right = third.combineWith(second.combineWith(first));
assertEquals(left, right);
assertEquals(left.hashCode(), right.hashCode());
assertNotEquals(firstSecond, left);
}
}
22 changes: 22 additions & 0 deletions idealPDS/src/test/java/typestate/VectorTest.java
Original file line number Diff line number Diff line change
Expand Up @@ -119,4 +119,26 @@ public void staticAccessTest() {
v.firstElement();
Assertions.mustBeInErrorState(v);
}

public void doSth(Vector<Object> x, Object element) {
if (staticallyUnknown()) {
x.add(element);
} else {
element = x.elementAt(0);
}
}

@Test
@TestParameters(expectedSeedCount = 1, expectedAssertionCount = 1)
public void testNoStackOverflowDueToNonCommutativeCombineWith() {
Vector<Object> x = new Vector<>();
Object element = new Object();
x.add(element);
while (staticallyUnknown()) {
// the method call seems to be crucial for triggering the StackOverflowError
// (inlining the code from doSth does not trigger the error)
doSth(x, element);
}
Assertions.mustBeInAcceptingState(x);
}
}
Loading