diff --git a/src/main/java/me/paultristanwagner/modelchecking/automaton/GNBA.java b/src/main/java/me/paultristanwagner/modelchecking/automaton/GNBA.java index 3533d2d..7804886 100644 --- a/src/main/java/me/paultristanwagner/modelchecking/automaton/GNBA.java +++ b/src/main/java/me/paultristanwagner/modelchecking/automaton/GNBA.java @@ -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 states; - private final List alphabet; - private final List initialStates; - private final List> acceptingSets; - private final List transitions; + private final Set states; + private final Set alphabet; + private final Set initialStates; + private final Set> acceptingSets; + private final Set transitions; public GNBA( - List states, - List alphabet, - List initialStates, - List> acceptingSets, - List transitions) { + Set states, + Set alphabet, + Set initialStates, + Set> acceptingSets, + Set transitions) { this.states = states; this.alphabet = alphabet; this.initialStates = initialStates; @@ -79,7 +78,7 @@ public NBA convertToNBA() { } if (!acceptingSets.isEmpty()) { - List acceptingSet = acceptingSets.get(0); + Set acceptingSet = acceptingSets.stream().findFirst().get(); for (String acceptingState : acceptingSet) { String nbaAcceptingState = stringTuple(acceptingState, 1); builder.addAcceptingState(nbaAcceptingState); @@ -87,8 +86,8 @@ public NBA convertToNBA() { } for (NBATransition transition : transitions) { - for (int i = 0; i < acceptingSets.size(); i++) { - List acceptingSet = acceptingSets.get(i); + int i = 0; + for (Set acceptingSet : acceptingSets) { String nbaFrom = stringTuple(transition.getFrom(), i + 1); String nbaTo; if (acceptingSet.contains(transition.getFrom())) { @@ -97,6 +96,8 @@ public NBA convertToNBA() { nbaTo = stringTuple(transition.getTo(), (i + 1)); } builder.addTransition(nbaFrom, transition.getAction(), nbaTo); + + i++; } } @@ -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); } } @@ -143,23 +144,23 @@ public static GNBA fromJson(String json) { return GSON.fromJson(json, GNBA.class); } - public List getStates() { + public Set getStates() { return states; } - public List getInitialStates() { + public Set getInitialStates() { return initialStates; } - public List getAlphabet() { + public Set getAlphabet() { return alphabet; } - public List> getAcceptingSets() { + public Set> getAcceptingSets() { return acceptingSets; } - public List getTransitions() { + public Set getTransitions() { return transitions; } } diff --git a/src/main/java/me/paultristanwagner/modelchecking/automaton/GNBABuilder.java b/src/main/java/me/paultristanwagner/modelchecking/automaton/GNBABuilder.java index 3eebd52..76ab9d9 100644 --- a/src/main/java/me/paultristanwagner/modelchecking/automaton/GNBABuilder.java +++ b/src/main/java/me/paultristanwagner/modelchecking/automaton/GNBABuilder.java @@ -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 states; - private final List alphabet; - private final List initialStates; - private final List> acceptingSets; - private final List transitions; + private final Set states; + private final Set alphabet; + private final Set initialStates; + private final Set> acceptingSets; + private final Set 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) { @@ -33,7 +32,7 @@ public GNBABuilder addState(String state) { return this; } - public GNBABuilder setAlphabet(List alphabet) { + public GNBABuilder setAlphabet(Set alphabet) { this.alphabet.clear(); this.alphabet.addAll(alphabet); return this; @@ -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 acceptingSet) { - this.acceptingSets.add(new ArrayList<>(acceptingSet)); + this.acceptingSets.add(new HashSet<>(acceptingSet)); return this; } diff --git a/src/main/java/me/paultristanwagner/modelchecking/automaton/NBA.java b/src/main/java/me/paultristanwagner/modelchecking/automaton/NBA.java index 992f6cf..c41b514 100644 --- a/src/main/java/me/paultristanwagner/modelchecking/automaton/NBA.java +++ b/src/main/java/me/paultristanwagner/modelchecking/automaton/NBA.java @@ -19,18 +19,18 @@ public class NBA { .create(); } - private final List states; - private final List alphabet; - private final List initialStates; - private final List acceptingStates; - private final List transitions; + private final Set states; + private final Set alphabet; + private final Set initialStates; + private final Set acceptingStates; + private final Set transitions; public NBA( - List states, - List alphabet, - List initialStates, - List acceptingStates, - List transitions) { + Set states, + Set alphabet, + Set initialStates, + Set acceptingStates, + Set transitions) { this.states = states; this.alphabet = alphabet; this.initialStates = initialStates; @@ -138,13 +138,13 @@ public NBAEmptinessResult checkEmptiness() { } public GNBA toGNBA() { - List states = new ArrayList<>(this.states); - List alphabet = new ArrayList<>(this.alphabet); - List initialStates = new ArrayList<>(this.initialStates); - List transitions = new ArrayList<>(this.transitions); + Set states = new HashSet<>(this.states); + Set alphabet = new HashSet<>(this.alphabet); + Set initialStates = new HashSet<>(this.initialStates); + Set transitions = new HashSet<>(this.transitions); - List> acceptingSets = new ArrayList<>(); - acceptingSets.add(new ArrayList<>(this.acceptingStates)); + Set> acceptingSets = new HashSet<>(); + acceptingSets.add(new HashSet<>(this.acceptingStates)); return new GNBA(states, alphabet, initialStates, acceptingSets, transitions); } @@ -209,23 +209,23 @@ public static NBA fromJson(String json) { return GSON.fromJson(json, NBA.class); } - public List getStates() { + public Set getStates() { return states; } - public List getAlphabet() { + public Set getAlphabet() { return alphabet; } - public List getInitialStates() { + public Set getInitialStates() { return initialStates; } - public List getAcceptingStates() { + public Set getAcceptingStates() { return acceptingStates; } - public List getTransitions() { + public Set getTransitions() { return transitions; } } diff --git a/src/main/java/me/paultristanwagner/modelchecking/automaton/NBABuilder.java b/src/main/java/me/paultristanwagner/modelchecking/automaton/NBABuilder.java index 34527ce..640d9d4 100644 --- a/src/main/java/me/paultristanwagner/modelchecking/automaton/NBABuilder.java +++ b/src/main/java/me/paultristanwagner/modelchecking/automaton/NBABuilder.java @@ -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 states; - private final List alphabet; - private final List initialStates; - private final List acceptingStates; - private final List transitions; + private final Set states; + private final Set alphabet; + private final Set initialStates; + private final Set acceptingStates; + private final Set 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) { @@ -32,7 +32,7 @@ public NBABuilder addState(String state) { return this; } - public NBABuilder setAlphabet(List alphabet) { + public NBABuilder setAlphabet(Set alphabet) { this.alphabet.clear(); this.alphabet.addAll(alphabet); return this; diff --git a/src/main/java/me/paultristanwagner/modelchecking/ltl/BasicLTLModelChecker.java b/src/main/java/me/paultristanwagner/modelchecking/ltl/BasicLTLModelChecker.java index b19d61c..5df762b 100644 --- a/src/main/java/me/paultristanwagner/modelchecking/ltl/BasicLTLModelChecker.java +++ b/src/main/java/me/paultristanwagner/modelchecking/ltl/BasicLTLModelChecker.java @@ -198,8 +198,7 @@ public Set reduceClosure(Set closure) { return reduced; } - private Set computeElementarySets( - Set atomicPropositions, Set closure) { + private Set computeElementarySets(Set atomicPropositions, Set closure) { Set elementarySets = new HashSet<>(); // todo: figure out what to do with this @@ -224,14 +223,14 @@ private Set computeElementarySets( int n = reduced.size(); int m = 1 << n; - while(m > 0) { + while (m > 0) { m--; Set assumed = new HashSet<>(); int i = 0; for (LTLFormula f : reduced) { - if((m & (1 << i)) != 0) { + if ((m & (1 << i)) != 0) { assumed.add(f); } i++; diff --git a/src/main/java/me/paultristanwagner/modelchecking/ts/TransitionSystem.java b/src/main/java/me/paultristanwagner/modelchecking/ts/TransitionSystem.java index 0b12b78..cb04296 100644 --- a/src/main/java/me/paultristanwagner/modelchecking/ts/TransitionSystem.java +++ b/src/main/java/me/paultristanwagner/modelchecking/ts/TransitionSystem.java @@ -24,18 +24,18 @@ public class TransitionSystem { .create(); } - private final List states; - private final List transitions; - private final List initialStates; - private final List atomicPropositions; - private final Map> labelingFunction; + private final Set states; + private final Set transitions; + private final Set initialStates; + private final Set atomicPropositions; + private final Map> labelingFunction; public TransitionSystem( - List states, - List transitions, - List initialStates, - List atomicPropositions, - Map> labelingFunction) { + Set states, + Set transitions, + Set initialStates, + Set atomicPropositions, + Map> labelingFunction) { this.states = states; this.transitions = transitions; this.initialStates = initialStates; @@ -43,7 +43,7 @@ public TransitionSystem( this.labelingFunction = labelingFunction; for (String state : states) { - labelingFunction.putIfAbsent(state, List.of()); + labelingFunction.putIfAbsent(state, Set.of()); } } @@ -57,14 +57,14 @@ public void verifyNoNullLabels() { } public TransitionSystem copy() { - List states = new ArrayList<>(this.states); - List transitions = new ArrayList<>(this.transitions); - List initialStates = new ArrayList<>(this.initialStates); - List atomicPropositions = new ArrayList<>(this.atomicPropositions); + Set states = new HashSet<>(this.states); + Set transitions = new HashSet<>(this.transitions); + Set initialStates = new HashSet<>(this.initialStates); + Set atomicPropositions = new HashSet<>(this.atomicPropositions); - Map> labelingFunction = new HashMap<>(); + Map> labelingFunction = new HashMap<>(); this.labelingFunction.forEach( - (state, labels) -> labelingFunction.put(state, new ArrayList<>(labels))); + (state, labels) -> labelingFunction.put(state, new HashSet<>(labels))); return new TransitionSystem( states, transitions, initialStates, atomicPropositions, labelingFunction); @@ -79,7 +79,7 @@ public TransitionSystem reachableSynchronousProduct(NBA nba) { Queue> queue = new ArrayDeque<>(); for (String initialState : initialStates) { - List label = labelingFunction.get(initialState); + Set label = labelingFunction.get(initialState); for (NBATransition nbaTransition : nba.getTransitions()) { String q0 = nbaTransition.getFrom(); @@ -122,7 +122,7 @@ public TransitionSystem reachableSynchronousProduct(NBA nba) { List sSuccessors = getSuccessors(s); for (String sSuccessor : sSuccessors) { - List sSuccessorLabel = labelingFunction.get(sSuccessor); + Set sSuccessorLabel = labelingFunction.get(sSuccessor); String sSuccessorLabelString = sSuccessorLabel.toString(); Set qSuccessors = nba.getSuccessors(q, sSuccessorLabelString); for (String qSuccessor : qSuccessors) { @@ -201,7 +201,7 @@ public TSPersistenceResult checkPersistence(Set persistentStates) { pi.push(s1); } else { pi.pop(); - List labels = labelingFunction.get(s); + Set labels = labelingFunction.get(s); boolean notPersistentState = labels.stream().noneMatch(persistentStates::contains); @@ -244,11 +244,11 @@ public String toString() { return toJson(); } - public List getStates() { + public Set getStates() { return states; } - public List getInitialStates() { + public Set getInitialStates() { return initialStates; } @@ -260,7 +260,7 @@ public List getSuccessors(String state) { .toList(); } - public List getAtomicPropositions() { + public Set getAtomicPropositions() { return atomicPropositions; } @@ -268,7 +268,7 @@ public void addLabel(String state, String atomicProposition) { labelingFunction.get(state).add(atomicProposition); } - public List getLabel(String state) { + public Set getLabel(String state) { return labelingFunction.get(state); } diff --git a/src/main/java/me/paultristanwagner/modelchecking/ts/TransitionSystemBuilder.java b/src/main/java/me/paultristanwagner/modelchecking/ts/TransitionSystemBuilder.java index 9663586..85b5399 100644 --- a/src/main/java/me/paultristanwagner/modelchecking/ts/TransitionSystemBuilder.java +++ b/src/main/java/me/paultristanwagner/modelchecking/ts/TransitionSystemBuilder.java @@ -4,17 +4,17 @@ public class TransitionSystemBuilder { - private final List states; - private final List transitions; - private final List initialStates; - private final List atomicPropositions; - private final Map> labelingFunction; + private final Set states; + private final Set transitions; + private final Set initialStates; + private final Set atomicPropositions; + private final Map> labelingFunction; public TransitionSystemBuilder() { - this.states = new ArrayList<>(); - this.transitions = new ArrayList<>(); - this.initialStates = new ArrayList<>(); - this.atomicPropositions = new ArrayList<>(); + this.states = new HashSet<>(); + this.transitions = new HashSet<>(); + this.initialStates = new HashSet<>(); + this.atomicPropositions = new HashSet<>(); this.labelingFunction = new HashMap<>(); } @@ -62,14 +62,14 @@ public TransitionSystemBuilder addAtomicProposition(String atomicProposition) { } public TransitionSystemBuilder addLabel(String state, String atomicProposition) { - List labels = labelingFunction.computeIfAbsent(state, k -> new ArrayList<>()); + Set labels = labelingFunction.computeIfAbsent(state, k -> new HashSet<>()); labels.add(atomicProposition); return this; } public TransitionSystemBuilder addLabels(String state, String... atomicPropositions) { - List labels = labelingFunction.computeIfAbsent(state, k -> new ArrayList<>()); + Set labels = labelingFunction.computeIfAbsent(state, k -> new HashSet<>()); labels.addAll(Arrays.asList(atomicPropositions)); return this; @@ -80,7 +80,7 @@ public TransitionSystem build() { states, transitions, initialStates, atomicPropositions, labelingFunction); } - public List getInitialStates() { + public Set getInitialStates() { return initialStates; } }