Skip to content

Commit

Permalink
Use sets instead of lists
Browse files Browse the repository at this point in the history
  • Loading branch information
@paultristanwagner
paultristanwagner committed Oct 2, 2023
1 parent 87a7f7e commit fe67275
Show file tree
Hide file tree
Showing 7 changed files with 107 additions and 113 deletions.
41 changes: 21 additions & 20 deletions src/main/java/me/paultristanwagner/modelchecking/automaton/GNBA.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,24 +5,23 @@
import com.google.gson.Gson;
import com.google.gson.GsonBuilder;
import java.util.HashSet;
import java.util.List;
import java.util.Set;

public final class GNBA {

private static final Gson GSON;
private final List<String> states;
private final List<String> alphabet;
private final List<String> initialStates;
private final List<List<String>> acceptingSets;
private final List<NBATransition> transitions;
private final Set<String> states;
private final Set<String> alphabet;
private final Set<String> initialStates;
private final Set<Set<String>> acceptingSets;
private final Set<NBATransition> transitions;

public GNBA(
List<String> states,
List<String> alphabet,
List<String> initialStates,
List<List<String>> acceptingSets,
List<NBATransition> transitions) {
Set<String> states,
Set<String> alphabet,
Set<String> initialStates,
Set<Set<String>> acceptingSets,
Set<NBATransition> transitions) {
this.states = states;
this.alphabet = alphabet;
this.initialStates = initialStates;
Expand Down Expand Up @@ -79,16 +78,16 @@ public NBA convertToNBA() {
}

if (!acceptingSets.isEmpty()) {
List<String> acceptingSet = acceptingSets.get(0);
Set<String> acceptingSet = acceptingSets.stream().findFirst().get();
for (String acceptingState : acceptingSet) {
String nbaAcceptingState = stringTuple(acceptingState, 1);
builder.addAcceptingState(nbaAcceptingState);
}
}

for (NBATransition transition : transitions) {
for (int i = 0; i < acceptingSets.size(); i++) {
List<String> acceptingSet = acceptingSets.get(i);
int i = 0;
for (Set<String> acceptingSet : acceptingSets) {
String nbaFrom = stringTuple(transition.getFrom(), i + 1);
String nbaTo;
if (acceptingSet.contains(transition.getFrom())) {
Expand All @@ -97,6 +96,8 @@ public NBA convertToNBA() {
nbaTo = stringTuple(transition.getTo(), (i + 1));
}
builder.addTransition(nbaFrom, transition.getAction(), nbaTo);

i++;
}
}

Expand All @@ -123,7 +124,7 @@ private NBA getCanonicalNBA() {
builder.addAcceptingState(state);
}
} else {
for (String acceptingState : acceptingSets.get(0)) {
for (String acceptingState : acceptingSets.stream().findFirst().get()) {
builder.addAcceptingState(acceptingState);
}
}
Expand All @@ -143,23 +144,23 @@ public static GNBA fromJson(String json) {
return GSON.fromJson(json, GNBA.class);
}

public List<String> getStates() {
public Set<String> getStates() {
return states;
}

public List<String> getInitialStates() {
public Set<String> getInitialStates() {
return initialStates;
}

public List<String> getAlphabet() {
public Set<String> getAlphabet() {
return alphabet;
}

public List<List<String>> getAcceptingSets() {
public Set<Set<String>> getAcceptingSets() {
return acceptingSets;
}

public List<NBATransition> getTransitions() {
public Set<NBATransition> getTransitions() {
return transitions;
}
}
32 changes: 13 additions & 19 deletions src/main/java/me/paultristanwagner/modelchecking/automaton/GNBABuilder.java
View file
Original file line number Diff line number Diff line change
@@ -1,23 +1,22 @@
package me.paultristanwagner.modelchecking.automaton;

import java.util.ArrayList;
import java.util.List;
import java.util.HashSet;
import java.util.Set;

public class GNBABuilder {

private final List<String> states;
private final List<String> alphabet;
private final List<String> initialStates;
private final List<List<String>> acceptingSets;
private final List<NBATransition> transitions;
private final Set<String> states;
private final Set<String> alphabet;
private final Set<String> initialStates;
private final Set<Set<String>> acceptingSets;
private final Set<NBATransition> transitions;

public GNBABuilder() {
this.states = new ArrayList<>();
this.alphabet = new ArrayList<>();
this.initialStates = new ArrayList<>();
this.acceptingSets = new ArrayList<>();
this.transitions = new ArrayList<>();
this.states = new HashSet<>();
this.alphabet = new HashSet<>();
this.initialStates = new HashSet<>();
this.acceptingSets = new HashSet<>();
this.transitions = new HashSet<>();
}

public GNBABuilder addStates(String... states) {
Expand All @@ -33,7 +32,7 @@ public GNBABuilder addState(String state) {
return this;
}

public GNBABuilder setAlphabet(List<String> alphabet) {
public GNBABuilder setAlphabet(Set<String> alphabet) {
this.alphabet.clear();
this.alphabet.addAll(alphabet);
return this;
Expand All @@ -44,13 +43,8 @@ public GNBABuilder addInitialState(String initialState) {
return this;
}

public GNBABuilder addAcceptingSet(String... acceptingSet) {
this.acceptingSets.add(List.of(acceptingSet));
return this;
}

public GNBABuilder addAcceptingSet(Set<String> acceptingSet) {
this.acceptingSets.add(new ArrayList<>(acceptingSet));
this.acceptingSets.add(new HashSet<>(acceptingSet));
return this;
}

Expand Down
42 changes: 21 additions & 21 deletions src/main/java/me/paultristanwagner/modelchecking/automaton/NBA.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -19,18 +19,18 @@ public class NBA {
.create();
}

private final List<String> states;
private final List<String> alphabet;
private final List<String> initialStates;
private final List<String> acceptingStates;
private final List<NBATransition> transitions;
private final Set<String> states;
private final Set<String> alphabet;
private final Set<String> initialStates;
private final Set<String> acceptingStates;
private final Set<NBATransition> transitions;

public NBA(
List<String> states,
List<String> alphabet,
List<String> initialStates,
List<String> acceptingStates,
List<NBATransition> transitions) {
Set<String> states,
Set<String> alphabet,
Set<String> initialStates,
Set<String> acceptingStates,
Set<NBATransition> transitions) {
this.states = states;
this.alphabet = alphabet;
this.initialStates = initialStates;
Expand Down Expand Up @@ -138,13 +138,13 @@ public NBAEmptinessResult checkEmptiness() {
}

public GNBA toGNBA() {
List<String> states = new ArrayList<>(this.states);
List<String> alphabet = new ArrayList<>(this.alphabet);
List<String> initialStates = new ArrayList<>(this.initialStates);
List<NBATransition> transitions = new ArrayList<>(this.transitions);
Set<String> states = new HashSet<>(this.states);
Set<String> alphabet = new HashSet<>(this.alphabet);
Set<String> initialStates = new HashSet<>(this.initialStates);
Set<NBATransition> transitions = new HashSet<>(this.transitions);

List<List<String>> acceptingSets = new ArrayList<>();
acceptingSets.add(new ArrayList<>(this.acceptingStates));
Set<Set<String>> acceptingSets = new HashSet<>();
acceptingSets.add(new HashSet<>(this.acceptingStates));

return new GNBA(states, alphabet, initialStates, acceptingSets, transitions);
}
Expand Down Expand Up @@ -209,23 +209,23 @@ public static NBA fromJson(String json) {
return GSON.fromJson(json, NBA.class);
}

public List<String> getStates() {
public Set<String> getStates() {
return states;
}

public List<String> getAlphabet() {
public Set<String> getAlphabet() {
return alphabet;
}

public List<String> getInitialStates() {
public Set<String> getInitialStates() {
return initialStates;
}

public List<String> getAcceptingStates() {
public Set<String> getAcceptingStates() {
return acceptingStates;
}

public List<NBATransition> getTransitions() {
public Set<NBATransition> getTransitions() {
return transitions;
}
}
26 changes: 13 additions & 13 deletions src/main/java/me/paultristanwagner/modelchecking/automaton/NBABuilder.java
View file
Original file line number Diff line number Diff line change
@@ -1,22 +1,22 @@
package me.paultristanwagner.modelchecking.automaton;

import java.util.ArrayList;
import java.util.List;
import java.util.HashSet;
import java.util.Set;

public class NBABuilder {

private final List<String> states;
private final List<String> alphabet;
private final List<String> initialStates;
private final List<String> acceptingStates;
private final List<NBATransition> transitions;
private final Set<String> states;
private final Set<String> alphabet;
private final Set<String> initialStates;
private final Set<String> acceptingStates;
private final Set<NBATransition> transitions;

public NBABuilder() {
this.states = new ArrayList<>();
this.alphabet = new ArrayList<>();
this.initialStates = new ArrayList<>();
this.acceptingStates = new ArrayList<>();
this.transitions = new ArrayList<>();
this.states = new HashSet<>();
this.alphabet = new HashSet<>();
this.initialStates = new HashSet<>();
this.acceptingStates = new HashSet<>();
this.transitions = new HashSet<>();
}

public NBABuilder addStates(String... states) {
Expand All @@ -32,7 +32,7 @@ public NBABuilder addState(String state) {
return this;
}

public NBABuilder setAlphabet(List<String> alphabet) {
public NBABuilder setAlphabet(Set<String> alphabet) {
this.alphabet.clear();
this.alphabet.addAll(alphabet);
return this;
Expand Down
7 changes: 3 additions & 4 deletions src/main/java/me/paultristanwagner/modelchecking/ltl/BasicLTLModelChecker.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -198,8 +198,7 @@ public Set<LTLFormula> reduceClosure(Set<LTLFormula> closure) {
return reduced;
}

private Set<B> computeElementarySets(
Set<String> atomicPropositions, Set<LTLFormula> closure) {
private Set<B> computeElementarySets(Set<String> atomicPropositions, Set<LTLFormula> closure) {
Set<B> elementarySets = new HashSet<>();

// todo: figure out what to do with this
Expand All @@ -224,14 +223,14 @@ private Set<B> computeElementarySets(

int n = reduced.size();
int m = 1 << n;
while(m > 0) {
while (m > 0) {
m--;

Set<LTLFormula> assumed = new HashSet<>();

int i = 0;
for (LTLFormula f : reduced) {
if((m & (1 << i)) != 0) {
if ((m & (1 << i)) != 0) {
assumed.add(f);
}
i++;
Expand Down
Loading

0 comments on commit fe67275

Please sign in to comment.