Skip to content

Commit e368a91

Browse files
mtf90mtf90
committed
lambda: analyze counterexamples exhaustively
closes #144
1 parent 527f580 commit e368a91

7 files changed

Lines changed: 282 additions & 7 deletions

File tree

‎algorithms/active/lambda/pom.xml‎

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -65,6 +65,11 @@ limitations under the License.
6565
</dependency>
6666

6767
<!-- test -->
68+
<dependency>
69+
<groupId>de.learnlib</groupId>
70+
<artifactId>learnlib-drivers-simulator</artifactId>
71+
<scope>test</scope>
72+
</dependency>
6873
<dependency>
6974
<groupId>de.learnlib</groupId>
7075
<artifactId>learnlib-equivalence-oracles</artifactId>
@@ -116,6 +121,14 @@ limitations under the License.
116121
<argLine>@{argLine} --add-reads=de.learnlib.algorithm.lambda=net.automatalib.util</argLine>
117122
</configuration>
118123
</plugin>
124+
<plugin>
125+
<groupId>org.apache.maven.plugins</groupId>
126+
<artifactId>maven-failsafe-plugin</artifactId>
127+
<configuration>
128+
<!-- append to existing argLine to nicely work together with jacoco plugin -->
129+
<argLine>@{argLine} --add-reads=de.learnlib.algorithm.lambda=net.automatalib.util</argLine>
130+
</configuration>
131+
</plugin>
119132
</plugins>
120133
</pluginManagement>
121134
</build>

‎algorithms/active/lambda/src/main/java/de/learnlib/algorithm/lambda/lstar/AbstractLLambda.java‎

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -84,7 +84,7 @@ public boolean refineHypothesis(DefaultQuery<I, D> counterexample) {
8484
witnesses.add(counterexample);
8585
boolean refined = false;
8686

87-
while (MQUtil.isCounterexample(counterexample, getHypothesisModel())) {
87+
while (!witnesses.isEmpty()) {
8888
final DefaultQuery<I, D> witness = witnesses.getFirst();
8989

9090
if (witness.getOutput() == null) {
@@ -96,11 +96,10 @@ public boolean refineHypothesis(DefaultQuery<I, D> counterexample) {
9696
if (valid) {
9797
analyzeCounterexample(witness, witnesses);
9898
learnLoop();
99+
refined = true;
99100
} else {
100101
witnesses.pop();
101102
}
102-
103-
refined = true;
104103
}
105104

106105
assert size() == shortPrefixes.size();

‎algorithms/active/lambda/src/main/java/de/learnlib/algorithm/lambda/ttt/AbstractTTTLambda.java‎

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -31,11 +31,12 @@
3131
import de.learnlib.util.MQUtil;
3232
import net.automatalib.alphabet.Alphabet;
3333
import net.automatalib.alphabet.SupportsGrowingAlphabet;
34+
import net.automatalib.automaton.concept.FiniteRepresentation;
3435
import net.automatalib.automaton.concept.SuffixOutput;
3536
import net.automatalib.word.Word;
3637

3738
public abstract class AbstractTTTLambda<M extends SuffixOutput<I, D>, I, D>
38-
implements LearningAlgorithm<M, I, D>, SupportsGrowingAlphabet<I> {
39+
implements LearningAlgorithm<M, I, D>, SupportsGrowingAlphabet<I>, FiniteRepresentation {
3940

4041
private final MembershipOracle<I, D> ceqs;
4142
private final Alphabet<I> alphabet;
@@ -69,7 +70,7 @@ public boolean refineHypothesis(DefaultQuery<I, D> counterexample) {
6970
witnesses.add(counterexample);
7071
boolean refined = false;
7172

72-
while (MQUtil.isCounterexample(counterexample, getHypothesisModel())) {
73+
while (!witnesses.isEmpty()) {
7374
final DefaultQuery<I, D> witness = witnesses.getFirst();
7475

7576
if (witness.getOutput() == null) {
@@ -81,13 +82,13 @@ public boolean refineHypothesis(DefaultQuery<I, D> counterexample) {
8182
if (valid) {
8283
analyzeCounterexample(witness, witnesses);
8384
makeConsistent();
85+
refined = true;
8486
} else {
8587
witnesses.pop();
8688
}
87-
88-
refined = true;
8989
}
9090

91+
assert size() == dtree().leaves().size();
9192
return refined;
9293
}
9394

‎algorithms/active/lambda/src/main/java/de/learnlib/algorithm/lambda/ttt/dfa/TTTLambdaDFA.java‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -61,4 +61,9 @@ public DFA<?, I> getHypothesisModel() {
6161
protected AbstractDecisionTree<I, Boolean> dtree() {
6262
return dtree;
6363
}
64+
65+
@Override
66+
public int size() {
67+
return hypothesis.size();
68+
}
6469
}

‎algorithms/active/lambda/src/main/java/de/learnlib/algorithm/lambda/ttt/mealy/TTTLambdaMealy.java‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -65,4 +65,9 @@ protected DTLeaf<I, Word<O>> getState(Word<I> prefix) {
6565
protected AbstractDecisionTree<I, Word<O>> dtree() {
6666
return dtree;
6767
}
68+
69+
@Override
70+
public int size() {
71+
return hypothesis.size();
72+
}
6873
}

‎algorithms/active/lambda/src/test/java/de/learnlib/algorithm/lambda/lstar/mealy/it/LLambdaMealyIT.java‎

Lines changed: 65 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -15,11 +15,33 @@
1515
*/
1616
package de.learnlib.algorithm.lambda.lstar.mealy.it;
1717

18+
import java.io.IOException;
19+
import java.io.InputStream;
20+
import java.util.Collection;
21+
import java.util.Random;
22+
23+
import de.learnlib.algorithm.LearningAlgorithm.MealyLearner;
1824
import de.learnlib.algorithm.lambda.lstar.LLambdaMealy;
25+
import de.learnlib.driver.simulator.MealySimulatorSUL;
26+
import de.learnlib.oracle.EquivalenceOracle.MealyEquivalenceOracle;
1927
import de.learnlib.oracle.MembershipOracle.MealyMembershipOracle;
28+
import de.learnlib.oracle.equivalence.MealyRandomWpMethodEQOracle;
29+
import de.learnlib.oracle.membership.SULOracle;
30+
import de.learnlib.query.DefaultQuery;
2031
import de.learnlib.testsupport.it.learner.AbstractMealyLearnerIT;
2132
import de.learnlib.testsupport.it.learner.LearnerVariantList.MealyLearnerVariantList;
33+
import de.learnlib.util.Experiment.MealyExperiment;
34+
import de.learnlib.util.mealy.MealyUtil;
2235
import net.automatalib.alphabet.Alphabet;
36+
import net.automatalib.automaton.transducer.MealyMachine;
37+
import net.automatalib.automaton.transducer.impl.CompactMealy;
38+
import net.automatalib.exception.FormatException;
39+
import net.automatalib.serialization.dot.DOTInputModelData;
40+
import net.automatalib.serialization.dot.DOTParsers;
41+
import net.automatalib.util.automaton.Automata;
42+
import net.automatalib.word.Word;
43+
import org.checkerframework.checker.nullness.qual.Nullable;
44+
import org.testng.Assert;
2345
import org.testng.annotations.Test;
2446

2547
@Test
@@ -33,4 +55,47 @@ protected <I, O> void addLearnerVariants(Alphabet<I> alphabet,
3355
variants.addLearnerVariant("LLambdaMealy", new LLambdaMealy<>(alphabet, mqOracle));
3456
}
3557

58+
/**
59+
* Checks that the number of prefixes is equal to the number of hypothesis states. For details, see <a
60+
* href="https://github.com/LearnLib/learnlib/issues/144">issue 144</a>.
61+
*/
62+
@Test
63+
public void testIssue144() throws IOException, FormatException {
64+
65+
try (InputStream is = LLambdaMealyIT.class.getClassLoader()
66+
.getResourceAsStream("mosquitto__two_client_will_retain.dot")) {
67+
final DOTInputModelData<Integer, String, CompactMealy<String, String>> model =
68+
DOTParsers.mealy().readModel(is);
69+
final CompactMealy<String, String> mealy = model.model;
70+
final Alphabet<String> alphabet = model.alphabet;
71+
72+
final int seed = -1177788003;
73+
74+
final MealyMembershipOracle<String, String> mqo = new SULOracle<>(new MealySimulatorSUL<>(mealy));
75+
final MealyLearner<String, String> learner = new LLambdaMealy<>(alphabet, mqo);
76+
final MealyEquivalenceOracle<String, String> eqo =
77+
new ShorteningEQO<>(new MealyRandomWpMethodEQOracle<>(mqo, 0, 4, 10_000, new Random(seed), 1));
78+
79+
final MealyExperiment<String, String> experiment = new MealyExperiment<>(learner, eqo, alphabet);
80+
final MealyMachine<?, String, ?, String> hyp = experiment.run();
81+
82+
Assert.assertTrue(Automata.testEquivalence(mealy, hyp, alphabet));
83+
}
84+
}
85+
86+
private static final class ShorteningEQO<I, O> implements MealyEquivalenceOracle<I, O> {
87+
88+
private final MealyEquivalenceOracle<I, O> delegate;
89+
90+
private ShorteningEQO(MealyEquivalenceOracle<I, O> delegate) {
91+
this.delegate = delegate;
92+
}
93+
94+
@Override
95+
public @Nullable DefaultQuery<I, Word<O>> findCounterExample(MealyMachine<?, I, ?, O> hypothesis,
96+
Collection<? extends I> inputs) {
97+
DefaultQuery<I, Word<O>> ce = delegate.findCounterExample(hypothesis, inputs);
98+
return ce == null ? null : MealyUtil.shortenCounterExample(hypothesis, ce);
99+
}
100+
}
36101
}

‎algorithms/active/lambda/src/test/resources/mosquitto__two_client_will_retain.dot‎

Lines changed: 187 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,187 @@
1+
// from https://gitlab.com/felixwallner/learn-combinations/-/tree/master/input/mealy/principle/BenchmarkMQTT
2+
digraph g {
3+
__start0 [label="" shape="none"];
4+
5+
s0 [shape="circle" label="s0"];
6+
s1 [shape="circle" label="s1"];
7+
s2 [shape="circle" label="s2"];
8+
s3 [shape="circle" label="s3"];
9+
s4 [shape="circle" label="s4"];
10+
s5 [shape="circle" label="s5"];
11+
s6 [shape="circle" label="s6"];
12+
s7 [shape="circle" label="s7"];
13+
s8 [shape="circle" label="s8"];
14+
s9 [shape="circle" label="s9"];
15+
s10 [shape="circle" label="s10"];
16+
s11 [shape="circle" label="s11"];
17+
s12 [shape="circle" label="s12"];
18+
s13 [shape="circle" label="s13"];
19+
s14 [shape="circle" label="s14"];
20+
s15 [shape="circle" label="s15"];
21+
s16 [shape="circle" label="s16"];
22+
s17 [shape="circle" label="s17"];
23+
s0 -> s1 [label="ConnectC2 / c1_ConnectionClosed__c2_ConnAck"];
24+
s0 -> s3 [label="ConnectC1WithWill / c1_ConnAck__c2_ConnectionClosed"];
25+
s0 -> s7 [label="ConnectC1WithWillRetain / c1_ConnAck__c2_ConnectionClosed"];
26+
s0 -> s0 [label="DeleteRetainedC1 / c1_ConnectionClosed__c2_ConnectionClosed"];
27+
s0 -> s0 [label="DeleteRetainedC2 / c1_ConnectionClosed__c2_ConnectionClosed"];
28+
s0 -> s0 [label="SubscribeC2 / c1_ConnectionClosed__c2_ConnectionClosed"];
29+
s0 -> s0 [label="UnSubScribeC2 / c1_ConnectionClosed__c2_ConnectionClosed"];
30+
s0 -> s0 [label="DisconnectTCPC1 / c1_ConnectionClosed__c2_ConnectionClosed"];
31+
s0 -> s0 [label="DisconnectC1 / c1_ConnectionClosed__c2_ConnectionClosed"];
32+
s1 -> s0 [label="ConnectC2 / c1_ConnectionClosed__c2_ConnectionClosed"];
33+
s1 -> s2 [label="ConnectC1WithWill / c1_ConnAck__Empty"];
34+
s1 -> s6 [label="ConnectC1WithWillRetain / c1_ConnAck__Empty"];
35+
s1 -> s1 [label="DeleteRetainedC1 / c1_ConnectionClosed__Empty"];
36+
s1 -> s1 [label="DeleteRetainedC2 / c1_ConnectionClosed__c2_PubAck"];
37+
s1 -> s4 [label="SubscribeC2 / c1_ConnectionClosed__c2_SubAck"];
38+
s1 -> s1 [label="UnSubScribeC2 / c1_ConnectionClosed__c2_UnSubAck"];
39+
s1 -> s1 [label="DisconnectTCPC1 / c1_ConnectionClosed__Empty"];
40+
s1 -> s1 [label="DisconnectC1 / c1_ConnectionClosed__Empty"];
41+
s2 -> s3 [label="ConnectC2 / Empty__c2_ConnectionClosed"];
42+
s2 -> s1 [label="ConnectC1WithWill / c1_ConnectionClosed__Empty"];
43+
s2 -> s1 [label="ConnectC1WithWillRetain / c1_ConnectionClosed__Empty"];
44+
s2 -> s2 [label="DeleteRetainedC1 / c1_PubAck__Empty"];
45+
s2 -> s2 [label="DeleteRetainedC2 / Empty__c2_PubAck"];
46+
s2 -> s14 [label="SubscribeC2 / Empty__c2_SubAck"];
47+
s2 -> s2 [label="UnSubScribeC2 / Empty__c2_UnSubAck"];
48+
s2 -> s1 [label="DisconnectTCPC1 / c1_ConnectionClosed__Empty"];
49+
s2 -> s1 [label="DisconnectC1 / c1_ConnectionClosed__Empty"];
50+
s3 -> s2 [label="ConnectC2 / Empty__c2_ConnAck"];
51+
s3 -> s0 [label="ConnectC1WithWill / c1_ConnectionClosed__c2_ConnectionClosed"];
52+
s3 -> s0 [label="ConnectC1WithWillRetain / c1_ConnectionClosed__c2_ConnectionClosed"];
53+
s3 -> s3 [label="DeleteRetainedC1 / c1_PubAck__c2_ConnectionClosed"];
54+
s3 -> s3 [label="DeleteRetainedC2 / Empty__c2_ConnectionClosed"];
55+
s3 -> s3 [label="SubscribeC2 / Empty__c2_ConnectionClosed"];
56+
s3 -> s3 [label="UnSubScribeC2 / Empty__c2_ConnectionClosed"];
57+
s3 -> s0 [label="DisconnectTCPC1 / c1_ConnectionClosed__c2_ConnectionClosed"];
58+
s3 -> s0 [label="DisconnectC1 / c1_ConnectionClosed__c2_ConnectionClosed"];
59+
s4 -> s0 [label="ConnectC2 / c1_ConnectionClosed__c2_ConnectionClosed"];
60+
s4 -> s14 [label="ConnectC1WithWill / c1_ConnAck__Empty"];
61+
s4 -> s5 [label="ConnectC1WithWillRetain / c1_ConnAck__Empty"];
62+
s4 -> s4 [label="DeleteRetainedC1 / c1_ConnectionClosed__Empty"];
63+
s4 -> s4 [label="DeleteRetainedC2 / c1_ConnectionClosed__Pub(c2,my_topic,)__c2_PubAck"];
64+
s4 -> s4 [label="SubscribeC2 / c1_ConnectionClosed__c2_SubAck"];
65+
s4 -> s1 [label="UnSubScribeC2 / c1_ConnectionClosed__c2_UnSubAck"];
66+
s4 -> s4 [label="DisconnectTCPC1 / c1_ConnectionClosed__Empty"];
67+
s4 -> s4 [label="DisconnectC1 / c1_ConnectionClosed__Empty"];
68+
s5 -> s7 [label="ConnectC2 / Empty__c2_ConnectionClosed"];
69+
s5 -> s12 [label="ConnectC1WithWill / c1_ConnectionClosed__Pub(c2,my_topic,bye)"];
70+
s5 -> s12 [label="ConnectC1WithWillRetain / c1_ConnectionClosed__Pub(c2,my_topic,bye)"];
71+
s5 -> s5 [label="DeleteRetainedC1 / c1_PubAck__Pub(c2,my_topic,)"];
72+
s5 -> s5 [label="DeleteRetainedC2 / Empty__Pub(c2,my_topic,)__c2_PubAck"];
73+
s5 -> s5 [label="SubscribeC2 / Empty__c2_SubAck"];
74+
s5 -> s6 [label="UnSubScribeC2 / Empty__c2_UnSubAck"];
75+
s5 -> s12 [label="DisconnectTCPC1 / c1_ConnectionClosed__Pub(c2,my_topic,bye)"];
76+
s5 -> s4 [label="DisconnectC1 / c1_ConnectionClosed__Empty"];
77+
s6 -> s7 [label="ConnectC2 / Empty__c2_ConnectionClosed"];
78+
s6 -> s9 [label="ConnectC1WithWill / c1_ConnectionClosed__Empty"];
79+
s6 -> s9 [label="ConnectC1WithWillRetain / c1_ConnectionClosed__Empty"];
80+
s6 -> s6 [label="DeleteRetainedC1 / c1_PubAck__Empty"];
81+
s6 -> s6 [label="DeleteRetainedC2 / Empty__c2_PubAck"];
82+
s6 -> s5 [label="SubscribeC2 / Empty__c2_SubAck"];
83+
s6 -> s6 [label="UnSubScribeC2 / Empty__c2_UnSubAck"];
84+
s6 -> s9 [label="DisconnectTCPC1 / c1_ConnectionClosed__Empty"];
85+
s6 -> s1 [label="DisconnectC1 / c1_ConnectionClosed__Empty"];
86+
s7 -> s6 [label="ConnectC2 / Empty__c2_ConnAck"];
87+
s7 -> s8 [label="ConnectC1WithWill / c1_ConnectionClosed__c2_ConnectionClosed"];
88+
s7 -> s8 [label="ConnectC1WithWillRetain / c1_ConnectionClosed__c2_ConnectionClosed"];
89+
s7 -> s7 [label="DeleteRetainedC1 / c1_PubAck__c2_ConnectionClosed"];
90+
s7 -> s7 [label="DeleteRetainedC2 / Empty__c2_ConnectionClosed"];
91+
s7 -> s7 [label="SubscribeC2 / Empty__c2_ConnectionClosed"];
92+
s7 -> s7 [label="UnSubScribeC2 / Empty__c2_ConnectionClosed"];
93+
s7 -> s8 [label="DisconnectTCPC1 / c1_ConnectionClosed__c2_ConnectionClosed"];
94+
s7 -> s0 [label="DisconnectC1 / c1_ConnectionClosed__c2_ConnectionClosed"];
95+
s8 -> s9 [label="ConnectC2 / c1_ConnectionClosed__c2_ConnAck"];
96+
s8 -> s10 [label="ConnectC1WithWill / c1_ConnAck__c2_ConnectionClosed"];
97+
s8 -> s16 [label="ConnectC1WithWillRetain / c1_ConnAck__c2_ConnectionClosed"];
98+
s8 -> s8 [label="DeleteRetainedC1 / c1_ConnectionClosed__c2_ConnectionClosed"];
99+
s8 -> s8 [label="DeleteRetainedC2 / c1_ConnectionClosed__c2_ConnectionClosed"];
100+
s8 -> s8 [label="SubscribeC2 / c1_ConnectionClosed__c2_ConnectionClosed"];
101+
s8 -> s8 [label="UnSubScribeC2 / c1_ConnectionClosed__c2_ConnectionClosed"];
102+
s8 -> s8 [label="DisconnectTCPC1 / c1_ConnectionClosed__c2_ConnectionClosed"];
103+
s8 -> s8 [label="DisconnectC1 / c1_ConnectionClosed__c2_ConnectionClosed"];
104+
s9 -> s8 [label="ConnectC2 / c1_ConnectionClosed__c2_ConnectionClosed"];
105+
s9 -> s11 [label="ConnectC1WithWill / c1_ConnAck__Empty"];
106+
s9 -> s17 [label="ConnectC1WithWillRetain / c1_ConnAck__Empty"];
107+
s9 -> s9 [label="DeleteRetainedC1 / c1_ConnectionClosed__Empty"];
108+
s9 -> s1 [label="DeleteRetainedC2 / c1_ConnectionClosed__c2_PubAck"];
109+
s9 -> s12 [label="SubscribeC2 / c1_ConnectionClosed__c2_SubAck__Pub(c2,my_topic,bye)"];
110+
s9 -> s9 [label="UnSubScribeC2 / c1_ConnectionClosed__c2_UnSubAck"];
111+
s9 -> s9 [label="DisconnectTCPC1 / c1_ConnectionClosed__Empty"];
112+
s9 -> s9 [label="DisconnectC1 / c1_ConnectionClosed__Empty"];
113+
s10 -> s11 [label="ConnectC2 / Empty__c2_ConnAck"];
114+
s10 -> s8 [label="ConnectC1WithWill / c1_ConnectionClosed__c2_ConnectionClosed"];
115+
s10 -> s8 [label="ConnectC1WithWillRetain / c1_ConnectionClosed__c2_ConnectionClosed"];
116+
s10 -> s3 [label="DeleteRetainedC1 / c1_PubAck__c2_ConnectionClosed"];
117+
s10 -> s10 [label="DeleteRetainedC2 / Empty__c2_ConnectionClosed"];
118+
s10 -> s10 [label="SubscribeC2 / Empty__c2_ConnectionClosed"];
119+
s10 -> s10 [label="UnSubScribeC2 / Empty__c2_ConnectionClosed"];
120+
s10 -> s8 [label="DisconnectTCPC1 / c1_ConnectionClosed__c2_ConnectionClosed"];
121+
s10 -> s8 [label="DisconnectC1 / c1_ConnectionClosed__c2_ConnectionClosed"];
122+
s11 -> s10 [label="ConnectC2 / Empty__c2_ConnectionClosed"];
123+
s11 -> s9 [label="ConnectC1WithWill / c1_ConnectionClosed__Empty"];
124+
s11 -> s9 [label="ConnectC1WithWillRetain / c1_ConnectionClosed__Empty"];
125+
s11 -> s2 [label="DeleteRetainedC1 / c1_PubAck__Empty"];
126+
s11 -> s2 [label="DeleteRetainedC2 / Empty__c2_PubAck"];
127+
s11 -> s15 [label="SubscribeC2 / Empty__c2_SubAck__Pub(c2,my_topic,bye)"];
128+
s11 -> s11 [label="UnSubScribeC2 / Empty__c2_UnSubAck"];
129+
s11 -> s9 [label="DisconnectTCPC1 / c1_ConnectionClosed__Empty"];
130+
s11 -> s9 [label="DisconnectC1 / c1_ConnectionClosed__Empty"];
131+
s12 -> s8 [label="ConnectC2 / c1_ConnectionClosed__c2_ConnectionClosed"];
132+
s12 -> s15 [label="ConnectC1WithWill / c1_ConnAck__Empty"];
133+
s12 -> s13 [label="ConnectC1WithWillRetain / c1_ConnAck__Empty"];
134+
s12 -> s12 [label="DeleteRetainedC1 / c1_ConnectionClosed__Empty"];
135+
s12 -> s4 [label="DeleteRetainedC2 / c1_ConnectionClosed__Pub(c2,my_topic,)__c2_PubAck"];
136+
s12 -> s12 [label="SubscribeC2 / c1_ConnectionClosed__c2_SubAck__Pub(c2,my_topic,bye)"];
137+
s12 -> s9 [label="UnSubScribeC2 / c1_ConnectionClosed__c2_UnSubAck"];
138+
s12 -> s12 [label="DisconnectTCPC1 / c1_ConnectionClosed__Empty"];
139+
s12 -> s12 [label="DisconnectC1 / c1_ConnectionClosed__Empty"];
140+
s13 -> s16 [label="ConnectC2 / Empty__c2_ConnectionClosed"];
141+
s13 -> s12 [label="ConnectC1WithWill / c1_ConnectionClosed__Pub(c2,my_topic,bye)"];
142+
s13 -> s12 [label="ConnectC1WithWillRetain / c1_ConnectionClosed__Pub(c2,my_topic,bye)"];
143+
s13 -> s5 [label="DeleteRetainedC1 / c1_PubAck__Pub(c2,my_topic,)"];
144+
s13 -> s5 [label="DeleteRetainedC2 / Empty__Pub(c2,my_topic,)__c2_PubAck"];
145+
s13 -> s13 [label="SubscribeC2 / Empty__c2_SubAck__Pub(c2,my_topic,bye)"];
146+
s13 -> s17 [label="UnSubScribeC2 / Empty__c2_UnSubAck"];
147+
s13 -> s12 [label="DisconnectTCPC1 / c1_ConnectionClosed__Pub(c2,my_topic,bye)"];
148+
s13 -> s12 [label="DisconnectC1 / c1_ConnectionClosed__Empty"];
149+
s14 -> s3 [label="ConnectC2 / Empty__c2_ConnectionClosed"];
150+
s14 -> s4 [label="ConnectC1WithWill / c1_ConnectionClosed__Pub(c2,my_topic,bye)"];
151+
s14 -> s4 [label="ConnectC1WithWillRetain / c1_ConnectionClosed__Pub(c2,my_topic,bye)"];
152+
s14 -> s14 [label="DeleteRetainedC1 / c1_PubAck__Pub(c2,my_topic,)"];
153+
s14 -> s14 [label="DeleteRetainedC2 / Empty__Pub(c2,my_topic,)__c2_PubAck"];
154+
s14 -> s14 [label="SubscribeC2 / Empty__c2_SubAck"];
155+
s14 -> s2 [label="UnSubScribeC2 / Empty__c2_UnSubAck"];
156+
s14 -> s4 [label="DisconnectTCPC1 / c1_ConnectionClosed__Pub(c2,my_topic,bye)"];
157+
s14 -> s4 [label="DisconnectC1 / c1_ConnectionClosed__Empty"];
158+
s15 -> s10 [label="ConnectC2 / Empty__c2_ConnectionClosed"];
159+
s15 -> s12 [label="ConnectC1WithWill / c1_ConnectionClosed__Pub(c2,my_topic,bye)"];
160+
s15 -> s12 [label="ConnectC1WithWillRetain / c1_ConnectionClosed__Pub(c2,my_topic,bye)"];
161+
s15 -> s14 [label="DeleteRetainedC1 / c1_PubAck__Pub(c2,my_topic,)"];
162+
s15 -> s14 [label="DeleteRetainedC2 / Empty__Pub(c2,my_topic,)__c2_PubAck"];
163+
s15 -> s15 [label="SubscribeC2 / Empty__c2_SubAck__Pub(c2,my_topic,bye)"];
164+
s15 -> s11 [label="UnSubScribeC2 / Empty__c2_UnSubAck"];
165+
s15 -> s12 [label="DisconnectTCPC1 / c1_ConnectionClosed__Pub(c2,my_topic,bye)"];
166+
s15 -> s12 [label="DisconnectC1 / c1_ConnectionClosed__Empty"];
167+
s16 -> s17 [label="ConnectC2 / Empty__c2_ConnAck"];
168+
s16 -> s8 [label="ConnectC1WithWill / c1_ConnectionClosed__c2_ConnectionClosed"];
169+
s16 -> s8 [label="ConnectC1WithWillRetain / c1_ConnectionClosed__c2_ConnectionClosed"];
170+
s16 -> s7 [label="DeleteRetainedC1 / c1_PubAck__c2_ConnectionClosed"];
171+
s16 -> s16 [label="DeleteRetainedC2 / Empty__c2_ConnectionClosed"];
172+
s16 -> s16 [label="SubscribeC2 / Empty__c2_ConnectionClosed"];
173+
s16 -> s16 [label="UnSubScribeC2 / Empty__c2_ConnectionClosed"];
174+
s16 -> s8 [label="DisconnectTCPC1 / c1_ConnectionClosed__c2_ConnectionClosed"];
175+
s16 -> s8 [label="DisconnectC1 / c1_ConnectionClosed__c2_ConnectionClosed"];
176+
s17 -> s16 [label="ConnectC2 / Empty__c2_ConnectionClosed"];
177+
s17 -> s9 [label="ConnectC1WithWill / c1_ConnectionClosed__Empty"];
178+
s17 -> s9 [label="ConnectC1WithWillRetain / c1_ConnectionClosed__Empty"];
179+
s17 -> s6 [label="DeleteRetainedC1 / c1_PubAck__Empty"];
180+
s17 -> s6 [label="DeleteRetainedC2 / Empty__c2_PubAck"];
181+
s17 -> s13 [label="SubscribeC2 / Empty__c2_SubAck__Pub(c2,my_topic,bye)"];
182+
s17 -> s17 [label="UnSubScribeC2 / Empty__c2_UnSubAck"];
183+
s17 -> s9 [label="DisconnectTCPC1 / c1_ConnectionClosed__Empty"];
184+
s17 -> s9 [label="DisconnectC1 / c1_ConnectionClosed__Empty"];
185+
186+
__start0 -> s0;
187+
}

0 commit comments

Comments
 (0)