diff --git a/README.md b/README.md index a72dff9..69abb7c 100644 --- a/README.md +++ b/README.md @@ -33,25 +33,23 @@ Example: See examples/ts0.json ``` { - "states": ["s0","s1","s2","s3","s4"], - "transitions": [ - ["s0","s1"], - ["s1","s2"], - ["s2","s3"], - ["s3","s3"], - ["s3","s0"], - ["s0","s4"], - ["s4","s4"] - ], - "initialStates": ["s0","s3"], - "atomicPropositions": ["a","b"], - "labelingFunction": { - "s0": [], - "s1": ["a"], - "s2": ["a","b"], - "s3": ["b"], - "s4": ["b"] - } + "states": ["s0", "s1", "s2", "s3", "s4"], + "initialStates": ["s0", "s3"], + "successors": { + "s0": ["s1", "s4"], + "s1": ["s2"], + "s2": ["s3"], + "s3": ["s0", "s3"], + "s4": ["s4"] + }, + "atomicPropositions": ["a", "b"], + "labelingFunction": { + "s0": [], + "s1": ["a"], + "s2": ["a", "b"], + "s3": ["b"], + "s4": ["b"] + } } ``` diff --git a/examples/etest8_5.json b/examples/etest8_5.json index 067bfc1..5c4f5d1 100644 --- a/examples/etest8_5.json +++ b/examples/etest8_5.json @@ -1,54 +1,17 @@ { - "states": [ - "s1", - "s2", - "s3", - "s4" - ], - "transitions": [ - [ - "s1", - "s2" - ], - [ - "s1", - "s3" - ], - [ - "s2", - "s4" - ], - [ - "s3", - "s1" - ], - [ - "s3", - "s4" - ], - [ - "s4", - "s1" - ] - ], - "initialStates": [ - "s1" - ], - "atomicPropositions": [ - "a", - "b" - ], + "states": ["s1", "s2", "s3", "s4"], + "initialStates": ["s1"], + "successors": { + "s1": ["s2", "s3"], + "s2": ["s4"], + "s3": ["s1", "s4"], + "s4": ["s1"] + }, + "atomicPropositions": ["a", "b"], "labelingFunction": { - "s3": [ - "b" - ], - "s4": [ - "a", - "b" - ], "s1": [], - "s2": [ - "a" - ] + "s2": ["a"], + "s3": ["b"], + "s4": ["a", "b"] } } \ No newline at end of file diff --git a/examples/ts0.json b/examples/ts0.json index 605201d..28c1c49 100644 --- a/examples/ts0.json +++ b/examples/ts0.json @@ -1,63 +1,19 @@ { - "states": [ - "s0", - "s1", - "s2", - "s3", - "s4" - ], - "transitions": [ - [ - "s0", - "s1" - ], - [ - "s1", - "s2" - ], - [ - "s2", - "s3" - ], - [ - "s3", - "s3" - ], - [ - "s3", - "s0" - ], - [ - "s0", - "s4" - ], - [ - "s4", - "s4" - ] - ], - "initialStates": [ - "s0", - "s3" - ], - "atomicPropositions": [ - "a", - "b" - ], + "states": ["s0", "s1", "s2", "s3", "s4"], + "initialStates": ["s0", "s3"], + "successors": { + "s0": ["s1", "s4"], + "s1": ["s2"], + "s2": ["s3"], + "s3": ["s0", "s3"], + "s4": ["s4"] + }, + "atomicPropositions": ["a", "b"], "labelingFunction": { "s0": [], - "s1": [ - "a" - ], - "s2": [ - "a", - "b" - ], - "s3": [ - "b" - ], - "s4": [ - "b" - ] + "s1": ["a"], + "s2": ["a", "b"], + "s3": ["b"], + "s4": ["b"] } } \ No newline at end of file diff --git a/examples/ts1.json b/examples/ts1.json index f1f9a0f..b9638be 100644 --- a/examples/ts1.json +++ b/examples/ts1.json @@ -1,38 +1,15 @@ { - "states": [ - "s0", - "s1", - "s2" - ], - "transitions": [ - [ - "s0", - "s1" - ], - [ - "s0", - "s2" - ], - [ - "s1", - "s1" - ], - [ - "s2", - "s2" - ] - ], - "initialStates": [ - "s0" - ], - "atomicPropositions": [ - "a" - ], + "states": ["s0", "s1", "s2"], + "initialStates": ["s0"], + "successors": { + "s0": ["s1", "s2"], + "s1": ["s1"], + "s2": ["s2"] + }, + "atomicPropositions": ["a"], "labelingFunction": { "s0": [], - "s1": [ - "a" - ], + "s1": ["a"], "s2": [] } } \ No newline at end of file diff --git a/src/main/java/me/paultristanwagner/modelchecking/Main.java b/src/main/java/me/paultristanwagner/modelchecking/Main.java index 25f25cc..0d0fd69 100644 --- a/src/main/java/me/paultristanwagner/modelchecking/Main.java +++ b/src/main/java/me/paultristanwagner/modelchecking/Main.java @@ -2,8 +2,8 @@ import static java.nio.charset.StandardCharsets.UTF_8; import static me.paultristanwagner.modelchecking.util.AnsiColor.*; -import static me.paultristanwagner.modelchecking.util.Symbol.MODELS_SYMBOL; -import static me.paultristanwagner.modelchecking.util.Symbol.NOT_MODELS_SYMBOL; +import static me.paultristanwagner.modelchecking.util.Symbol.MODELS; +import static me.paultristanwagner.modelchecking.util.Symbol.NOT_MODELS; import com.google.gson.JsonSyntaxException; import java.io.*; @@ -26,8 +26,8 @@ import me.paultristanwagner.modelchecking.ltl.formula.LTLFormula; import me.paultristanwagner.modelchecking.ltl.parse.LTLParser; import me.paultristanwagner.modelchecking.parse.SyntaxError; +import me.paultristanwagner.modelchecking.ts.BasicTransitionSystem; import me.paultristanwagner.modelchecking.ts.CyclePath; -import me.paultristanwagner.modelchecking.ts.TransitionSystem; import me.paultristanwagner.modelchecking.ts.TransitionSystemLoader; import me.paultristanwagner.modelchecking.util.Symbol; @@ -38,7 +38,7 @@ public class Main { public static final Scanner SCANNER = new Scanner(System.in); public static void main(String[] args) { - TransitionSystem ts = enterTransitionSystem(); + BasicTransitionSystem ts = enterTransitionSystem(); ts.verifyNoNullLabels(); while (true) { @@ -65,7 +65,7 @@ public static void main(String[] args) { ModelCheckingResult result; Optional counterExample = Optional.empty(); if (formula instanceof LTLFormula ltlFormula) { - phiSymbol = Symbol.LOWERCASE_PHI_SYMBOL; + phiSymbol = Symbol.LOWERCASE_PHI; OUT.println(phiSymbol + " := " + formula + GRAY + " (LTL)" + RESET); LTLModelChecker modelChecker = new BasicLTLModelChecker(); @@ -76,14 +76,14 @@ public static void main(String[] args) { counterExample = Optional.of(ltlModelCheckingResult.getCounterExample()); } } else if (formula instanceof CTLFormula ctlFormula) { - phiSymbol = Symbol.UPPERCASE_PHI_SYMBOL; + phiSymbol = Symbol.UPPERCASE_PHI; OUT.println(phiSymbol + " := " + formula + GRAY + " (CTL)" + RESET); CTLModelChecker modelChecker = new BasicCTLModelChecker(); result = modelChecker.check(ts, ctlFormula); } else if (formula instanceof CTLStarFormula ctlStarFormula) { - phiSymbol = Symbol.UPPERCASE_PHI_SYMBOL; + phiSymbol = Symbol.UPPERCASE_PHI; OUT.println(phiSymbol + " := " + formula + GRAY + " (CTL*)" + RESET); @@ -95,9 +95,9 @@ public static void main(String[] args) { } if (result.isModel()) { - OUT.println(GREEN + "TS " + MODELS_SYMBOL + " " + phiSymbol + RESET); + OUT.println(GREEN + "TS " + MODELS + " " + phiSymbol + RESET); } else { - OUT.println(RED + "TS " + NOT_MODELS_SYMBOL + " " + phiSymbol); + OUT.println(RED + "TS " + NOT_MODELS + " " + phiSymbol); counterExample.ifPresent(infinitePath -> OUT.println("Counterexample: " + infinitePath)); OUT.print(RESET); } @@ -211,8 +211,8 @@ private static CTLStarFormula parseCTLStarFormula(String string) { return ctlStarParser.parse(string); } - private static TransitionSystem enterTransitionSystem() { - TransitionSystem ts = null; + private static BasicTransitionSystem enterTransitionSystem() { + BasicTransitionSystem ts = null; while (ts == null) { File file = null; String fileName = null; diff --git a/src/main/java/me/paultristanwagner/modelchecking/ModelChecker.java b/src/main/java/me/paultristanwagner/modelchecking/ModelChecker.java index 72a666a..cc99d31 100644 --- a/src/main/java/me/paultristanwagner/modelchecking/ModelChecker.java +++ b/src/main/java/me/paultristanwagner/modelchecking/ModelChecker.java @@ -1,11 +1,12 @@ package me.paultristanwagner.modelchecking; import java.util.Set; -import me.paultristanwagner.modelchecking.ts.TransitionSystem; +import me.paultristanwagner.modelchecking.automaton.State; +import me.paultristanwagner.modelchecking.ts.BasicTransitionSystem; public interface ModelChecker { - R check(TransitionSystem ts, T formula); + R check(BasicTransitionSystem ts, T formula); - Set sat(TransitionSystem ts, T formula); + Set sat(BasicTransitionSystem ts, T formula); } diff --git a/src/main/java/me/paultristanwagner/modelchecking/automaton/BasicState.java b/src/main/java/me/paultristanwagner/modelchecking/automaton/BasicState.java new file mode 100644 index 0000000..ef4e4b8 --- /dev/null +++ b/src/main/java/me/paultristanwagner/modelchecking/automaton/BasicState.java @@ -0,0 +1,48 @@ +package me.paultristanwagner.modelchecking.automaton; + +import com.google.gson.*; +import java.lang.reflect.Type; +import java.util.Objects; + +public class BasicState extends State { + + protected final String name; + + public BasicState(String name) { + this.name = name; + } + + @Override + public String toString() { + return name; + } + + @Override + public boolean equals(Object o) { + if (this == o) return true; + if (o == null || getClass() != o.getClass()) return false; + BasicState that = (BasicState) o; + return Objects.equals(name, that.name); + } + + @Override + public int hashCode() { + return Objects.hash(name); + } + + public static class BasicStateJsonAdapter + implements JsonSerializer, JsonDeserializer { + + @Override + public BasicState deserialize( + JsonElement json, Type typeOfT, JsonDeserializationContext context) + throws JsonParseException { + return new BasicState(json.getAsString()); + } + + @Override + public JsonElement serialize(BasicState src, Type typeOfSrc, JsonSerializationContext context) { + return new JsonPrimitive(src.name); + } + } +} diff --git a/src/main/java/me/paultristanwagner/modelchecking/automaton/CompositeState.java b/src/main/java/me/paultristanwagner/modelchecking/automaton/CompositeState.java new file mode 100644 index 0000000..15b64d1 --- /dev/null +++ b/src/main/java/me/paultristanwagner/modelchecking/automaton/CompositeState.java @@ -0,0 +1,40 @@ +package me.paultristanwagner.modelchecking.automaton; + +import java.util.Objects; + +public class CompositeState extends State { + + protected State left; + protected Object right; + + public CompositeState(State left, Object right) { + this.left = left; + this.right = right; + } + + public State getLeft() { + return left; + } + + public Object getRight() { + return right; + } + + @Override + public boolean equals(Object o) { + if (this == o) return true; + if (o == null || getClass() != o.getClass()) return false; + CompositeState that = (CompositeState) o; + return Objects.equals(left, that.left) && Objects.equals(right, that.right); + } + + @Override + public int hashCode() { + return Objects.hash(left, right); + } + + @Override + public String toString() { + return "<" + left + ", " + right + ">"; + } +} diff --git a/src/main/java/me/paultristanwagner/modelchecking/automaton/GNBA.java b/src/main/java/me/paultristanwagner/modelchecking/automaton/GNBA.java index 31c2900..76f5ac0 100644 --- a/src/main/java/me/paultristanwagner/modelchecking/automaton/GNBA.java +++ b/src/main/java/me/paultristanwagner/modelchecking/automaton/GNBA.java @@ -1,51 +1,37 @@ package me.paultristanwagner.modelchecking.automaton; import static me.paultristanwagner.modelchecking.util.GsonUtil.GSON; -import static me.paultristanwagner.modelchecking.util.TupleUtil.stringTuple; import java.lang.reflect.Type; -import java.util.HashSet; import java.util.Set; public class GNBA { - private final Set states; + private final Set states; private final Set alphabet; - private final Set initialStates; - private final Set> acceptingSets; - private final Set> transitions; + private final Set initialStates; + private final Set> acceptingSets; + private final TransitionFunction transitionFunction; public GNBA( - Set states, + Set states, Set alphabet, - Set initialStates, - Set> acceptingSets, - Set> transitions) { + Set initialStates, + Set> acceptingSets, + TransitionFunction transitionFunction) { this.states = states; this.alphabet = alphabet; this.initialStates = initialStates; this.acceptingSets = acceptingSets; - this.transitions = transitions; + this.transitionFunction = transitionFunction; } - public Set getSuccessors(String state) { - Set successors = new HashSet<>(); - for (NBATransition transition : transitions) { - if (transition.getFrom().equals(state)) { - successors.add(transition.getTo()); - } - } - return successors; + public Set getSuccessors(State state) { + return transitionFunction.getSuccessors(state); } - public Set getSuccessors(String state, String action) { - Set successors = new HashSet<>(); - for (NBATransition transition : transitions) { - if (transition.getFrom().equals(state) && transition.getAction().equals(action)) { - successors.add(transition.getTo()); - } - } - return successors; + public Set getSuccessors(State state, ActionType action) { + return transitionFunction.getSuccessors(state, action); } public NBA convertToNBA() { @@ -56,35 +42,35 @@ public NBA convertToNBA() { NBABuilder builder = new NBABuilder<>(); builder.setAlphabet(alphabet); - for (String state : states) { + for (State state : states) { for (int i = 0; i < acceptingSets.size(); i++) { - String nbaState = stringTuple(state, i + 1); + State nbaState = State.composite(state, i + 1); builder.addState(nbaState); } } - for (String initialState : initialStates) { - String nbaInitialState = stringTuple(initialState, 1); + for (State initialState : initialStates) { + State nbaInitialState = State.composite(initialState, 1); builder.addInitialState(nbaInitialState); } if (!acceptingSets.isEmpty()) { - Set acceptingSet = acceptingSets.stream().findFirst().get(); - for (String acceptingState : acceptingSet) { - String nbaAcceptingState = stringTuple(acceptingState, 1); + Set acceptingSet = acceptingSets.stream().findFirst().get(); + for (State acceptingState : acceptingSet) { + State nbaAcceptingState = State.composite(acceptingState, 1); builder.addAcceptingState(nbaAcceptingState); } } - for (NBATransition transition : transitions) { + for (NBATransition transition : transitionFunction.getTransitions()) { int i = 0; - for (Set acceptingSet : acceptingSets) { - String nbaFrom = stringTuple(transition.getFrom(), i + 1); - String nbaTo; + for (Set acceptingSet : acceptingSets) { + State nbaFrom = State.composite(transition.getFrom(), i + 1); + State nbaTo; if (acceptingSet.contains(transition.getFrom())) { - nbaTo = stringTuple(transition.getTo(), ((i + 1) % acceptingSets.size() + 1)); + nbaTo = State.composite(transition.getTo(), (i + 1) % acceptingSets.size() + 1); } else { - nbaTo = stringTuple(transition.getTo(), (i + 1)); + nbaTo = State.composite(transition.getTo(), i + 1); } builder.addTransition(nbaFrom, transition.getAction(), nbaTo); @@ -102,25 +88,25 @@ private NBA getCanonicalNBA() { NBABuilder builder = new NBABuilder<>(); builder.setAlphabet(alphabet); - for (String state : states) { + for (State state : states) { builder.addState(state); } - for (String initialState : initialStates) { + for (State initialState : initialStates) { builder.addInitialState(initialState); } if (acceptingSets.isEmpty()) { - for (String state : states) { + for (State state : states) { builder.addAcceptingState(state); } } else { - for (String acceptingState : acceptingSets.stream().findFirst().get()) { + for (State acceptingState : acceptingSets.stream().findFirst().get()) { builder.addAcceptingState(acceptingState); } } - for (NBATransition transition : transitions) { + for (NBATransition transition : transitionFunction.getTransitions()) { builder.addTransition(transition.getFrom(), transition.getAction(), transition.getTo()); } @@ -135,11 +121,11 @@ public static GNBA fromJson(String json, Type type) { return GSON.fromJson(json, type); } - public Set getStates() { + public Set getStates() { return states; } - public Set getInitialStates() { + public Set getInitialStates() { return initialStates; } @@ -147,11 +133,11 @@ public Set getAlphabet() { return alphabet; } - public Set> getAcceptingSets() { + public Set> getAcceptingSets() { return acceptingSets; } - public Set> getTransitions() { - return transitions; + public TransitionFunction getTransitionFunction() { + return transitionFunction; } } diff --git a/src/main/java/me/paultristanwagner/modelchecking/automaton/GNBABuilder.java b/src/main/java/me/paultristanwagner/modelchecking/automaton/GNBABuilder.java index 3417c9e..b7356c7 100644 --- a/src/main/java/me/paultristanwagner/modelchecking/automaton/GNBABuilder.java +++ b/src/main/java/me/paultristanwagner/modelchecking/automaton/GNBABuilder.java @@ -5,55 +5,67 @@ public class GNBABuilder { - private final Set states; + private final Set states; private final Set alphabet; - private final Set initialStates; - private final Set> acceptingSets; - private final Set> transitions; + private final Set initialStates; + private final Set> acceptingSets; + private final TransitionFunction transitionFunction; public GNBABuilder() { this.states = new HashSet<>(); this.alphabet = new HashSet<>(); this.initialStates = new HashSet<>(); this.acceptingSets = new HashSet<>(); - this.transitions = new HashSet<>(); + this.transitionFunction = new TransitionFunction<>(); } - public GNBABuilder addStates(String... states) { - for (String state : states) { + public GNBABuilder addStates(State... states) { + for (State state : states) { addState(state); } return this; } - public GNBABuilder addState(String state) { + public GNBABuilder addState(State state) { this.states.add(state); return this; } + public GNBABuilder addState(String name) { + return this.addState(State.named(name)); + } + public GNBABuilder setAlphabet(Set alphabet) { this.alphabet.clear(); this.alphabet.addAll(alphabet); return this; } - public GNBABuilder addInitialState(String initialState) { + public GNBABuilder addInitialState(State initialState) { this.initialStates.add(initialState); return this; } - public GNBABuilder addAcceptingSet(Set acceptingSet) { + public GNBABuilder addInitialState(String name) { + return this.addInitialState(State.named(name)); + } + + public GNBABuilder addAcceptingSet(Set acceptingSet) { this.acceptingSets.add(new HashSet<>(acceptingSet)); return this; } - public GNBABuilder addTransition(String from, ActionType action, String to) { - this.transitions.add(NBATransition.of(from, action, to)); + public GNBABuilder addTransition(State from, ActionType action, State to) { + this.transitionFunction.addTransition(from, action, to); return this; } + public GNBABuilder addTransition(String fromName, ActionType action, String toName) { + return this.addTransition(State.named(fromName), action, State.named(toName)); + } + public GNBA build() { - return new GNBA<>(states, alphabet, initialStates, acceptingSets, transitions); + return new GNBA<>(states, alphabet, initialStates, acceptingSets, transitionFunction); } } diff --git a/src/main/java/me/paultristanwagner/modelchecking/automaton/NBA.java b/src/main/java/me/paultristanwagner/modelchecking/automaton/NBA.java index 6deb664..f56a73e 100644 --- a/src/main/java/me/paultristanwagner/modelchecking/automaton/NBA.java +++ b/src/main/java/me/paultristanwagner/modelchecking/automaton/NBA.java @@ -1,106 +1,54 @@ package me.paultristanwagner.modelchecking.automaton; import static me.paultristanwagner.modelchecking.util.GsonUtil.GSON; -import static me.paultristanwagner.modelchecking.util.Pair.pair; -import static me.paultristanwagner.modelchecking.util.TupleUtil.stringTuple; import java.lang.reflect.Type; import java.util.*; - -import com.google.gson.annotations.SerializedName; import me.paultristanwagner.modelchecking.ts.CyclePath; -import me.paultristanwagner.modelchecking.util.Pair; public class NBA { - private final Set states; + private final Set states; private final Set alphabet; - private final Set initialStates; - private final Set acceptingStates; - private final Set> transitions; - - private final transient Map> successorCache; - private final transient Map, Set> successorActionCache; - - private NBA() { - this.states = new HashSet<>(); - this.alphabet = new HashSet<>(); - this.initialStates = new HashSet<>(); - this.acceptingStates = new HashSet<>(); - this.transitions = new HashSet<>(); - - this.successorCache = new HashMap<>(); - this.successorActionCache = new HashMap<>(); - } + private final Set initialStates; + private final Set acceptingStates; + private final TransitionFunction transitionFunction; public NBA( - Set states, + Set states, Set alphabet, - Set initialStates, - Set acceptingStates, - Set> transitions) { + Set initialStates, + Set acceptingStates, + TransitionFunction transitionFunction) { this.states = states; this.alphabet = alphabet; this.initialStates = initialStates; this.acceptingStates = acceptingStates; - this.transitions = transitions; - - this.successorCache = new HashMap<>(); - this.successorActionCache = new HashMap<>(); + this.transitionFunction = transitionFunction; } - public Set getSuccessors(String state) { - if(successorCache.containsKey(state)) { - return successorCache.get(state); - } - - Set successors = new HashSet<>(); - for (NBATransition transition : transitions) { - if (transition.getFrom().equals(state)) { - successors.add(transition.getTo()); - } - } - - successorCache.put(state, successors); - - return successors; + public Set getSuccessors(State state) { + return transitionFunction.getSuccessors(state); } - public Set getSuccessors(String state, ActionType action) { - if(successorActionCache.containsKey(pair(state, action))) { - return successorActionCache.get(pair(state, action)); - } - - Set successors = new HashSet<>(); - for (NBATransition transition : transitions) { - if (!transition.getFrom().equals(state)) { - continue; - } - - if (transition.getAction().equals(action)) { - successors.add(transition.getTo()); - } - } - - successorActionCache.put(pair(state, action), successors); - - return successors; + public Set getSuccessors(State state, ActionType action) { + return transitionFunction.getSuccessors(state, action); } - private boolean cycleCheck(String s, Set v, Stack xi) { + private boolean cycleCheck(State s, Set v, Stack xi) { xi.push(s); v.add(s); while (!xi.isEmpty()) { - String s1 = xi.peek(); - Set successors = getSuccessors(s1); + State s1 = xi.peek(); + Set successors = getSuccessors(s1); if (successors.contains(s)) { xi.push(s); return true; } else if (!v.containsAll(successors)) { - Set remainingSuccessors = new HashSet<>(successors); + Set remainingSuccessors = new HashSet<>(successors); remainingSuccessors.removeAll(v); - String s2 = remainingSuccessors.stream().findAny().get(); + State s2 = remainingSuccessors.stream().findAny().get(); v.add(s2); xi.push(s2); } else { @@ -113,36 +61,36 @@ private boolean cycleCheck(String s, Set v, Stack xi) { public NBAEmptinessResult checkEmptiness() { // run a nested-depth-first-search - Set u = new HashSet<>(); - Set v = new HashSet<>(); + Set u = new HashSet<>(); + Set v = new HashSet<>(); - Stack pi = new Stack<>(); - Stack xi = new Stack<>(); + Stack pi = new Stack<>(); + Stack xi = new Stack<>(); while (!u.containsAll(initialStates)) { - Set remaining = new HashSet<>(initialStates); + Set remaining = new HashSet<>(initialStates); remaining.removeAll(u); - String s0 = remaining.stream().findAny().get(); + State s0 = remaining.stream().findAny().get(); u.add(s0); pi.push(s0); while (!pi.isEmpty()) { - String s = pi.peek(); + State s = pi.peek(); - Set remainingSuccessors = new HashSet<>(getSuccessors(s)); + Set remainingSuccessors = new HashSet<>(getSuccessors(s)); remainingSuccessors.removeAll(u); if (!remainingSuccessors.isEmpty()) { - String s1 = remainingSuccessors.stream().findAny().get(); + State s1 = remainingSuccessors.stream().findAny().get(); u.add(s1); pi.push(s1); } else { pi.pop(); if (acceptingStates.contains(s) && cycleCheck(s, v, xi)) { - List piList = new ArrayList<>(pi); - List xiList = new ArrayList<>(xi); + List piList = new ArrayList<>(pi); + List xiList = new ArrayList<>(xi); CyclePath witness = new CyclePath(piList, xiList); return NBAEmptinessResult.nonEmpty(witness); @@ -155,59 +103,62 @@ public NBAEmptinessResult checkEmptiness() { } public GNBA toGNBA() { - Set states = new HashSet<>(this.states); + Set states = new HashSet<>(this.states); Set alphabet = new HashSet<>(this.alphabet); - Set initialStates = new HashSet<>(this.initialStates); - Set> transitions = new HashSet<>(this.transitions); + Set initialStates = new HashSet<>(this.initialStates); + TransitionFunction transitionFunction = + new TransitionFunction<>(this.transitionFunction); - Set> acceptingSets = new HashSet<>(); + Set> acceptingSets = new HashSet<>(); acceptingSets.add(new HashSet<>(this.acceptingStates)); - return new GNBA<>(states, alphabet, initialStates, acceptingSets, transitions); + return new GNBA<>(states, alphabet, initialStates, acceptingSets, transitionFunction); } public GNBA product(NBA other) { GNBABuilder builder = new GNBABuilder<>(); builder.setAlphabet(alphabet); - for (String state1 : states) { - for (String state2 : other.states) { - String state = stringTuple(state1, state2); + for (State state1 : states) { + for (State state2 : other.states) { + State state = State.composite(state1, state2); builder.addState(state); } } - for (String initialState : initialStates) { - for (String otherInitialState : other.initialStates) { - String state = stringTuple(initialState, otherInitialState); + for (State initialState : initialStates) { + for (State otherInitialState : other.initialStates) { + State state = State.composite(initialState, otherInitialState); builder.addInitialState(state); } } - for (NBATransition transition : transitions) { - for (NBATransition otherTransition : other.transitions) { - if (!transition.getAction().equals(otherTransition.getAction())) { - continue; + Set actions = new HashSet<>(); + actions.addAll(transitionFunction.getActions()); + actions.addAll(other.transitionFunction.getActions()); + for (ActionType action : actions) { + for (NBATransition transition : transitionFunction.getTransitions(action)) { + for (NBATransition otherTransition : + other.transitionFunction.getTransitions(action)) { + State from = State.composite(transition.getFrom(), otherTransition.getFrom()); + State to = State.composite(transition.getTo(), otherTransition.getTo()); + builder.addTransition(from, action, to); } - - String from = stringTuple(transition.getFrom(), otherTransition.getFrom()); - String to = stringTuple(transition.getTo(), otherTransition.getTo()); - builder.addTransition(from, transition.getAction(), to); } } - Set acceptingSet1 = new HashSet<>(); - for (String acceptingState : acceptingStates) { - for (String state : other.states) { - String newAcceptingState = stringTuple(acceptingState, state); + Set acceptingSet1 = new HashSet<>(); + for (State acceptingState : acceptingStates) { + for (State state : other.states) { + State newAcceptingState = State.composite(acceptingState, state); acceptingSet1.add(newAcceptingState); } } - Set acceptingSet2 = new HashSet<>(); - for (String acceptingState : other.acceptingStates) { - for (String state : states) { - String newAcceptingState = stringTuple(state, acceptingState); + Set acceptingSet2 = new HashSet<>(); + for (State acceptingState : other.acceptingStates) { + for (State state : states) { + State newAcceptingState = State.composite(state, acceptingState); acceptingSet2.add(newAcceptingState); } } @@ -226,7 +177,7 @@ public static NBA fromJson(String json, Type type) { return GSON.fromJson(json, type); } - public Set getStates() { + public Set getStates() { return states; } @@ -234,15 +185,15 @@ public Set getAlphabet() { return alphabet; } - public Set getInitialStates() { + public Set getInitialStates() { return initialStates; } - public Set getAcceptingStates() { + public Set getAcceptingStates() { return acceptingStates; } - public Set> getTransitions() { - return transitions; + public TransitionFunction getTransitionFunction() { + return transitionFunction; } } diff --git a/src/main/java/me/paultristanwagner/modelchecking/automaton/NBABuilder.java b/src/main/java/me/paultristanwagner/modelchecking/automaton/NBABuilder.java index eae38a5..0a692fa 100644 --- a/src/main/java/me/paultristanwagner/modelchecking/automaton/NBABuilder.java +++ b/src/main/java/me/paultristanwagner/modelchecking/automaton/NBABuilder.java @@ -5,55 +5,71 @@ public class NBABuilder { - private final Set states; + private final Set states; private final Set alphabet; - private final Set initialStates; - private final Set acceptingStates; - private final Set> transitions; + private final Set initialStates; + private final Set acceptingStates; + private final TransitionFunction transitionFunction; public NBABuilder() { this.states = new HashSet<>(); this.alphabet = new HashSet<>(); this.initialStates = new HashSet<>(); this.acceptingStates = new HashSet<>(); - this.transitions = new HashSet<>(); + this.transitionFunction = new TransitionFunction<>(); } - public NBABuilder addStates(String... states) { - for (String state : states) { + public NBABuilder addStates(State... states) { + for (State state : states) { addState(state); } return this; } - public NBABuilder addState(String state) { + public NBABuilder addState(State state) { this.states.add(state); return this; } + public NBABuilder addState(String name) { + return this.addState(State.named(name)); + } + public NBABuilder setAlphabet(Set alphabet) { this.alphabet.clear(); this.alphabet.addAll(alphabet); return this; } - public NBABuilder addInitialState(String initialState) { + public NBABuilder addInitialState(State initialState) { this.initialStates.add(initialState); return this; } - public NBABuilder addAcceptingState(String acceptingState) { + public NBABuilder addInitialState(String name) { + return this.addInitialState(State.named(name)); + } + + public NBABuilder addAcceptingState(State acceptingState) { this.acceptingStates.add(acceptingState); return this; } - public NBABuilder addTransition(String from, ActionType action, String to) { - this.transitions.add(NBATransition.of(from, action, to)); + public NBABuilder addAcceptingState(String name) { + return this.addAcceptingState(State.named(name)); + } + + public NBABuilder addTransition(State from, ActionType action, State to) { + this.transitionFunction.addTransition(from, action, to); return this; } + public NBABuilder addTransition(String fromName, ActionType action, String toName) { + return this.addTransition(State.named(fromName), action, State.named(toName)); + } + public NBA build() { - return new NBA(states, alphabet, initialStates, acceptingStates, transitions); + return new NBA<>(states, alphabet, initialStates, acceptingStates, transitionFunction); } } diff --git a/src/main/java/me/paultristanwagner/modelchecking/automaton/NBATransition.java b/src/main/java/me/paultristanwagner/modelchecking/automaton/NBATransition.java index a1ef4f2..3d0332d 100644 --- a/src/main/java/me/paultristanwagner/modelchecking/automaton/NBATransition.java +++ b/src/main/java/me/paultristanwagner/modelchecking/automaton/NBATransition.java @@ -7,22 +7,21 @@ public class NBATransition { - private final String from; + private final State from; private final ActionType action; - private final String to; + private final State to; - protected NBATransition(String from, ActionType action, String to) { + protected NBATransition(State from, ActionType action, State to) { this.from = from; this.action = action; this.to = to; } - public static NBATransition of( - String from, ActionType action, String to) { + public static NBATransition of(State from, ActionType action, State to) { return new NBATransition<>(from, action, to); } - public String getFrom() { + public State getFrom() { return from; } @@ -30,7 +29,7 @@ public ActionType getAction() { return action; } - public String getTo() { + public State getTo() { return to; } @@ -43,10 +42,10 @@ public JsonElement serialize( java.lang.reflect.Type typeOfSrc, JsonSerializationContext context) { JsonArray jsonArray = new JsonArray(); - jsonArray.add(transition.getFrom()); + jsonArray.add(context.serialize(transition.getFrom())); jsonArray.add( context.serialize(transition.getAction(), new TypeToken() {}.getType())); - jsonArray.add(transition.getTo()); + jsonArray.add(context.serialize(transition.getTo())); return jsonArray; } @@ -56,9 +55,9 @@ public NBATransition deserialize( JsonElement json, java.lang.reflect.Type typeOfT, JsonDeserializationContext context) throws JsonParseException { JsonArray tuple = json.getAsJsonArray(); - String from = tuple.get(0).getAsString(); + State from = context.deserialize(tuple.get(0), BasicState.class); String action = tuple.get(1).getAsString(); - String to = tuple.get(2).getAsString(); + State to = context.deserialize(tuple.get(2), BasicState.class); return NBATransition.of(from, action, to); } } @@ -69,14 +68,11 @@ public static class AdvancedNBATransitionAdapter @Override public JsonElement serialize( - NBATransition> transition, - java.lang.reflect.Type typeOfSrc, - JsonSerializationContext context) { + NBATransition> src, Type typeOfSrc, JsonSerializationContext context) { JsonArray jsonArray = new JsonArray(); - jsonArray.add(transition.getFrom()); - jsonArray.add( - context.serialize(transition.getAction(), new TypeToken>() {}.getType())); - jsonArray.add(transition.getTo()); + jsonArray.add(context.serialize(src.getFrom())); + jsonArray.add(context.serialize(src.getAction(), new TypeToken>() {}.getType())); + jsonArray.add(context.serialize(src.getTo())); return jsonArray; } @@ -86,10 +82,10 @@ public NBATransition> deserialize( JsonElement json, Type typeOfT, JsonDeserializationContext context) throws JsonParseException { JsonArray tuple = json.getAsJsonArray(); - String from = tuple.get(0).getAsString(); + State from = context.deserialize(tuple.get(0), BasicState.class); Set action = context.deserialize(tuple.get(1), new TypeToken>() {}.getType()); - String to = tuple.get(2).getAsString(); + State to = context.deserialize(tuple.get(2), BasicState.class); return NBATransition.of(from, action, to); } } diff --git a/src/main/java/me/paultristanwagner/modelchecking/automaton/SetState.java b/src/main/java/me/paultristanwagner/modelchecking/automaton/SetState.java new file mode 100644 index 0000000..9da6269 --- /dev/null +++ b/src/main/java/me/paultristanwagner/modelchecking/automaton/SetState.java @@ -0,0 +1,60 @@ +package me.paultristanwagner.modelchecking.automaton; + +import com.google.gson.*; +import com.google.gson.reflect.TypeToken; +import java.lang.reflect.Type; +import java.util.HashSet; +import java.util.Objects; +import java.util.Set; + +public class SetState extends State { + + protected Set set; + + public SetState(Set set) { + this.set = set; + } + + public Set getSet() { + return set; + } + + @Override + public boolean equals(Object o) { + if (this == o) return true; + if (o == null || getClass() != o.getClass()) return false; + SetState setState = (SetState) o; + return Objects.equals(set, setState.set); + } + + @Override + public int hashCode() { + return Objects.hash(set); + } + + public static class SetStateJsonAdapter + implements JsonSerializer>, JsonDeserializer> { + + @Override + public SetState deserialize( + JsonElement json, Type typeOfT, JsonDeserializationContext context) + throws JsonParseException { + JsonArray jsonArray = json.getAsJsonArray(); + Set set = new HashSet<>(); + for (JsonElement jsonElement : jsonArray) { + set.add(context.deserialize(jsonElement, new TypeToken() {}.getType())); + } + return new SetState<>(set); + } + + @Override + public JsonElement serialize( + SetState src, Type typeOfSrc, JsonSerializationContext context) { + JsonArray jsonArray = new JsonArray(); + for (T t : src.set) { + jsonArray.add(context.serialize(t, new TypeToken() {}.getType())); + } + return jsonArray; + } + } +} diff --git a/src/main/java/me/paultristanwagner/modelchecking/automaton/State.java b/src/main/java/me/paultristanwagner/modelchecking/automaton/State.java new file mode 100644 index 0000000..ca840cd --- /dev/null +++ b/src/main/java/me/paultristanwagner/modelchecking/automaton/State.java @@ -0,0 +1,16 @@ +package me.paultristanwagner.modelchecking.automaton; + +public abstract class State { + + public static BasicState named(String name) { + return new BasicState(name); + } + + public static CompositeState composite(State state, Object other) { + return new CompositeState(state, other); + } + + public static CompositeState composite(String name, Object other) { + return composite(named(name), other); + } +} diff --git a/src/main/java/me/paultristanwagner/modelchecking/automaton/TransitionFunction.java b/src/main/java/me/paultristanwagner/modelchecking/automaton/TransitionFunction.java new file mode 100644 index 0000000..06f6da1 --- /dev/null +++ b/src/main/java/me/paultristanwagner/modelchecking/automaton/TransitionFunction.java @@ -0,0 +1,145 @@ +package me.paultristanwagner.modelchecking.automaton; + +import static me.paultristanwagner.modelchecking.util.Pair.pair; + +import com.google.gson.*; +import com.google.gson.reflect.TypeToken; +import java.util.HashMap; +import java.util.HashSet; +import java.util.Map; +import java.util.Set; +import me.paultristanwagner.modelchecking.util.Pair; + +public class TransitionFunction { + + private final Set> transitions; + private final Set actions; + private final Map> stateSuccessors; + private final Map, Set> stateActionSuccessors; + private final Map>> actionTransitionMap; + + public TransitionFunction() { + this.transitions = new HashSet<>(); + this.actions = new HashSet<>(); + this.stateSuccessors = new HashMap<>(); + this.stateActionSuccessors = new HashMap<>(); + this.actionTransitionMap = new HashMap<>(); + } + + public TransitionFunction(TransitionFunction other) { + this.transitions = new HashSet<>(other.transitions); + this.actions = new HashSet<>(); + this.stateSuccessors = new HashMap<>(other.stateSuccessors); + this.stateActionSuccessors = new HashMap<>(other.stateActionSuccessors); + this.actionTransitionMap = new HashMap<>(other.actionTransitionMap); + } + + public void addTransition(State from, ActionType action, State to) { + NBATransition transition = new NBATransition<>(from, action, to); + transitions.add(transition); + actions.add(action); + + Set successors = stateSuccessors.getOrDefault(from, new HashSet<>()); + successors.add(to); + stateSuccessors.put(from, successors); + + Set actionSuccessors = + stateActionSuccessors.getOrDefault(pair(from, action), new HashSet<>()); + actionSuccessors.add(to); + stateActionSuccessors.put(pair(from, action), actionSuccessors); + + Set> actionTransitions = + actionTransitionMap.getOrDefault(action, new HashSet<>()); + actionTransitions.add(transition); + actionTransitionMap.put(action, actionTransitions); + } + + public Set getActions() { + return actions; + } + + public Set getSuccessors(State state, ActionType action) { + return stateActionSuccessors.getOrDefault(pair(state, action), new HashSet<>()); + } + + public Set getSuccessors(State state) { + return stateSuccessors.getOrDefault(state, new HashSet<>()); + } + + public Set> getTransitions(ActionType action) { + return actionTransitionMap.getOrDefault(action, new HashSet<>()); + } + + public Set> getTransitions() { + return transitions; + } + + public static class BasicTransitionFunctionAdapter + implements JsonSerializer>, + JsonDeserializer> { + + @Override + public JsonElement serialize( + TransitionFunction transitionFunction, + java.lang.reflect.Type typeOfSrc, + JsonSerializationContext context) { + JsonArray jsonArray = new JsonArray(); + for (NBATransition transition : transitionFunction.getTransitions()) { + jsonArray.add(context.serialize(transition)); + } + + return jsonArray; + } + + @Override + public TransitionFunction deserialize( + JsonElement json, java.lang.reflect.Type typeOfT, JsonDeserializationContext context) + throws JsonParseException { + TransitionFunction transitionFunction = new TransitionFunction<>(); + JsonArray jsonArray = json.getAsJsonArray(); + for (JsonElement jsonElement : jsonArray) { + NBATransition transition = + context.deserialize(jsonElement, new TypeToken>() {}.getType()); + transitionFunction.addTransition( + transition.getFrom(), transition.getAction(), transition.getTo()); + } + + return transitionFunction; + } + } + + public static class AdvancedTransitionFunctionAdapter + implements JsonSerializer>>, + JsonDeserializer>> { + + @Override + public JsonElement serialize( + TransitionFunction> transitionFunction, + java.lang.reflect.Type typeOfSrc, + JsonSerializationContext context) { + JsonArray jsonArray = new JsonArray(); + for (NBATransition> transition : transitionFunction.getTransitions()) { + jsonArray.add(context.serialize(transition)); + } + + return jsonArray; + } + + @Override + public TransitionFunction> deserialize( + JsonElement json, java.lang.reflect.Type typeOfT, JsonDeserializationContext context) + throws JsonParseException { + TransitionFunction> transitionFunction = new TransitionFunction<>(); + JsonArray jsonArray = json.getAsJsonArray(); + for (JsonElement jsonElement : jsonArray) { + NBATransition> transition = + context.deserialize( + jsonElement, new TypeToken>>() {}.getType()); + transitionFunction.addTransition( + transition.getFrom(), transition.getAction(), transition.getTo()); + } + + return transitionFunction; + } + } +} diff --git a/src/main/java/me/paultristanwagner/modelchecking/ctl/BasicCTLModelChecker.java b/src/main/java/me/paultristanwagner/modelchecking/ctl/BasicCTLModelChecker.java index 96c6edc..d57b2b5 100644 --- a/src/main/java/me/paultristanwagner/modelchecking/ctl/BasicCTLModelChecker.java +++ b/src/main/java/me/paultristanwagner/modelchecking/ctl/BasicCTLModelChecker.java @@ -7,21 +7,22 @@ import java.util.Iterator; import java.util.List; import java.util.Set; +import me.paultristanwagner.modelchecking.automaton.State; import me.paultristanwagner.modelchecking.ctl.formula.path.CTLAlwaysFormula; import me.paultristanwagner.modelchecking.ctl.formula.path.CTLNextFormula; import me.paultristanwagner.modelchecking.ctl.formula.path.CTLPathFormula; import me.paultristanwagner.modelchecking.ctl.formula.path.CTLUntilFormula; import me.paultristanwagner.modelchecking.ctl.formula.state.*; -import me.paultristanwagner.modelchecking.ts.TransitionSystem; +import me.paultristanwagner.modelchecking.ts.BasicTransitionSystem; public class BasicCTLModelChecker implements CTLModelChecker { @Override - public CTLModelCheckingResult check(TransitionSystem ts, CTLFormula formula) { + public CTLModelCheckingResult check(BasicTransitionSystem ts, CTLFormula formula) { CTLENFConverter converter = new CTLENFConverter(); CTLFormula enfFormula = converter.convert(formula); - Set satStates = sat(ts, enfFormula); + Set satStates = sat(ts, enfFormula); boolean models = satStates.containsAll(ts.getInitialStates()); @@ -33,7 +34,7 @@ public CTLModelCheckingResult check(TransitionSystem ts, CTLFormula formula) { } @Override - public Set sat(TransitionSystem ts, CTLFormula formula) { + public Set sat(BasicTransitionSystem ts, CTLFormula formula) { if (formula instanceof CTLIdentifierFormula identifierFormula) { return satIdentifier(ts, identifierFormula); } else if (formula instanceof CTLNotFormula notFormula) { @@ -55,7 +56,7 @@ public Set sat(TransitionSystem ts, CTLFormula formula) { throw new UnsupportedOperationException(); } - private Set satExists(TransitionSystem ts, CTLExistsFormula formula) { + private Set satExists(BasicTransitionSystem ts, CTLExistsFormula formula) { CTLPathFormula pathFormula = formula.getPathFormula(); if (pathFormula instanceof CTLNextFormula nextFormula) { return satExistsNext(ts, nextFormula); @@ -68,15 +69,15 @@ private Set satExists(TransitionSystem ts, CTLExistsFormula formula) { throw new UnsupportedOperationException(); } - private Set satExistsNext(TransitionSystem ts, CTLNextFormula nextFormula) { - Set result = new HashSet<>(); - Set satStates = sat(ts, nextFormula.getStateFormula()); + private Set satExistsNext(BasicTransitionSystem ts, CTLNextFormula nextFormula) { + Set result = new HashSet<>(); + Set satStates = sat(ts, nextFormula.getStateFormula()); - for (String state : ts.getStates()) { - List successors = ts.getSuccessors(state); + for (State state : ts.getStates()) { + Set successors = ts.getSuccessors(state); boolean hasSatSuccessor = false; - for (String successor : successors) { + for (State successor : successors) { if (satStates.contains(successor)) { hasSatSuccessor = true; break; @@ -91,26 +92,26 @@ private Set satExistsNext(TransitionSystem ts, CTLNextFormula nextFormul return result; } - private Set satExistsUntil(TransitionSystem ts, CTLUntilFormula untilFormula) { + private Set satExistsUntil(BasicTransitionSystem ts, CTLUntilFormula untilFormula) { CTLFormula left = untilFormula.getLeft(); CTLFormula right = untilFormula.getRight(); - Set satLeft = sat(ts, left); + Set satLeft = sat(ts, left); - Set T = sat(ts, right); + Set T = sat(ts, right); boolean changed = true; while (changed) { changed = false; - for (String state : satLeft) { + for (State state : satLeft) { if (T.contains(state)) { continue; } - List successors = ts.getSuccessors(state); + Set successors = ts.getSuccessors(state); boolean hasTSuccessor = false; - for (String successor : successors) { + for (State successor : successors) { if (T.contains(successor)) { hasTSuccessor = true; break; @@ -127,21 +128,21 @@ private Set satExistsUntil(TransitionSystem ts, CTLUntilFormula untilFor return T; } - private Set satExistsAlways(TransitionSystem ts, CTLAlwaysFormula formula) { + private Set satExistsAlways(BasicTransitionSystem ts, CTLAlwaysFormula formula) { CTLFormula stateFormula = formula.getStateFormula(); - Set V = sat(ts, stateFormula); + Set V = sat(ts, stateFormula); boolean changed = true; while (changed) { changed = false; - Iterator iterator = V.iterator(); + Iterator iterator = V.iterator(); while (iterator.hasNext()) { - String state = iterator.next(); - List successors = ts.getSuccessors(state); + State state = iterator.next(); + Set successors = ts.getSuccessors(state); boolean hasVSuccessor = false; - for (String successor : successors) { + for (State successor : successors) { if (V.contains(successor)) { hasVSuccessor = true; break; @@ -158,11 +159,11 @@ private Set satExistsAlways(TransitionSystem ts, CTLAlwaysFormula formul return V; } - private Set satIdentifier(TransitionSystem ts, CTLIdentifierFormula formula) { + private Set satIdentifier(BasicTransitionSystem ts, CTLIdentifierFormula formula) { String atomicProposition = formula.getIdentifier(); - Set satStates = new HashSet<>(); - for (String state : ts.getStates()) { + Set satStates = new HashSet<>(); + for (State state : ts.getStates()) { if (ts.getLabel(state).contains(atomicProposition)) { satStates.add(state); } @@ -171,18 +172,18 @@ private Set satIdentifier(TransitionSystem ts, CTLIdentifierFormula form return satStates; } - private Set satNot(TransitionSystem ts, CTLNotFormula formula) { - Set satStates = sat(ts, formula.getArgument()); - Set allStates = new HashSet<>(ts.getStates()); + private Set satNot(BasicTransitionSystem ts, CTLNotFormula formula) { + Set satStates = sat(ts, formula.getArgument()); + Set allStates = new HashSet<>(ts.getStates()); - Set result = new HashSet<>(allStates); + Set result = new HashSet<>(allStates); result.removeAll(satStates); return result; } - private Set satOr(TransitionSystem ts, CTLOrFormula formula) { - Set result = new HashSet<>(); + private Set satOr(BasicTransitionSystem ts, CTLOrFormula formula) { + Set result = new HashSet<>(); List components = formula.getComponents(); for (CTLFormula component : components) { result.addAll(sat(ts, component)); @@ -191,8 +192,8 @@ private Set satOr(TransitionSystem ts, CTLOrFormula formula) { return result; } - private Set satAnd(TransitionSystem ts, CTLAndFormula formula) { - Set result = new HashSet<>(ts.getStates()); + private Set satAnd(BasicTransitionSystem ts, CTLAndFormula formula) { + Set result = new HashSet<>(ts.getStates()); List components = formula.getComponents(); for (CTLFormula component : components) { result.retainAll(sat(ts, component)); @@ -201,11 +202,11 @@ private Set satAnd(TransitionSystem ts, CTLAndFormula formula) { return result; } - private Set satTrue(TransitionSystem ts, CTLTrueFormula formula) { + private Set satTrue(BasicTransitionSystem ts, CTLTrueFormula formula) { return new HashSet<>(ts.getStates()); } - private Set satFalse(TransitionSystem ts, CTLFalseFormula formula) { + private Set satFalse(BasicTransitionSystem ts, CTLFalseFormula formula) { return new HashSet<>(); } } diff --git a/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/path/CTLAlwaysFormula.java b/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/path/CTLAlwaysFormula.java index 1a86c97..48c93e4 100644 --- a/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/path/CTLAlwaysFormula.java +++ b/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/path/CTLAlwaysFormula.java @@ -1,6 +1,6 @@ package me.paultristanwagner.modelchecking.ctl.formula.path; -import static me.paultristanwagner.modelchecking.util.Symbol.ALWAYS_SYMBOL; +import static me.paultristanwagner.modelchecking.util.Symbol.ALWAYS; import me.paultristanwagner.modelchecking.ctl.formula.state.CTLFormula; import me.paultristanwagner.modelchecking.ctl.formula.state.CTLParenthesisFormula; @@ -24,9 +24,9 @@ public CTLFormula getStateFormula() { @Override public String toString() { if (stateFormula instanceof CTLParenthesisFormula) { - return ALWAYS_SYMBOL + stateFormula; + return ALWAYS + stateFormula; } else { - return ALWAYS_SYMBOL + "(" + stateFormula + ")"; + return ALWAYS + "(" + stateFormula + ")"; } } } diff --git a/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/path/CTLEventuallyFormula.java b/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/path/CTLEventuallyFormula.java index 2125d92..73c8959 100644 --- a/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/path/CTLEventuallyFormula.java +++ b/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/path/CTLEventuallyFormula.java @@ -1,6 +1,6 @@ package me.paultristanwagner.modelchecking.ctl.formula.path; -import static me.paultristanwagner.modelchecking.util.Symbol.EVENTUALLY_SYMBOL; +import static me.paultristanwagner.modelchecking.util.Symbol.EVENTUALLY; import me.paultristanwagner.modelchecking.ctl.formula.state.CTLFormula; import me.paultristanwagner.modelchecking.ctl.formula.state.CTLParenthesisFormula; @@ -24,9 +24,9 @@ public CTLFormula getStateFormula() { @Override public String toString() { if (stateFormula instanceof CTLParenthesisFormula) { - return EVENTUALLY_SYMBOL + stateFormula; + return EVENTUALLY + stateFormula; } else { - return EVENTUALLY_SYMBOL + "(" + stateFormula + ")"; + return EVENTUALLY + "(" + stateFormula + ")"; } } } diff --git a/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/path/CTLNextFormula.java b/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/path/CTLNextFormula.java index a6ec5c3..aadcbe7 100644 --- a/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/path/CTLNextFormula.java +++ b/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/path/CTLNextFormula.java @@ -1,6 +1,6 @@ package me.paultristanwagner.modelchecking.ctl.formula.path; -import static me.paultristanwagner.modelchecking.util.Symbol.NEXT_SYMBOL; +import static me.paultristanwagner.modelchecking.util.Symbol.NEXT; import me.paultristanwagner.modelchecking.ctl.formula.state.CTLFormula; import me.paultristanwagner.modelchecking.ctl.formula.state.CTLParenthesisFormula; @@ -24,9 +24,9 @@ public CTLFormula getStateFormula() { @Override public String toString() { if (stateFormula instanceof CTLParenthesisFormula) { - return NEXT_SYMBOL + stateFormula; + return NEXT + stateFormula; } else { - return NEXT_SYMBOL + "(" + stateFormula + ")"; + return NEXT + "(" + stateFormula + ")"; } } } diff --git a/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/path/CTLUntilFormula.java b/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/path/CTLUntilFormula.java index d26bdff..0c39cee 100644 --- a/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/path/CTLUntilFormula.java +++ b/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/path/CTLUntilFormula.java @@ -1,6 +1,6 @@ package me.paultristanwagner.modelchecking.ctl.formula.path; -import static me.paultristanwagner.modelchecking.util.Symbol.UNTIL_SYMBOL; +import static me.paultristanwagner.modelchecking.util.Symbol.UNTIL; import me.paultristanwagner.modelchecking.ctl.formula.state.CTLFormula; @@ -28,6 +28,6 @@ public CTLFormula getRight() { @Override public String toString() { - return "(" + left.toString() + " " + UNTIL_SYMBOL + " " + right.toString() + ")"; + return "(" + left.toString() + " " + UNTIL + " " + right.toString() + ")"; } } diff --git a/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/state/CTLAllFormula.java b/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/state/CTLAllFormula.java index 2ce12f2..8c65f9d 100644 --- a/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/state/CTLAllFormula.java +++ b/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/state/CTLAllFormula.java @@ -1,6 +1,6 @@ package me.paultristanwagner.modelchecking.ctl.formula.state; -import static me.paultristanwagner.modelchecking.util.Symbol.UNIVERSAL_QUANTIFIER_SYMBOL; +import static me.paultristanwagner.modelchecking.util.Symbol.UNIVERSAL_QUANTIFIER; import me.paultristanwagner.modelchecking.ctl.formula.path.CTLPathFormula; @@ -22,6 +22,6 @@ public CTLPathFormula getPathFormula() { @Override public String toString() { - return UNIVERSAL_QUANTIFIER_SYMBOL + pathFormula.toString(); + return UNIVERSAL_QUANTIFIER + pathFormula.toString(); } } diff --git a/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/state/CTLAndFormula.java b/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/state/CTLAndFormula.java index 616bcb2..5b942af 100644 --- a/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/state/CTLAndFormula.java +++ b/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/state/CTLAndFormula.java @@ -1,6 +1,6 @@ package me.paultristanwagner.modelchecking.ctl.formula.state; -import static me.paultristanwagner.modelchecking.util.Symbol.AND_SYMBOL; +import static me.paultristanwagner.modelchecking.util.Symbol.AND; import java.util.Arrays; import java.util.List; @@ -33,7 +33,7 @@ public String toString() { if (i < components.size() - 1) { builder.append(" "); - builder.append(AND_SYMBOL); + builder.append(AND); builder.append(" "); } } diff --git a/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/state/CTLExistsFormula.java b/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/state/CTLExistsFormula.java index 9c6335c..3f8c4f1 100644 --- a/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/state/CTLExistsFormula.java +++ b/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/state/CTLExistsFormula.java @@ -1,6 +1,6 @@ package me.paultristanwagner.modelchecking.ctl.formula.state; -import static me.paultristanwagner.modelchecking.util.Symbol.EXISTENTIAL_QUANTIFIER_SYMBOL; +import static me.paultristanwagner.modelchecking.util.Symbol.EXISTENTIAL_QUANTIFIER; import me.paultristanwagner.modelchecking.ctl.formula.path.CTLPathFormula; @@ -22,6 +22,6 @@ public CTLPathFormula getPathFormula() { @Override public String toString() { - return EXISTENTIAL_QUANTIFIER_SYMBOL + pathFormula.toString(); + return EXISTENTIAL_QUANTIFIER + pathFormula.toString(); } } diff --git a/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/state/CTLNotFormula.java b/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/state/CTLNotFormula.java index 533992f..8f224d4 100644 --- a/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/state/CTLNotFormula.java +++ b/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/state/CTLNotFormula.java @@ -1,6 +1,6 @@ package me.paultristanwagner.modelchecking.ctl.formula.state; -import static me.paultristanwagner.modelchecking.util.Symbol.NOT_SYMBOL; +import static me.paultristanwagner.modelchecking.util.Symbol.NOT; public class CTLNotFormula extends CTLFormula { @@ -20,6 +20,6 @@ public CTLFormula getArgument() { @Override public String toString() { - return NOT_SYMBOL + argument.toString(); + return NOT + argument.toString(); } } diff --git a/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/state/CTLOrFormula.java b/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/state/CTLOrFormula.java index e05e7c0..4e19f8d 100644 --- a/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/state/CTLOrFormula.java +++ b/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/state/CTLOrFormula.java @@ -1,6 +1,6 @@ package me.paultristanwagner.modelchecking.ctl.formula.state; -import static me.paultristanwagner.modelchecking.util.Symbol.OR_SYMBOL; +import static me.paultristanwagner.modelchecking.util.Symbol.OR; import java.util.Arrays; import java.util.List; @@ -33,7 +33,7 @@ public String toString() { if (i < components.size() - 1) { builder.append(" "); - builder.append(OR_SYMBOL); + builder.append(OR); builder.append(" "); } } diff --git a/src/main/java/me/paultristanwagner/modelchecking/ctl/parse/CTLLexer.java b/src/main/java/me/paultristanwagner/modelchecking/ctl/parse/CTLLexer.java index f1b8f29..b3acae3 100644 --- a/src/main/java/me/paultristanwagner/modelchecking/ctl/parse/CTLLexer.java +++ b/src/main/java/me/paultristanwagner/modelchecking/ctl/parse/CTLLexer.java @@ -4,6 +4,7 @@ import me.paultristanwagner.modelchecking.parse.Lexer; import me.paultristanwagner.modelchecking.parse.TokenType; +import me.paultristanwagner.modelchecking.util.Symbol; public class CTLLexer extends Lexer { @@ -11,20 +12,20 @@ public class CTLLexer extends Lexer { static final TokenType RPAREN = TokenType.of(")", "^\\)"); static final TokenType TRUE = TokenType.of("true", "^(true|TRUE)"); static final TokenType FALSE = TokenType.of("false", "^(false|FALSE)"); - static final TokenType NOT = TokenType.of("not", "^(" + NOT_SYMBOL + "|!|not|NOT|~)"); - static final TokenType AND = TokenType.of("and", "^(" + AND_SYMBOL + "|&|and|AND)"); - static final TokenType OR = TokenType.of("or", "^(" + OR_SYMBOL + "|\\||or|OR)"); - static final TokenType NEXT = TokenType.of("next", "^(" + NEXT_SYMBOL + "|next|NEXT|O)"); - static final TokenType UNTIL = TokenType.of("until", "^(" + UNTIL_SYMBOL + "|until|UNTIL)"); + static final TokenType NOT = TokenType.of("not", "^(" + Symbol.NOT + "|!|not|NOT|~)"); + static final TokenType AND = TokenType.of("and", "^(" + Symbol.AND + "|&|and|AND)"); + static final TokenType OR = TokenType.of("or", "^(" + Symbol.OR + "|\\||or|OR)"); + static final TokenType NEXT = TokenType.of("next", "^(" + Symbol.NEXT + "|next|NEXT|O)"); + static final TokenType UNTIL = TokenType.of("until", "^(" + Symbol.UNTIL + "|until|UNTIL)"); static final TokenType EVENTUALLY = TokenType.of( - "eventually", "^(" + EVENTUALLY_SYMBOL + "|eventually|EVENTUALLY|diamond|DIAMOND)"); + "eventually", "^(" + Symbol.EVENTUALLY + "|eventually|EVENTUALLY|diamond|DIAMOND)"); static final TokenType ALWAYS = - TokenType.of("always", "^(" + ALWAYS_SYMBOL + "|always|ALWAYS|box|BOX)"); + TokenType.of("always", "^(" + Symbol.ALWAYS + "|always|ALWAYS|box|BOX)"); static final TokenType ALL = - TokenType.of("all", "^(" + UNIVERSAL_QUANTIFIER_SYMBOL + "|all|ALL|A)"); + TokenType.of("all", "^(" + UNIVERSAL_QUANTIFIER + "|all|ALL|A)"); static final TokenType EXISTS = - TokenType.of("exists", "^(" + EXISTENTIAL_QUANTIFIER_SYMBOL + "|exists|EXISTS|ex|EX|E)"); + TokenType.of("exists", "^(" + EXISTENTIAL_QUANTIFIER + "|exists|EXISTS|ex|EX|E)"); static final TokenType IDENTIFIER = TokenType.of("identifier", "^[a-z]"); public CTLLexer(String input) { diff --git a/src/main/java/me/paultristanwagner/modelchecking/ctlstar/BasicCTLStarModelChecker.java b/src/main/java/me/paultristanwagner/modelchecking/ctlstar/BasicCTLStarModelChecker.java index e2c2b93..22dbafd 100644 --- a/src/main/java/me/paultristanwagner/modelchecking/ctlstar/BasicCTLStarModelChecker.java +++ b/src/main/java/me/paultristanwagner/modelchecking/ctlstar/BasicCTLStarModelChecker.java @@ -3,17 +3,18 @@ import static me.paultristanwagner.modelchecking.ltl.formula.LTLNotFormula.not; import java.util.*; +import me.paultristanwagner.modelchecking.automaton.State; import me.paultristanwagner.modelchecking.ctlstar.formula.*; import me.paultristanwagner.modelchecking.ltl.BasicLTLModelChecker; import me.paultristanwagner.modelchecking.ltl.LTLModelChecker; import me.paultristanwagner.modelchecking.ltl.formula.LTLFormula; -import me.paultristanwagner.modelchecking.ts.TransitionSystem; +import me.paultristanwagner.modelchecking.ts.BasicTransitionSystem; public class BasicCTLStarModelChecker implements CTLStarModelChecker { @Override - public CTLStarModelCheckingResult check(TransitionSystem ts, CTLStarFormula formula) { - ts = ts.copy(); + public CTLStarModelCheckingResult check(BasicTransitionSystem ts, CTLStarFormula formula) { + ts = (BasicTransitionSystem) ts.copy(); while (true) { Set stateSubFormulas = getNonTrivialMinimalStateSubFormulas(formula); @@ -27,7 +28,7 @@ public CTLStarModelCheckingResult check(TransitionSystem ts, CTLStarFormula form for (CTLStarFormula subFormula : stateSubFormulasList) { if (subFormula != formula && subFormula instanceof CTLStarIdentifierFormula) continue; - Set satStates = sat(ts, subFormula); + Set satStates = sat(ts, subFormula); if (subFormula == formula) { if (satStates.containsAll(ts.getInitialStates())) { @@ -38,7 +39,7 @@ public CTLStarModelCheckingResult check(TransitionSystem ts, CTLStarFormula form } String freshAtomicProposition = ts.introduceFreshAtomicProposition(); - for (String satState : satStates) { + for (State satState : satStates) { ts.addLabel(satState, freshAtomicProposition); } formula.replaceFormula(subFormula, freshAtomicProposition); @@ -47,7 +48,7 @@ public CTLStarModelCheckingResult check(TransitionSystem ts, CTLStarFormula form } @Override - public Set sat(TransitionSystem ts, CTLStarFormula formula) { + public Set sat(BasicTransitionSystem ts, CTLStarFormula formula) { if (formula instanceof CTLStarTrueFormula) { return satTrue(ts); } else if (formula instanceof CTLStarFalseFormula) { @@ -71,35 +72,35 @@ public Set sat(TransitionSystem ts, CTLStarFormula formula) { throw new UnsupportedOperationException(); } - private Set satExists(TransitionSystem ts, CTLStarExistsFormula existsFormula) { + private Set satExists(BasicTransitionSystem ts, CTLStarExistsFormula existsFormula) { LTLModelChecker ltlModelChecker = new BasicLTLModelChecker(); LTLFormula ltlFormula = existsFormula.getFormula().toLTL(); LTLFormula negated = not(ltlFormula); - Set negation = ltlModelChecker.sat(ts, negated); - Set sat = new HashSet<>(ts.getStates()); + Set negation = ltlModelChecker.sat(ts, negated); + Set sat = new HashSet<>(ts.getStates()); sat.removeAll(negation); return sat; } - private Set satAll(TransitionSystem ts, CTLStarAllFormula allFormula) { + private Set satAll(BasicTransitionSystem ts, CTLStarAllFormula allFormula) { LTLModelChecker ltlModelChecker = new BasicLTLModelChecker(); LTLFormula ltlFormula = allFormula.getFormula().toLTL(); return ltlModelChecker.sat(ts, ltlFormula); } - private Set satTrue(TransitionSystem ts) { + private Set satTrue(BasicTransitionSystem ts) { return new HashSet<>(ts.getStates()); } - private Set satFalse(TransitionSystem ts) { + private Set satFalse(BasicTransitionSystem ts) { return new HashSet<>(); } - private Set satIdentifier(TransitionSystem ts, CTLStarIdentifierFormula formula) { + private Set satIdentifier(BasicTransitionSystem ts, CTLStarIdentifierFormula formula) { String atomicProposition = formula.getIdentifier(); - Set satStates = new HashSet<>(); - for (String state : ts.getStates()) { + Set satStates = new HashSet<>(); + for (State state : ts.getStates()) { if (ts.getLabel(state).contains(atomicProposition)) { satStates.add(state); } @@ -108,24 +109,24 @@ private Set satIdentifier(TransitionSystem ts, CTLStarIdentifierFormula return satStates; } - private Set satAnd(TransitionSystem ts, CTLStarAndFormula andFormula) { - Set satStates = new HashSet<>(ts.getStates()); + private Set satAnd(BasicTransitionSystem ts, CTLStarAndFormula andFormula) { + Set satStates = new HashSet<>(ts.getStates()); for (CTLStarFormula component : andFormula.getComponents()) { satStates.retainAll(sat(ts, component)); } return satStates; } - private Set satOr(TransitionSystem ts, CTLStarOrFormula orFormula) { - Set satStates = new HashSet<>(); + private Set satOr(BasicTransitionSystem ts, CTLStarOrFormula orFormula) { + Set satStates = new HashSet<>(); for (CTLStarFormula component : orFormula.getComponents()) { satStates.addAll(sat(ts, component)); } return satStates; } - private Set satNot(TransitionSystem ts, CTLStarNotFormula notFormula) { - Set satStates = new HashSet<>(ts.getStates()); + private Set satNot(BasicTransitionSystem ts, CTLStarNotFormula notFormula) { + Set satStates = new HashSet<>(ts.getStates()); satStates.removeAll(sat(ts, notFormula.getFormula())); return satStates; } diff --git a/src/main/java/me/paultristanwagner/modelchecking/ctlstar/formula/CTLStarAllFormula.java b/src/main/java/me/paultristanwagner/modelchecking/ctlstar/formula/CTLStarAllFormula.java index 0af9fdd..1634641 100644 --- a/src/main/java/me/paultristanwagner/modelchecking/ctlstar/formula/CTLStarAllFormula.java +++ b/src/main/java/me/paultristanwagner/modelchecking/ctlstar/formula/CTLStarAllFormula.java @@ -50,7 +50,7 @@ public CTLStarFormula getFormula() { @Override public String toString() { - return Symbol.UNIVERSAL_QUANTIFIER_SYMBOL + formula; + return Symbol.UNIVERSAL_QUANTIFIER + formula; } @Override diff --git a/src/main/java/me/paultristanwagner/modelchecking/ctlstar/formula/CTLStarAlwaysFormula.java b/src/main/java/me/paultristanwagner/modelchecking/ctlstar/formula/CTLStarAlwaysFormula.java index 7834eed..4c2fecc 100644 --- a/src/main/java/me/paultristanwagner/modelchecking/ctlstar/formula/CTLStarAlwaysFormula.java +++ b/src/main/java/me/paultristanwagner/modelchecking/ctlstar/formula/CTLStarAlwaysFormula.java @@ -50,7 +50,7 @@ public CTLStarFormula getFormula() { @Override public String toString() { - return Symbol.ALWAYS_SYMBOL + formula; + return Symbol.ALWAYS + formula; } @Override diff --git a/src/main/java/me/paultristanwagner/modelchecking/ctlstar/formula/CTLStarAndFormula.java b/src/main/java/me/paultristanwagner/modelchecking/ctlstar/formula/CTLStarAndFormula.java index 4183354..ad23687 100644 --- a/src/main/java/me/paultristanwagner/modelchecking/ctlstar/formula/CTLStarAndFormula.java +++ b/src/main/java/me/paultristanwagner/modelchecking/ctlstar/formula/CTLStarAndFormula.java @@ -1,6 +1,6 @@ package me.paultristanwagner.modelchecking.ctlstar.formula; -import static me.paultristanwagner.modelchecking.util.Symbol.AND_SYMBOL; +import static me.paultristanwagner.modelchecking.util.Symbol.AND; import java.util.*; import me.paultristanwagner.modelchecking.ltl.formula.LTLAndFormula; @@ -75,7 +75,7 @@ public String toString() { if (i < components.size() - 1) { builder.append(" "); - builder.append(AND_SYMBOL); + builder.append(AND); builder.append(" "); } } diff --git a/src/main/java/me/paultristanwagner/modelchecking/ctlstar/formula/CTLStarEventuallyFormula.java b/src/main/java/me/paultristanwagner/modelchecking/ctlstar/formula/CTLStarEventuallyFormula.java index 30c910a..18b68d3 100644 --- a/src/main/java/me/paultristanwagner/modelchecking/ctlstar/formula/CTLStarEventuallyFormula.java +++ b/src/main/java/me/paultristanwagner/modelchecking/ctlstar/formula/CTLStarEventuallyFormula.java @@ -48,7 +48,7 @@ public LTLFormula toLTL() { @Override public String toString() { - return Symbol.EVENTUALLY_SYMBOL + formula; + return Symbol.EVENTUALLY + formula; } public CTLStarFormula getFormula() { diff --git a/src/main/java/me/paultristanwagner/modelchecking/ctlstar/formula/CTLStarExistsFormula.java b/src/main/java/me/paultristanwagner/modelchecking/ctlstar/formula/CTLStarExistsFormula.java index 9153eb0..3b401e5 100644 --- a/src/main/java/me/paultristanwagner/modelchecking/ctlstar/formula/CTLStarExistsFormula.java +++ b/src/main/java/me/paultristanwagner/modelchecking/ctlstar/formula/CTLStarExistsFormula.java @@ -1,6 +1,6 @@ package me.paultristanwagner.modelchecking.ctlstar.formula; -import static me.paultristanwagner.modelchecking.util.Symbol.EXISTENTIAL_QUANTIFIER_SYMBOL; +import static me.paultristanwagner.modelchecking.util.Symbol.EXISTENTIAL_QUANTIFIER; import java.util.Objects; import java.util.Set; @@ -51,7 +51,7 @@ public LTLFormula toLTL() { @Override public String toString() { - return EXISTENTIAL_QUANTIFIER_SYMBOL + formula; + return EXISTENTIAL_QUANTIFIER + formula; } @Override diff --git a/src/main/java/me/paultristanwagner/modelchecking/ctlstar/formula/CTLStarNextFormula.java b/src/main/java/me/paultristanwagner/modelchecking/ctlstar/formula/CTLStarNextFormula.java index f34b776..e2f65d4 100644 --- a/src/main/java/me/paultristanwagner/modelchecking/ctlstar/formula/CTLStarNextFormula.java +++ b/src/main/java/me/paultristanwagner/modelchecking/ctlstar/formula/CTLStarNextFormula.java @@ -1,6 +1,6 @@ package me.paultristanwagner.modelchecking.ctlstar.formula; -import static me.paultristanwagner.modelchecking.util.Symbol.NEXT_SYMBOL; +import static me.paultristanwagner.modelchecking.util.Symbol.NEXT; import java.util.Objects; import java.util.Set; @@ -51,7 +51,7 @@ public CTLStarFormula getFormula() { @Override public String toString() { - return NEXT_SYMBOL + formula; + return NEXT + formula; } @Override diff --git a/src/main/java/me/paultristanwagner/modelchecking/ctlstar/formula/CTLStarNotFormula.java b/src/main/java/me/paultristanwagner/modelchecking/ctlstar/formula/CTLStarNotFormula.java index c12fe36..2db33e7 100644 --- a/src/main/java/me/paultristanwagner/modelchecking/ctlstar/formula/CTLStarNotFormula.java +++ b/src/main/java/me/paultristanwagner/modelchecking/ctlstar/formula/CTLStarNotFormula.java @@ -1,6 +1,6 @@ package me.paultristanwagner.modelchecking.ctlstar.formula; -import static me.paultristanwagner.modelchecking.util.Symbol.NOT_SYMBOL; +import static me.paultristanwagner.modelchecking.util.Symbol.NOT; import java.util.Objects; import java.util.Set; @@ -51,7 +51,7 @@ public CTLStarFormula getFormula() { @Override public String toString() { - return NOT_SYMBOL + formula; + return NOT + formula; } @Override diff --git a/src/main/java/me/paultristanwagner/modelchecking/ctlstar/formula/CTLStarOrFormula.java b/src/main/java/me/paultristanwagner/modelchecking/ctlstar/formula/CTLStarOrFormula.java index 46b6187..e6dadd3 100644 --- a/src/main/java/me/paultristanwagner/modelchecking/ctlstar/formula/CTLStarOrFormula.java +++ b/src/main/java/me/paultristanwagner/modelchecking/ctlstar/formula/CTLStarOrFormula.java @@ -1,6 +1,6 @@ package me.paultristanwagner.modelchecking.ctlstar.formula; -import static me.paultristanwagner.modelchecking.util.Symbol.OR_SYMBOL; +import static me.paultristanwagner.modelchecking.util.Symbol.OR; import java.util.*; import me.paultristanwagner.modelchecking.ltl.formula.LTLFormula; @@ -75,7 +75,7 @@ public String toString() { if (i < components.size() - 1) { builder.append(" "); - builder.append(OR_SYMBOL); + builder.append(OR); builder.append(" "); } } diff --git a/src/main/java/me/paultristanwagner/modelchecking/ctlstar/parse/CTLStarLexer.java b/src/main/java/me/paultristanwagner/modelchecking/ctlstar/parse/CTLStarLexer.java index 41a32db..b37a5ff 100644 --- a/src/main/java/me/paultristanwagner/modelchecking/ctlstar/parse/CTLStarLexer.java +++ b/src/main/java/me/paultristanwagner/modelchecking/ctlstar/parse/CTLStarLexer.java @@ -4,6 +4,7 @@ import me.paultristanwagner.modelchecking.parse.Lexer; import me.paultristanwagner.modelchecking.parse.TokenType; +import me.paultristanwagner.modelchecking.util.Symbol; public class CTLStarLexer extends Lexer { @@ -11,20 +12,20 @@ public class CTLStarLexer extends Lexer { static final TokenType RPAREN = TokenType.of(")", "^\\)"); static final TokenType TRUE = TokenType.of("true", "^(true|TRUE)"); static final TokenType FALSE = TokenType.of("false", "^(false|FALSE)"); - static final TokenType NOT = TokenType.of("not", "^(" + NOT_SYMBOL + "|!|not|NOT|~)"); - static final TokenType AND = TokenType.of("and", "^(" + AND_SYMBOL + "|&|and|AND)"); - static final TokenType OR = TokenType.of("or", "^(" + OR_SYMBOL + "|\\||or|OR)"); - static final TokenType NEXT = TokenType.of("next", "^(" + NEXT_SYMBOL + "|next|NEXT|O)"); - static final TokenType UNTIL = TokenType.of("until", "^(" + UNTIL_SYMBOL + "|until|UNTIL)"); + static final TokenType NOT = TokenType.of("not", "^(" + Symbol.NOT + "|!|not|NOT|~)"); + static final TokenType AND = TokenType.of("and", "^(" + Symbol.AND + "|&|and|AND)"); + static final TokenType OR = TokenType.of("or", "^(" + Symbol.OR + "|\\||or|OR)"); + static final TokenType NEXT = TokenType.of("next", "^(" + Symbol.NEXT + "|next|NEXT|O)"); + static final TokenType UNTIL = TokenType.of("until", "^(" + Symbol.UNTIL + "|until|UNTIL)"); static final TokenType EVENTUALLY = TokenType.of( - "eventually", "^(" + EVENTUALLY_SYMBOL + "|eventually|EVENTUALLY|diamond|DIAMOND)"); + "eventually", "^(" + Symbol.EVENTUALLY + "|eventually|EVENTUALLY|diamond|DIAMOND)"); static final TokenType ALWAYS = - TokenType.of("always", "^(" + ALWAYS_SYMBOL + "|always|ALWAYS|box|BOX)"); + TokenType.of("always", "^(" + Symbol.ALWAYS + "|always|ALWAYS|box|BOX)"); static final TokenType ALL = - TokenType.of("all", "^(" + UNIVERSAL_QUANTIFIER_SYMBOL + "|all|ALL|A)"); + TokenType.of("all", "^(" + UNIVERSAL_QUANTIFIER + "|all|ALL|A)"); static final TokenType EXISTS = - TokenType.of("exists", "^(" + EXISTENTIAL_QUANTIFIER_SYMBOL + "|exists|EXISTS|ex|EX|E)"); + TokenType.of("exists", "^(" + EXISTENTIAL_QUANTIFIER + "|exists|EXISTS|ex|EX|E)"); static final TokenType IDENTIFIER = TokenType.of("identifier", "^[a-z]"); public CTLStarLexer(String input) { diff --git a/src/main/java/me/paultristanwagner/modelchecking/ltl/BasicLTLModelChecker.java b/src/main/java/me/paultristanwagner/modelchecking/ltl/BasicLTLModelChecker.java index 03b8e69..a5eaf99 100644 --- a/src/main/java/me/paultristanwagner/modelchecking/ltl/BasicLTLModelChecker.java +++ b/src/main/java/me/paultristanwagner/modelchecking/ltl/BasicLTLModelChecker.java @@ -5,10 +5,9 @@ import static me.paultristanwagner.modelchecking.ltl.formula.LTLIdentifierFormula.identifier; import java.util.*; -import me.paultristanwagner.modelchecking.automaton.GNBA; -import me.paultristanwagner.modelchecking.automaton.GNBABuilder; -import me.paultristanwagner.modelchecking.automaton.NBA; +import me.paultristanwagner.modelchecking.automaton.*; import me.paultristanwagner.modelchecking.ltl.formula.*; +import me.paultristanwagner.modelchecking.ts.BasicTransitionSystem; import me.paultristanwagner.modelchecking.ts.CyclePath; import me.paultristanwagner.modelchecking.ts.TSPersistenceResult; import me.paultristanwagner.modelchecking.ts.TransitionSystem; @@ -16,7 +15,7 @@ public class BasicLTLModelChecker implements LTLModelChecker { @Override - public LTLModelCheckingResult check(TransitionSystem ts, LTLFormula formula) { + public LTLModelCheckingResult check(BasicTransitionSystem ts, LTLFormula formula) { ts = ts.copy(); // Ensure that the transition system contains only the mentioned atomic propositions @@ -38,9 +37,9 @@ public LTLModelCheckingResult check(TransitionSystem ts, LTLFormula formula) { GNBA> gnba = computeGNBA(ts, negation); NBA> nba = gnba.convertToNBA(); - TransitionSystem synchronousProduct = ts.reachableSynchronousProduct(nba); + TransitionSystem synchronousProduct = ts.reachableSynchronousProduct(nba); - Set persistentStates = new HashSet<>(nba.getStates()); + Set persistentStates = new HashSet<>(nba.getStates()); nba.getAcceptingStates().forEach(persistentStates::remove); TSPersistenceResult result = synchronousProduct.checkPersistence(persistentStates); @@ -53,21 +52,21 @@ public LTLModelCheckingResult check(TransitionSystem ts, LTLFormula formula) { } @Override - public Set sat(TransitionSystem ts, LTLFormula formula) { - Set result = new HashSet<>(); + public Set sat(BasicTransitionSystem ts, LTLFormula formula) { + Set result = new HashSet<>(); LTLFormula negation = formula.negate(); - GNBA gnba = computeGNBA(ts, negation); - NBA nba = gnba.convertToNBA(); + GNBA> gnba = computeGNBA(ts, negation); + NBA> nba = gnba.convertToNBA(); - for (String state : ts.getStates()) { - TransitionSystem initial = ts.copy(); + for (State state : ts.getStates()) { + TransitionSystem initial = ts.copy(); initial.clearInitialStates(); initial.addInitialState(state); - TransitionSystem synchronousProduct = initial.reachableSynchronousProduct(nba); + TransitionSystem synchronousProduct = initial.reachableSynchronousProduct(nba); - Set persistentStates = new HashSet<>(nba.getStates()); + Set persistentStates = new HashSet<>(nba.getStates()); nba.getAcceptingStates().forEach(persistentStates::remove); TSPersistenceResult persistenceResult = synchronousProduct.checkPersistence(persistentStates); @@ -79,7 +78,7 @@ public Set sat(TransitionSystem ts, LTLFormula formula) { return result; } - private GNBA> computeGNBA(TransitionSystem ts, LTLFormula formula) { + private GNBA> computeGNBA(BasicTransitionSystem ts, LTLFormula formula) { Set atomicPropositions = new HashSet<>(ts.getAtomicPropositions()); Set closure = formula.getClosure(); Set elementarySets = computeElementarySets(atomicPropositions, closure); @@ -94,7 +93,8 @@ private GNBA> computeGNBA(TransitionSystem ts, LTLFormula formula) { * (2) eventually phi in B <=> phi in B or eventually phi in B' */ for (B one : elementarySets) { - gnbaBuilder.addState(one.toString()); + State state = new SetState<>(one.assumedSubformulas); + gnbaBuilder.addState(state); Set assumedAtomicPropositions = one.assumedAtomicPropositions(); @@ -145,8 +145,9 @@ private GNBA> computeGNBA(TransitionSystem ts, LTLFormula formula) { continue; } - gnbaBuilder.addTransition( - one.toString(), assumedAtomicPropositions, potentialSuccessor.toString()); + State from = new SetState<>(one.assumedSubformulas); + State to = new SetState<>(potentialSuccessor.assumedSubformulas); + gnbaBuilder.addTransition(from, assumedAtomicPropositions, to); } } @@ -158,29 +159,31 @@ private GNBA> computeGNBA(TransitionSystem ts, LTLFormula formula) { */ for (LTLFormula ltlFormula : closure) { if (ltlFormula instanceof LTLUntilFormula untilFormula) { - Set acceptingSet = new HashSet<>(); + Set acceptingSet = new HashSet<>(); - for (B state : elementarySets) { - if (!state.isAssumed(untilFormula) || state.isAssumed(untilFormula.getRight())) { - acceptingSet.add(state.toString()); + for (B b : elementarySets) { + if (!b.isAssumed(untilFormula) || b.isAssumed(untilFormula.getRight())) { + State state = new SetState<>(b.assumedSubformulas); + acceptingSet.add(state); } } gnbaBuilder.addAcceptingSet(acceptingSet); } else if (ltlFormula instanceof LTLEventuallyFormula eventuallyFormula) { - Set acceptingSet = new HashSet<>(); - for (B state : elementarySets) { - if (!state.isAssumed(eventuallyFormula) - || state.isAssumed(eventuallyFormula.getFormula())) { - acceptingSet.add(state.toString()); + Set acceptingSet = new HashSet<>(); + for (B b : elementarySets) { + if (!b.isAssumed(eventuallyFormula) || b.isAssumed(eventuallyFormula.getFormula())) { + State state = new SetState<>(b.assumedSubformulas); + acceptingSet.add(state); } } gnbaBuilder.addAcceptingSet(acceptingSet); } else if (ltlFormula instanceof LTLAlwaysFormula alwaysFormula) { - Set acceptingSet = new HashSet<>(); - for (B state : elementarySets) { - if (state.isAssumed(alwaysFormula) || !state.isAssumed(alwaysFormula.getFormula())) { - acceptingSet.add(state.toString()); + Set acceptingSet = new HashSet<>(); + for (B b : elementarySets) { + if (b.isAssumed(alwaysFormula) || !b.isAssumed(alwaysFormula.getFormula())) { + State state = new SetState<>(b.assumedSubformulas); + acceptingSet.add(state); } } gnbaBuilder.addAcceptingSet(acceptingSet); @@ -189,7 +192,8 @@ private GNBA> computeGNBA(TransitionSystem ts, LTLFormula formula) { for (B elementarySet : elementarySets) { if (elementarySet.isAssumed(formula)) { - gnbaBuilder.addInitialState(elementarySet.toString()); + State state = new SetState<>(elementarySet.assumedSubformulas); + gnbaBuilder.addInitialState(state); } } diff --git a/src/main/java/me/paultristanwagner/modelchecking/ltl/LTLModelChecker.java b/src/main/java/me/paultristanwagner/modelchecking/ltl/LTLModelChecker.java index b04bf72..2bdc0fb 100644 --- a/src/main/java/me/paultristanwagner/modelchecking/ltl/LTLModelChecker.java +++ b/src/main/java/me/paultristanwagner/modelchecking/ltl/LTLModelChecker.java @@ -1,11 +1,6 @@ package me.paultristanwagner.modelchecking.ltl; -import java.util.Set; import me.paultristanwagner.modelchecking.ModelChecker; import me.paultristanwagner.modelchecking.ltl.formula.LTLFormula; -import me.paultristanwagner.modelchecking.ts.TransitionSystem; -public interface LTLModelChecker extends ModelChecker { - - Set sat(TransitionSystem ts, LTLFormula formula); -} +public interface LTLModelChecker extends ModelChecker {} diff --git a/src/main/java/me/paultristanwagner/modelchecking/ltl/formula/LTLAlwaysFormula.java b/src/main/java/me/paultristanwagner/modelchecking/ltl/formula/LTLAlwaysFormula.java index 1a6ebb6..5d614cc 100644 --- a/src/main/java/me/paultristanwagner/modelchecking/ltl/formula/LTLAlwaysFormula.java +++ b/src/main/java/me/paultristanwagner/modelchecking/ltl/formula/LTLAlwaysFormula.java @@ -1,6 +1,6 @@ package me.paultristanwagner.modelchecking.ltl.formula; -import static me.paultristanwagner.modelchecking.util.Symbol.ALWAYS_SYMBOL; +import static me.paultristanwagner.modelchecking.util.Symbol.ALWAYS; import java.util.ArrayList; import java.util.List; @@ -32,7 +32,7 @@ public List getAllSubformulas() { @Override public String toString() { - return ALWAYS_SYMBOL + formula; + return ALWAYS + formula; } @Override diff --git a/src/main/java/me/paultristanwagner/modelchecking/ltl/formula/LTLAndFormula.java b/src/main/java/me/paultristanwagner/modelchecking/ltl/formula/LTLAndFormula.java index 422cb60..de3f2bf 100644 --- a/src/main/java/me/paultristanwagner/modelchecking/ltl/formula/LTLAndFormula.java +++ b/src/main/java/me/paultristanwagner/modelchecking/ltl/formula/LTLAndFormula.java @@ -1,6 +1,6 @@ package me.paultristanwagner.modelchecking.ltl.formula; -import static me.paultristanwagner.modelchecking.util.Symbol.AND_SYMBOL; +import static me.paultristanwagner.modelchecking.util.Symbol.AND; import java.util.ArrayList; import java.util.Arrays; @@ -45,7 +45,7 @@ public String toString() { if (i < components.size() - 1) { builder.append(" "); - builder.append(AND_SYMBOL); + builder.append(AND); builder.append(" "); } } diff --git a/src/main/java/me/paultristanwagner/modelchecking/ltl/formula/LTLEventuallyFormula.java b/src/main/java/me/paultristanwagner/modelchecking/ltl/formula/LTLEventuallyFormula.java index d9e6719..6264cdb 100644 --- a/src/main/java/me/paultristanwagner/modelchecking/ltl/formula/LTLEventuallyFormula.java +++ b/src/main/java/me/paultristanwagner/modelchecking/ltl/formula/LTLEventuallyFormula.java @@ -1,6 +1,6 @@ package me.paultristanwagner.modelchecking.ltl.formula; -import static me.paultristanwagner.modelchecking.util.Symbol.EVENTUALLY_SYMBOL; +import static me.paultristanwagner.modelchecking.util.Symbol.EVENTUALLY; import java.util.ArrayList; import java.util.List; @@ -38,7 +38,7 @@ public boolean equals(Object obj) { @Override public String toString() { - return EVENTUALLY_SYMBOL + formula; + return EVENTUALLY + formula; } @Override diff --git a/src/main/java/me/paultristanwagner/modelchecking/ltl/formula/LTLImplicationFormula.java b/src/main/java/me/paultristanwagner/modelchecking/ltl/formula/LTLImplicationFormula.java index fedf5f7..d49b23a 100644 --- a/src/main/java/me/paultristanwagner/modelchecking/ltl/formula/LTLImplicationFormula.java +++ b/src/main/java/me/paultristanwagner/modelchecking/ltl/formula/LTLImplicationFormula.java @@ -1,6 +1,6 @@ package me.paultristanwagner.modelchecking.ltl.formula; -import static me.paultristanwagner.modelchecking.util.Symbol.IMPLICATION_SYMBOL; +import static me.paultristanwagner.modelchecking.util.Symbol.IMPLICATION; import java.util.ArrayList; import java.util.List; @@ -39,7 +39,7 @@ public LTLFormula getRight() { @Override public String toString() { - return "(" + left + " " + IMPLICATION_SYMBOL + " " + right + ")"; + return "(" + left + " " + IMPLICATION + " " + right + ")"; } @Override diff --git a/src/main/java/me/paultristanwagner/modelchecking/ltl/formula/LTLNextFormula.java b/src/main/java/me/paultristanwagner/modelchecking/ltl/formula/LTLNextFormula.java index 672e900..3837037 100644 --- a/src/main/java/me/paultristanwagner/modelchecking/ltl/formula/LTLNextFormula.java +++ b/src/main/java/me/paultristanwagner/modelchecking/ltl/formula/LTLNextFormula.java @@ -1,6 +1,6 @@ package me.paultristanwagner.modelchecking.ltl.formula; -import static me.paultristanwagner.modelchecking.util.Symbol.NEXT_SYMBOL; +import static me.paultristanwagner.modelchecking.util.Symbol.NEXT; import java.util.ArrayList; import java.util.List; @@ -37,7 +37,7 @@ public boolean equals(Object obj) { @Override public String toString() { - return NEXT_SYMBOL + formula; + return NEXT + formula; } @Override diff --git a/src/main/java/me/paultristanwagner/modelchecking/ltl/formula/LTLNotFormula.java b/src/main/java/me/paultristanwagner/modelchecking/ltl/formula/LTLNotFormula.java index bc957a3..7076aee 100644 --- a/src/main/java/me/paultristanwagner/modelchecking/ltl/formula/LTLNotFormula.java +++ b/src/main/java/me/paultristanwagner/modelchecking/ltl/formula/LTLNotFormula.java @@ -1,6 +1,6 @@ package me.paultristanwagner.modelchecking.ltl.formula; -import static me.paultristanwagner.modelchecking.util.Symbol.NOT_SYMBOL; +import static me.paultristanwagner.modelchecking.util.Symbol.NOT; import java.util.ArrayList; import java.util.List; @@ -33,9 +33,9 @@ public LTLFormula getFormula() { @Override public String toString() { if (formula instanceof LTLAndFormula || formula instanceof LTLOrFormula) { - return NOT_SYMBOL + "(" + formula + ")"; + return NOT + "(" + formula + ")"; } - return NOT_SYMBOL + formula; + return NOT + formula; } @Override diff --git a/src/main/java/me/paultristanwagner/modelchecking/ltl/formula/LTLOrFormula.java b/src/main/java/me/paultristanwagner/modelchecking/ltl/formula/LTLOrFormula.java index 0278ce1..1d356d9 100644 --- a/src/main/java/me/paultristanwagner/modelchecking/ltl/formula/LTLOrFormula.java +++ b/src/main/java/me/paultristanwagner/modelchecking/ltl/formula/LTLOrFormula.java @@ -1,6 +1,6 @@ package me.paultristanwagner.modelchecking.ltl.formula; -import static me.paultristanwagner.modelchecking.util.Symbol.OR_SYMBOL; +import static me.paultristanwagner.modelchecking.util.Symbol.OR; import java.util.ArrayList; import java.util.List; @@ -44,7 +44,7 @@ public String toString() { if (i < components.size() - 1) { builder.append(" "); - builder.append(OR_SYMBOL); + builder.append(OR); builder.append(" "); } } diff --git a/src/main/java/me/paultristanwagner/modelchecking/ltl/formula/LTLUntilFormula.java b/src/main/java/me/paultristanwagner/modelchecking/ltl/formula/LTLUntilFormula.java index 41b0eed..b199ab7 100644 --- a/src/main/java/me/paultristanwagner/modelchecking/ltl/formula/LTLUntilFormula.java +++ b/src/main/java/me/paultristanwagner/modelchecking/ltl/formula/LTLUntilFormula.java @@ -1,6 +1,6 @@ package me.paultristanwagner.modelchecking.ltl.formula; -import static me.paultristanwagner.modelchecking.util.Symbol.UNTIL_SYMBOL; +import static me.paultristanwagner.modelchecking.util.Symbol.UNTIL; import java.util.ArrayList; import java.util.List; @@ -39,7 +39,7 @@ public LTLFormula getRight() { @Override public String toString() { - return "(" + left + " " + UNTIL_SYMBOL + " " + right + ")"; + return "(" + left + " " + UNTIL + " " + right + ")"; } @Override diff --git a/src/main/java/me/paultristanwagner/modelchecking/ltl/parse/LTLLexer.java b/src/main/java/me/paultristanwagner/modelchecking/ltl/parse/LTLLexer.java index a056fa5..aa4a1de 100644 --- a/src/main/java/me/paultristanwagner/modelchecking/ltl/parse/LTLLexer.java +++ b/src/main/java/me/paultristanwagner/modelchecking/ltl/parse/LTLLexer.java @@ -1,9 +1,8 @@ package me.paultristanwagner.modelchecking.ltl.parse; -import static me.paultristanwagner.modelchecking.util.Symbol.*; - import me.paultristanwagner.modelchecking.parse.Lexer; import me.paultristanwagner.modelchecking.parse.TokenType; +import me.paultristanwagner.modelchecking.util.Symbol; public class LTLLexer extends Lexer { @@ -11,18 +10,18 @@ public class LTLLexer extends Lexer { static final TokenType RPAREN = TokenType.of(")", "^\\)"); static final TokenType TRUE = TokenType.of("true", "^(true|TRUE)"); static final TokenType FALSE = TokenType.of("false", "^(false|FALSE)"); - static final TokenType NOT = TokenType.of("not", "^(" + NOT_SYMBOL + "|!|not|NOT|~)"); - static final TokenType AND = TokenType.of("and", "^(" + AND_SYMBOL + "|&|and|AND)"); - static final TokenType OR = TokenType.of("or", "^(" + OR_SYMBOL + "|\\||or|OR)"); + static final TokenType NOT = TokenType.of("not", "^(" + Symbol.NOT + "|!|not|NOT|~)"); + static final TokenType AND = TokenType.of("and", "^(" + Symbol.AND + "|&|and|AND)"); + static final TokenType OR = TokenType.of("or", "^(" + Symbol.OR + "|\\||or|OR)"); static final TokenType IMPLICATION = - TokenType.of("implication", "^(" + IMPLICATION_SYMBOL + "|->|implies|IMPLIES)"); - static final TokenType NEXT = TokenType.of("next", "^(" + NEXT_SYMBOL + "|next|NEXT|O)"); - static final TokenType UNTIL = TokenType.of("until", "^(" + UNTIL_SYMBOL + "|until|UNTIL)"); + TokenType.of("implication", "^(" + Symbol.IMPLICATION + "|->|implies|IMPLIES)"); + static final TokenType NEXT = TokenType.of("next", "^(" + Symbol.NEXT + "|next|NEXT|O)"); + static final TokenType UNTIL = TokenType.of("until", "^(" + Symbol.UNTIL + "|until|UNTIL)"); static final TokenType EVENTUALLY = TokenType.of( - "eventually", "^(" + EVENTUALLY_SYMBOL + "|eventually|EVENTUALLY|diamond|DIAMOND)"); + "eventually", "^(" + Symbol.EVENTUALLY + "|eventually|EVENTUALLY|diamond|DIAMOND)"); static final TokenType ALWAYS = - TokenType.of("always", "^(" + ALWAYS_SYMBOL + "|always|ALWAYS|box|BOX)"); + TokenType.of("always", "^(" + Symbol.ALWAYS + "|always|ALWAYS|box|BOX)"); static final TokenType IDENTIFIER = TokenType.of("identifier", "^[a-zA-Z_][a-zA-Z0-9_]*"); public LTLLexer(String input) { diff --git a/src/main/java/me/paultristanwagner/modelchecking/ts/BasicTransitionSystem.java b/src/main/java/me/paultristanwagner/modelchecking/ts/BasicTransitionSystem.java new file mode 100644 index 0000000..62deea3 --- /dev/null +++ b/src/main/java/me/paultristanwagner/modelchecking/ts/BasicTransitionSystem.java @@ -0,0 +1,46 @@ +package me.paultristanwagner.modelchecking.ts; + +import java.util.HashMap; +import java.util.HashSet; +import java.util.Map; +import java.util.Set; +import me.paultristanwagner.modelchecking.automaton.State; + +public class BasicTransitionSystem extends TransitionSystem { + + public BasicTransitionSystem( + Set states, + Map> successors, + Set initialStates, + Set atomicPropositions, + Map> labelingFunction) { + super(states, successors, initialStates, atomicPropositions, labelingFunction); + } + + public String introduceFreshAtomicProposition() { + int i = 0; + while (true) { + String atomicProposition = "a_" + i; + if (!atomicPropositions.contains(atomicProposition)) { + atomicPropositions.add(atomicProposition); + return atomicProposition; + } + i++; + } + } + + @Override + public BasicTransitionSystem copy() { + Set states = new HashSet<>(this.states); + Map> transitions = new HashMap<>(this.successors); + Set initialStates = new HashSet<>(this.initialStates); + Set atomicPropositions = new HashSet<>(this.atomicPropositions); + + Map> labelingFunction = new HashMap<>(); + this.labelingFunction.forEach( + (state, labels) -> labelingFunction.put(state, new HashSet<>(labels))); + + return new BasicTransitionSystem( + states, transitions, initialStates, atomicPropositions, labelingFunction); + } +} diff --git a/src/main/java/me/paultristanwagner/modelchecking/ts/CyclePath.java b/src/main/java/me/paultristanwagner/modelchecking/ts/CyclePath.java index 383513a..d90fa74 100644 --- a/src/main/java/me/paultristanwagner/modelchecking/ts/CyclePath.java +++ b/src/main/java/me/paultristanwagner/modelchecking/ts/CyclePath.java @@ -4,23 +4,21 @@ import java.util.ArrayList; import java.util.List; +import me.paultristanwagner.modelchecking.automaton.CompositeState; +import me.paultristanwagner.modelchecking.automaton.State; -public record CyclePath(List start, List cycle) { - - private static final String TUPLE_PREFIX = "("; - private static final String TUPLE_SUFFIX = ")"; - private static final String TUPLE_SEPARATOR = ","; +public record CyclePath(List start, List cycle) { @Override public String toString() { StringBuilder sb = new StringBuilder(); - for (String s : start) { + for (State s : start) { sb.append(s).append(" "); } sb.append("("); for (int i = 0; i < cycle.size() - 1; i++) { - String s = cycle.get(i); + State s = cycle.get(i); sb.append(s); if (i < cycle.size() - 2) { @@ -34,39 +32,29 @@ public String toString() { } public CyclePath reduce() { - for (String s : start) { - if (!s.startsWith(TUPLE_PREFIX) || !s.endsWith(TUPLE_SUFFIX)) { - return this; - } + for (State s : start) { + if (!(s instanceof CompositeState)) return this; } - for (String s : cycle) { - if (!s.startsWith(TUPLE_PREFIX) || !s.endsWith(TUPLE_SUFFIX)) { - return this; - } + for (State s : cycle) { + if (!(s instanceof CompositeState)) return this; } - List transformedStart = transformList(start); - List transformedCycle = transformList(cycle); + List transformedStart = reduceList(start); + List transformedCycle = reduceList(cycle); return new CyclePath(transformedStart, transformedCycle); } - private List transformList(List list) { - List transformed = new ArrayList<>(); - for (String s : list) { - transformed.add(transformTuple(s)); + private List reduceList(List list) { + List transformed = new ArrayList<>(); + for (State s : list) { + if (!(s instanceof CompositeState compositeState)) { + throw new IllegalStateException("Can only reduce composite states"); + } + transformed.add(compositeState.getLeft()); } return transformed; } - - private String transformTuple(String tupleString) { - String removedPrefix = tupleString.substring(TUPLE_PREFIX.length()); - String removedSuffix = - removedPrefix.substring(0, removedPrefix.length() - TUPLE_SUFFIX.length()); - String[] split = removedSuffix.split(TUPLE_SEPARATOR); - - return split[0]; - } } diff --git a/src/main/java/me/paultristanwagner/modelchecking/ts/TSTransition.java b/src/main/java/me/paultristanwagner/modelchecking/ts/TSTransition.java deleted file mode 100644 index faad00c..0000000 --- a/src/main/java/me/paultristanwagner/modelchecking/ts/TSTransition.java +++ /dev/null @@ -1,52 +0,0 @@ -package me.paultristanwagner.modelchecking.ts; - -import com.google.gson.*; - -public class TSTransition { - - private final String from; - private final String to; - - private TSTransition(String from, String to) { - this.from = from; - this.to = to; - } - - public static TSTransition of(String from, String to) { - return new TSTransition(from, to); - } - - public String getFrom() { - return from; - } - - public String getTo() { - return to; - } - - public static class TSTransitionAdapter - implements JsonSerializer, JsonDeserializer { - - @Override - public JsonElement serialize( - TSTransition transition, - java.lang.reflect.Type typeOfSrc, - JsonSerializationContext context) { - JsonArray jsonArray = new JsonArray(); - jsonArray.add(transition.getFrom()); - jsonArray.add(transition.getTo()); - - return jsonArray; - } - - @Override - public TSTransition deserialize( - JsonElement json, java.lang.reflect.Type typeOfT, JsonDeserializationContext context) - throws JsonParseException { - JsonArray tuple = json.getAsJsonArray(); - String from = tuple.get(0).getAsString(); - String to = tuple.get(1).getAsString(); - return TSTransition.of(from, to); - } - } -} diff --git a/src/main/java/me/paultristanwagner/modelchecking/ts/TransitionSystem.java b/src/main/java/me/paultristanwagner/modelchecking/ts/TransitionSystem.java index a662084..f63e418 100644 --- a/src/main/java/me/paultristanwagner/modelchecking/ts/TransitionSystem.java +++ b/src/main/java/me/paultristanwagner/modelchecking/ts/TransitionSystem.java @@ -3,34 +3,43 @@ import static me.paultristanwagner.modelchecking.ts.TSPersistenceResult.notPersistent; import static me.paultristanwagner.modelchecking.ts.TSPersistenceResult.persistent; import static me.paultristanwagner.modelchecking.util.GsonUtil.GSON; -import static me.paultristanwagner.modelchecking.util.TupleUtil.stringTuple; import java.util.*; -import java.util.AbstractMap.SimpleEntry; +import java.util.List; +import me.paultristanwagner.modelchecking.automaton.CompositeState; import me.paultristanwagner.modelchecking.automaton.NBA; import me.paultristanwagner.modelchecking.automaton.NBATransition; - -public class TransitionSystem { - - private final Set states; - private final Set transitions; - private final Set initialStates; - private final Set atomicPropositions; - private final Map> labelingFunction; +import me.paultristanwagner.modelchecking.automaton.State; + +public class TransitionSystem { + + protected final Set states; + protected final Map> successors; + protected final Set initialStates; + protected final Set atomicPropositions; + protected final Map> labelingFunction; + + protected TransitionSystem() { + this.states = new HashSet<>(); + this.successors = new HashMap<>(); + this.initialStates = new HashSet<>(); + this.atomicPropositions = new HashSet<>(); + this.labelingFunction = new HashMap<>(); + } public TransitionSystem( - Set states, - Set transitions, - Set initialStates, - Set atomicPropositions, - Map> labelingFunction) { + Set states, + Map> successors, + Set initialStates, + Set atomicPropositions, + Map> labelingFunction) { this.states = states; - this.transitions = transitions; + this.successors = successors; this.initialStates = initialStates; this.atomicPropositions = atomicPropositions; this.labelingFunction = labelingFunction; - for (String state : states) { + for (State state : states) { labelingFunction.putIfAbsent(state, Set.of()); } } @@ -44,74 +53,74 @@ public void verifyNoNullLabels() { }); } - public TransitionSystem copy() { - Set states = new HashSet<>(this.states); - Set transitions = new HashSet<>(this.transitions); - Set initialStates = new HashSet<>(this.initialStates); - Set atomicPropositions = new HashSet<>(this.atomicPropositions); + public TransitionSystem copy() { + Set states = new HashSet<>(this.states); + Map> successors = new HashMap<>(this.successors); + 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 HashSet<>(labels))); - return new TransitionSystem( - states, transitions, initialStates, atomicPropositions, labelingFunction); + return new TransitionSystem<>( + states, successors, initialStates, atomicPropositions, labelingFunction); } - public TransitionSystem reachableSynchronousProduct(NBA> nba) { - TransitionSystemBuilder builder = new TransitionSystemBuilder(); + public TransitionSystem reachableSynchronousProduct(NBA> nba) { + TransitionSystemBuilder builder = new TransitionSystemBuilder<>(); - for (String state : nba.getStates()) { + for (State state : nba.getStates()) { builder.addAtomicProposition(state); } - Queue> queue = new ArrayDeque<>(); - for (String initialState : initialStates) { - Set label = labelingFunction.get(initialState); + Queue queue = new ArrayDeque<>(); + for (State initialState : initialStates) { + Set label = labelingFunction.get(initialState); - for (NBATransition> nbaTransition : nba.getTransitions()) { - String q0 = nbaTransition.getFrom(); + for (NBATransition> nbaTransition : + nba.getTransitionFunction().getTransitions()) { + State q0 = nbaTransition.getFrom(); if (!nba.getInitialStates().contains(q0)) { continue; } - String q = nbaTransition.getTo(); + State q = nbaTransition.getTo(); if (!nbaTransition.getAction().equals(label)) { continue; } - String resultState = stringTuple(initialState, q); + CompositeState resultState = State.composite(initialState, q); builder.addState(resultState); builder.addLabel(resultState, q); builder.addInitialState(resultState); - queue.add(new SimpleEntry<>(initialState, q)); + queue.add(resultState); } } - Set> visited = new HashSet<>(); + Set visited = new HashSet<>(); while (!queue.isEmpty()) { - SimpleEntry state = queue.poll(); + CompositeState state = queue.poll(); visited.add(state); - String s = state.getKey(); + State s = state.getLeft(); - String q = state.getValue(); - List sSuccessors = getSuccessors(s); + State q = (State) state.getRight(); + Set sSuccessors = getSuccessors(s); - for (String sSuccessor : sSuccessors) { - Set sSuccessorLabel = labelingFunction.get(sSuccessor); - Set qSuccessors = nba.getSuccessors(q, sSuccessorLabel); - for (String qSuccessor : qSuccessors) { + for (State sSuccessor : sSuccessors) { + Set sSuccessorLabel = labelingFunction.get(sSuccessor); + Set qSuccessors = nba.getSuccessors(q, sSuccessorLabel); + for (State qSuccessor : qSuccessors) { - String from = stringTuple(s, q); - String to = stringTuple(sSuccessor, qSuccessor); + CompositeState from = State.composite(s, q); + CompositeState to = State.composite(sSuccessor, qSuccessor); builder.addTransition(from, to); - SimpleEntry successor = new SimpleEntry<>(sSuccessor, qSuccessor); - if (!visited.contains(successor)) { - queue.add(successor); + if (!visited.contains(to)) { + queue.add(to); builder.addState(to); builder.addLabel(to, qSuccessor); } @@ -122,20 +131,20 @@ public TransitionSystem reachableSynchronousProduct(NBA> nba) { return builder.build(); } - private boolean cycleCheck(String s, Set v, Stack xi) { + private boolean cycleCheck(State s, Set v, Stack xi) { xi.push(s); v.add(s); while (!xi.isEmpty()) { - String s1 = xi.peek(); - List successors = getSuccessors(s1); + State s1 = xi.peek(); + Set successors = getSuccessors(s1); if (successors.contains(s)) { xi.push(s); return true; } else if (!v.containsAll(successors)) { - Set remainingSuccessors = new HashSet<>(successors); + Set remainingSuccessors = new HashSet<>(successors); remainingSuccessors.removeAll(v); - String s2 = remainingSuccessors.stream().findAny().get(); + State s2 = remainingSuccessors.stream().findAny().get(); v.add(s2); xi.push(s2); } else { @@ -149,42 +158,42 @@ private boolean cycleCheck(String s, Set v, Stack xi) { /** * @return whether the ts satisfies the persistence property 'eventually always P' */ - public TSPersistenceResult checkPersistence(Set persistentStates) { + public TSPersistenceResult checkPersistence(Set persistentStates) { // run a nested-depth-first-search - Set u = new HashSet<>(); - Set v = new HashSet<>(); + Set u = new HashSet<>(); + Set v = new HashSet<>(); - Stack pi = new Stack<>(); - Stack xi = new Stack<>(); + Stack pi = new Stack<>(); + Stack xi = new Stack<>(); while (!u.containsAll(initialStates)) { - Set remaining = new HashSet<>(initialStates); + Set remaining = new HashSet<>(initialStates); remaining.removeAll(u); - String s0 = remaining.stream().findAny().get(); + State s0 = remaining.stream().findAny().get(); u.add(s0); pi.push(s0); while (!pi.isEmpty()) { - String s = pi.peek(); + State s = pi.peek(); - Set remainingSuccessors = new HashSet<>(getSuccessors(s)); + Set remainingSuccessors = new HashSet<>(getSuccessors(s)); remainingSuccessors.removeAll(u); if (!remainingSuccessors.isEmpty()) { - String s1 = remainingSuccessors.stream().findAny().get(); + State s1 = remainingSuccessors.stream().findAny().get(); u.add(s1); pi.push(s1); } else { pi.pop(); - Set labels = labelingFunction.get(s); + Set labels = labelingFunction.get(s); boolean notPersistentState = labels.stream().noneMatch(persistentStates::contains); if (notPersistentState && cycleCheck(s, v, xi)) { - List piList = new ArrayList<>(pi); - List xiList = new ArrayList<>(xi); + List piList = new ArrayList<>(pi); + List xiList = new ArrayList<>(xi); CyclePath witness = new CyclePath(piList, xiList); return notPersistent(witness); @@ -196,32 +205,20 @@ public TSPersistenceResult checkPersistence(Set persistentStates) { return persistent(); } - public void addAtomicProposition(String atomicProposition) { + public void addAtomicProposition(APType atomicProposition) { atomicPropositions.add(atomicProposition); } - public void removeAtomicProposition(String atomicProposition) { + public void removeAtomicProposition(APType atomicProposition) { atomicPropositions.remove(atomicProposition); labelingFunction.forEach((state, labels) -> labels.remove(atomicProposition)); } - public String introduceFreshAtomicProposition() { - int i = 0; - while (true) { - String atomicProposition = "a_" + i; - if (!atomicPropositions.contains(atomicProposition)) { - atomicPropositions.add(atomicProposition); - return atomicProposition; - } - i++; - } - } - public void clearInitialStates() { initialStates.clear(); } - public void addInitialState(String state) { + public void addInitialState(State state) { initialStates.add(state); } @@ -230,31 +227,27 @@ public String toString() { return toJson(); } - public Set getStates() { + public Set getStates() { return states; } - public Set getInitialStates() { + public Set getInitialStates() { return initialStates; } - // todo: low hanging fruit: precompute successors - public List getSuccessors(String state) { - return transitions.stream() - .filter(transition -> transition.getFrom().equals(state)) - .map(TSTransition::getTo) - .toList(); + public Set getSuccessors(State state) { + return successors.getOrDefault(state, new HashSet<>()); } - public Set getAtomicPropositions() { + public Set getAtomicPropositions() { return atomicPropositions; } - public void addLabel(String state, String atomicProposition) { + public void addLabel(State state, APType atomicProposition) { labelingFunction.get(state).add(atomicProposition); } - public Set getLabel(String state) { + public Set getLabel(State 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 85b5399..2eb37f3 100644 --- a/src/main/java/me/paultristanwagner/modelchecking/ts/TransitionSystemBuilder.java +++ b/src/main/java/me/paultristanwagner/modelchecking/ts/TransitionSystemBuilder.java @@ -1,86 +1,93 @@ package me.paultristanwagner.modelchecking.ts; import java.util.*; +import me.paultristanwagner.modelchecking.automaton.State; -public class TransitionSystemBuilder { +public class TransitionSystemBuilder { - private final Set states; - private final Set transitions; - private final Set initialStates; - private final Set atomicPropositions; - private final Map> labelingFunction; + private final Set states; + private final Map> successors; + private final Set initialStates; + private final Set atomicPropositions; + private final Map> labelingFunction; public TransitionSystemBuilder() { this.states = new HashSet<>(); - this.transitions = new HashSet<>(); + this.successors = new HashMap<>(); this.initialStates = new HashSet<>(); this.atomicPropositions = new HashSet<>(); this.labelingFunction = new HashMap<>(); } - public TransitionSystemBuilder addStates(String... states) { - for (String state : states) { + public TransitionSystemBuilder addStates(State... states) { + for (State state : states) { addState(state); } return this; } - public TransitionSystemBuilder addState(String state) { + public TransitionSystemBuilder addState(State state) { this.states.add(state); return this; } - public TransitionSystemBuilder addTransition(TSTransition transition) { - this.transitions.add(transition); + public TransitionSystemBuilder addTransition(State from, State to) { + this.successors.compute( + from, + (k, v) -> { + if (v == null) { + Set successors = new HashSet<>(); + successors.add(to); + return successors; + } else { + v.add(to); + return v; + } + }); return this; } - public TransitionSystemBuilder addTransition(String from, String to) { - this.transitions.add(TSTransition.of(from, to)); - return this; - } - - public TransitionSystemBuilder addInitialState(String initialState) { + public TransitionSystemBuilder addInitialState(State initialState) { this.initialStates.add(initialState); return this; } - public TransitionSystemBuilder setAtomicPropositions(String... atomicPropositions) { + public final TransitionSystemBuilder setAtomicPropositions(APType... atomicPropositions) { return setAtomicPropositions(Arrays.asList(atomicPropositions)); } - public TransitionSystemBuilder setAtomicPropositions(List atomicPropositions) { + public TransitionSystemBuilder setAtomicPropositions(List atomicPropositions) { this.atomicPropositions.clear(); this.atomicPropositions.addAll(atomicPropositions); return this; } - public TransitionSystemBuilder addAtomicProposition(String atomicProposition) { + public TransitionSystemBuilder addAtomicProposition(APType atomicProposition) { this.atomicPropositions.add(atomicProposition); return this; } - public TransitionSystemBuilder addLabel(String state, String atomicProposition) { - Set labels = labelingFunction.computeIfAbsent(state, k -> new HashSet<>()); - labels.add(atomicProposition); + public TransitionSystemBuilder addLabel(State state, APType atomicProposition) { + Set label = labelingFunction.computeIfAbsent(state, k -> new HashSet<>()); + label.add(atomicProposition); return this; } - public TransitionSystemBuilder addLabels(String state, String... atomicPropositions) { - Set labels = labelingFunction.computeIfAbsent(state, k -> new HashSet<>()); + public TransitionSystemBuilder addLabels(State state, APType... atomicPropositions) { + Set labels = labelingFunction.computeIfAbsent(state, k -> new HashSet<>()); labels.addAll(Arrays.asList(atomicPropositions)); return this; } - public TransitionSystem build() { - return new TransitionSystem( - states, transitions, initialStates, atomicPropositions, labelingFunction); + public TransitionSystem build() { + return new TransitionSystem<>( + states, successors, initialStates, atomicPropositions, labelingFunction); } - public Set getInitialStates() { + public Set getInitialStates() { return initialStates; } } diff --git a/src/main/java/me/paultristanwagner/modelchecking/ts/TransitionSystemLoader.java b/src/main/java/me/paultristanwagner/modelchecking/ts/TransitionSystemLoader.java index c5183ee..b78ee67 100644 --- a/src/main/java/me/paultristanwagner/modelchecking/ts/TransitionSystemLoader.java +++ b/src/main/java/me/paultristanwagner/modelchecking/ts/TransitionSystemLoader.java @@ -9,17 +9,17 @@ public class TransitionSystemLoader { - public static TransitionSystem load(String path) throws IOException { + public static BasicTransitionSystem load(String path) throws IOException { File file = new File(path); return load(file); } - public static TransitionSystem load(File file) throws IOException { + public static BasicTransitionSystem load(File file) throws IOException { String fileContent = new String(Files.readAllBytes(file.toPath())); return fromJson(fileContent); } - public static TransitionSystem fromJson(String string) { - return GSON.fromJson(string, new TypeToken() {}.getType()); + public static BasicTransitionSystem fromJson(String string) { + return GSON.fromJson(string, new TypeToken() {}.getType()); } } diff --git a/src/main/java/me/paultristanwagner/modelchecking/util/GsonUtil.java b/src/main/java/me/paultristanwagner/modelchecking/util/GsonUtil.java index c90d28a..24690c3 100644 --- a/src/main/java/me/paultristanwagner/modelchecking/util/GsonUtil.java +++ b/src/main/java/me/paultristanwagner/modelchecking/util/GsonUtil.java @@ -4,17 +4,30 @@ import com.google.gson.GsonBuilder; import com.google.gson.reflect.TypeToken; import java.util.Set; -import me.paultristanwagner.modelchecking.automaton.NBATransition; -import me.paultristanwagner.modelchecking.ts.TSTransition; +import me.paultristanwagner.modelchecking.automaton.*; public class GsonUtil { static { GSON = new GsonBuilder() - .registerTypeAdapter(TSTransition.class, new TSTransition.TSTransitionAdapter()) - .registerTypeAdapter(new TypeToken>() {}.getType(), new NBATransition.BasicNBATransitionAdapter()) - .registerTypeAdapter(new TypeToken>>() {}.getType(), new NBATransition.AdvancedNBATransitionAdapter()) + .registerTypeAdapter( + new TypeToken>() {}.getType(), + new TransitionFunction.BasicTransitionFunctionAdapter()) + .registerTypeAdapter( + new TypeToken>>() {}.getType(), + new TransitionFunction.AdvancedTransitionFunctionAdapter()) + .registerTypeAdapter( + new TypeToken>>() {}.getType(), + new NBATransition.AdvancedNBATransitionAdapter()) + .registerTypeAdapter( + new TypeToken>() {}.getType(), + new NBATransition.BasicNBATransitionAdapter()) + .registerTypeAdapter(State.class, new BasicState.BasicStateJsonAdapter()) + .registerTypeAdapter(BasicState.class, new BasicState.BasicStateJsonAdapter()) + .registerTypeAdapter( + new TypeToken>() {}.getType(), + new SetState.SetStateJsonAdapter()) .setPrettyPrinting() .create(); } diff --git a/src/main/java/me/paultristanwagner/modelchecking/util/Pair.java b/src/main/java/me/paultristanwagner/modelchecking/util/Pair.java index 5a258c0..85fa9db 100644 --- a/src/main/java/me/paultristanwagner/modelchecking/util/Pair.java +++ b/src/main/java/me/paultristanwagner/modelchecking/util/Pair.java @@ -7,7 +7,7 @@ public class Pair { private final A a; private final B b; - private Pair(A a, B b) { + protected Pair(A a, B b) { this.a = a; this.b = b; } diff --git a/src/main/java/me/paultristanwagner/modelchecking/util/Symbol.java b/src/main/java/me/paultristanwagner/modelchecking/util/Symbol.java index 2f0c0d8..100c65d 100644 --- a/src/main/java/me/paultristanwagner/modelchecking/util/Symbol.java +++ b/src/main/java/me/paultristanwagner/modelchecking/util/Symbol.java @@ -2,24 +2,24 @@ public class Symbol { - public static final String NOT_SYMBOL = "¬"; - public static final String AND_SYMBOL = "∧"; - public static final String OR_SYMBOL = "∨"; - public static final String IMPLICATION_SYMBOL = "→"; - public static final String NEXT_SYMBOL = "◯"; - public static final String UNTIL_SYMBOL = "U"; - public static final String EVENTUALLY_SYMBOL = "◊"; - public static final String ALWAYS_SYMBOL = "□"; - public static final String UNIVERSAL_QUANTIFIER_SYMBOL = "∀"; - public static final String EXISTENTIAL_QUANTIFIER_SYMBOL = "∃"; + public static final String NOT = "¬"; + public static final String AND = "∧"; + public static final String OR = "∨"; + public static final String IMPLICATION = "→"; + public static final String NEXT = "◯"; + public static final String UNTIL = "U"; + public static final String EVENTUALLY = "◊"; + public static final String ALWAYS = "□"; + public static final String UNIVERSAL_QUANTIFIER = "∀"; + public static final String EXISTENTIAL_QUANTIFIER = "∃"; - public static final String LOWERCASE_PHI_SYMBOL = "φ"; - public static final String UPPERCASE_PHI_SYMBOL = "Φ"; + public static final String LOWERCASE_PHI = "φ"; + public static final String UPPERCASE_PHI = "Φ"; public static final String LOWERCASE_OMEGA = "ω"; - public static final String MODELS_SYMBOL = "⊨"; - public static final String NOT_MODELS_SYMBOL = "⊭"; + public static final String MODELS = "⊨"; + public static final String NOT_MODELS = "⊭"; public static final String CHECKMARK = "✓"; public static final String CROSS = "✗"; diff --git a/src/main/java/me/paultristanwagner/modelchecking/util/TupleUtil.java b/src/main/java/me/paultristanwagner/modelchecking/util/TupleUtil.java deleted file mode 100644 index 45a6e36..0000000 --- a/src/main/java/me/paultristanwagner/modelchecking/util/TupleUtil.java +++ /dev/null @@ -1,17 +0,0 @@ -package me.paultristanwagner.modelchecking.util; - -public class TupleUtil { - - public static String stringTuple(Object... o) { - StringBuilder sb = new StringBuilder(); - sb.append("("); - for (int i = 0; i < o.length; i++) { - sb.append(o[i]); - if (i < o.length - 1) { - sb.append(","); - } - } - sb.append(")"); - return sb.toString(); - } -} diff --git a/src/test/java/me/paultristanwagner/modelchecking/CTLModelCheckerTest.java b/src/test/java/me/paultristanwagner/modelchecking/CTLModelCheckerTest.java index 4c2ee61..ec52c6e 100644 --- a/src/test/java/me/paultristanwagner/modelchecking/CTLModelCheckerTest.java +++ b/src/test/java/me/paultristanwagner/modelchecking/CTLModelCheckerTest.java @@ -11,7 +11,7 @@ import me.paultristanwagner.modelchecking.ctl.CTLModelCheckingResult; import me.paultristanwagner.modelchecking.ctl.formula.state.CTLFormula; import me.paultristanwagner.modelchecking.ctl.parse.CTLParser; -import me.paultristanwagner.modelchecking.ts.TransitionSystem; +import me.paultristanwagner.modelchecking.ts.BasicTransitionSystem; import me.paultristanwagner.modelchecking.ts.TransitionSystemLoader; import org.junit.jupiter.api.BeforeAll; import org.junit.jupiter.api.Test; @@ -37,7 +37,7 @@ public class CTLModelCheckerTest { "exists always exists next (not a and not b)" }; - private static TransitionSystem ts; + private static BasicTransitionSystem ts; private static CTLParser parser; private static CTLModelChecker modelChecker; diff --git a/src/test/java/me/paultristanwagner/modelchecking/CTLStarModelCheckerTest.java b/src/test/java/me/paultristanwagner/modelchecking/CTLStarModelCheckerTest.java index 0c6c7fb..14bedab 100644 --- a/src/test/java/me/paultristanwagner/modelchecking/CTLStarModelCheckerTest.java +++ b/src/test/java/me/paultristanwagner/modelchecking/CTLStarModelCheckerTest.java @@ -11,7 +11,7 @@ import me.paultristanwagner.modelchecking.ctlstar.CTLStarModelCheckingResult; import me.paultristanwagner.modelchecking.ctlstar.formula.CTLStarFormula; import me.paultristanwagner.modelchecking.ctlstar.parse.CTLStarParser; -import me.paultristanwagner.modelchecking.ts.TransitionSystem; +import me.paultristanwagner.modelchecking.ts.BasicTransitionSystem; import me.paultristanwagner.modelchecking.ts.TransitionSystemLoader; import org.junit.jupiter.api.BeforeAll; import org.junit.jupiter.api.Test; @@ -37,7 +37,7 @@ public class CTLStarModelCheckerTest { "exists always exists next (not a and not b)" }; - private static TransitionSystem ts; + private static BasicTransitionSystem ts; private static CTLStarParser parser; private static CTLStarModelChecker modelChecker; diff --git a/src/test/java/me/paultristanwagner/modelchecking/LTLModelCheckerTest.java b/src/test/java/me/paultristanwagner/modelchecking/LTLModelCheckerTest.java index 0f3062d..ae3c989 100644 --- a/src/test/java/me/paultristanwagner/modelchecking/LTLModelCheckerTest.java +++ b/src/test/java/me/paultristanwagner/modelchecking/LTLModelCheckerTest.java @@ -11,7 +11,7 @@ import me.paultristanwagner.modelchecking.ltl.LTLModelCheckingResult; import me.paultristanwagner.modelchecking.ltl.formula.LTLFormula; import me.paultristanwagner.modelchecking.ltl.parse.LTLParser; -import me.paultristanwagner.modelchecking.ts.TransitionSystem; +import me.paultristanwagner.modelchecking.ts.BasicTransitionSystem; import me.paultristanwagner.modelchecking.ts.TransitionSystemLoader; import org.junit.jupiter.api.BeforeAll; import org.junit.jupiter.api.Test; @@ -36,7 +36,7 @@ public class LTLModelCheckerTest { "(always eventually a) and (eventually always b)" }; - private static TransitionSystem ts; + private static BasicTransitionSystem ts; private static LTLParser parser; private static LTLModelChecker modelChecker; diff --git a/src/test/java/me/paultristanwagner/modelchecking/SynchronousProductTest.java b/src/test/java/me/paultristanwagner/modelchecking/SynchronousProductTest.java index cb3738d..efc206f 100644 --- a/src/test/java/me/paultristanwagner/modelchecking/SynchronousProductTest.java +++ b/src/test/java/me/paultristanwagner/modelchecking/SynchronousProductTest.java @@ -1,12 +1,14 @@ package me.paultristanwagner.modelchecking; +import static me.paultristanwagner.modelchecking.util.GsonUtil.GSON; + import com.google.gson.reflect.TypeToken; import java.io.IOException; import java.io.InputStream; import java.util.Set; import me.paultristanwagner.modelchecking.automaton.NBA; +import me.paultristanwagner.modelchecking.automaton.State; import me.paultristanwagner.modelchecking.ts.TransitionSystem; -import me.paultristanwagner.modelchecking.ts.TransitionSystemLoader; import org.junit.jupiter.api.Assertions; import org.junit.jupiter.api.Test; @@ -17,14 +19,15 @@ public void testSynchronousProduct() throws IOException { InputStream tsInputStream = getClass().getClassLoader().getResourceAsStream("ts_message_delivery.json"); String tsJson = new String(tsInputStream.readAllBytes()); - TransitionSystem ts = TransitionSystemLoader.fromJson(tsJson); + TransitionSystem ts = + GSON.fromJson(tsJson, new TypeToken>() {}.getType()); InputStream nbaInputStream = getClass().getClassLoader().getResourceAsStream("nba_never_delivered.json"); String nbaJson = new String(nbaInputStream.readAllBytes()); NBA> nba = NBA.fromJson(nbaJson, new TypeToken>>() {}.getType()); - TransitionSystem result = ts.reachableSynchronousProduct(nba); + TransitionSystem result = ts.reachableSynchronousProduct(nba); Assertions.assertNotNull(result); Assertions.assertEquals(10, result.getStates().size()); diff --git a/src/test/resources/gnba_inf_crit1_and_inf_crit2.json b/src/test/resources/gnba_inf_crit1_and_inf_crit2.json index 397fb03..742c932 100644 --- a/src/test/resources/gnba_inf_crit1_and_inf_crit2.json +++ b/src/test/resources/gnba_inf_crit1_and_inf_crit2.json @@ -1,50 +1,16 @@ { - "states": [ - "q0", - "q1", - "q2" - ], - "alphabet": [ - "true", - "crit1", - "crit2" - ], - "initialStates": [ - "q0" - ], + "states": ["q0", "q1", "q2"], + "alphabet": ["true", "crit1", "crit2"], + "initialStates": ["q0"], "acceptingSets": [ - [ - "q1" - ], - [ - "q2" - ] + ["q1"], + ["q2"] ], - "transitions": [ - [ - "q0", - "true", - "q0" - ], - [ - "q0", - "crit1", - "q1" - ], - [ - "q1", - "true", - "q0" - ], - [ - "q0", - "crit2", - "q2" - ], - [ - "q2", - "true", - "q0" - ] + "transitionFunction": [ + ["q0", "true", "q0"], + ["q0", "crit1", "q1"], + ["q1", "true", "q0"], + ["q0", "crit2", "q2"], + ["q2", "true", "q0"] ] } \ No newline at end of file diff --git a/src/test/resources/nba_fin_a.json b/src/test/resources/nba_fin_a.json index 558ec48..27d4adf 100644 --- a/src/test/resources/nba_fin_a.json +++ b/src/test/resources/nba_fin_a.json @@ -1,30 +1,11 @@ { - "states": [ - "q0", - "q1" - ], - "alphabet": [], - "initialStates": [ - "q0" - ], - "acceptingStates": [ - "q1" - ], - "transitions": [ - [ - "q0", - "A", - "q0" - ], - [ - "q0", - "", - "q1" - ], - [ - "q1", - "", - "q1" - ] + "states": ["q0", "q1"], + "alphabet": ["A"], + "initialStates": ["q0"], + "acceptingStates": ["q1"], + "transitionFunction": [ + ["q0", "A", "q0"], + ["q0", "", "q1"], + ["q1", "", "q1"] ] } \ No newline at end of file diff --git a/src/test/resources/nba_inf_a_1.json b/src/test/resources/nba_inf_a_1.json index 1fcb319..7e41ebd 100644 --- a/src/test/resources/nba_inf_a_1.json +++ b/src/test/resources/nba_inf_a_1.json @@ -1,27 +1,10 @@ { - "states": [ - "q1", - "q2" - ], - "alphabet": [ - "A" - ], - "initialStates": [ - "q1" - ], - "acceptingStates": [ - "q1" - ], - "transitions": [ - [ - "q1", - "A", - "q2" - ], - [ - "q2", - "A", - "q1" - ] + "states": ["q1", "q2"], + "alphabet": ["A"], + "initialStates": ["q1"], + "acceptingStates": ["q1"], + "transitionFunction": [ + ["q1", "A", "q2"], + ["q2", "A", "q1"] ] } \ No newline at end of file diff --git a/src/test/resources/nba_inf_a_2.json b/src/test/resources/nba_inf_a_2.json index d299d86..f8f37d8 100644 --- a/src/test/resources/nba_inf_a_2.json +++ b/src/test/resources/nba_inf_a_2.json @@ -1,27 +1,10 @@ { - "states": [ - "p1", - "p2" - ], - "alphabet": [ - "A" - ], - "initialStates": [ - "p1" - ], - "acceptingStates": [ - "p2" - ], - "transitions": [ - [ - "p1", - "A", - "p2" - ], - [ - "p2", - "A", - "p1" - ] + "states": ["p1", "p2"], + "alphabet": ["A"], + "initialStates": ["p1"], + "acceptingStates": ["p2"], + "transitionFunction": [ + ["p1", "A", "p2"], + ["p2", "A", "p1"] ] } \ No newline at end of file diff --git a/src/test/resources/nba_never_delivered.json b/src/test/resources/nba_never_delivered.json index f96ba68..2b7d70c 100644 --- a/src/test/resources/nba_never_delivered.json +++ b/src/test/resources/nba_never_delivered.json @@ -1,7 +1,9 @@ { "states": ["q0","qF","q1"], "alphabet": ["start","delivered","lost","try_to_send"], - "transitions": [ + "initialStates": ["q0"], + "acceptingStates": ["qF"], + "transitionFunction": [ ["q0", ["try_to_send"], "qF"], ["q0", [], "q0"], ["q0", ["start"], "q0"], @@ -18,7 +20,5 @@ ["q1", ["delivered"], "q1"], ["q1", ["lost"], "q1"], ["q1", ["try_to_send"], "q1"] - ], - "initialStates": ["q0"], - "acceptingStates": ["qF"] + ] } \ No newline at end of file diff --git a/src/test/resources/ts_message_delivery.json b/src/test/resources/ts_message_delivery.json index a3a7c28..74c48fe 100644 --- a/src/test/resources/ts_message_delivery.json +++ b/src/test/resources/ts_message_delivery.json @@ -1,14 +1,13 @@ { - "states": ["start","try_to_send","lost","delivered"], - "transitions": [ - ["start","try_to_send"], - ["try_to_send","lost"], - ["lost","try_to_send"], - ["try_to_send","delivered"], - ["delivered","start"] - ], + "states": ["start", "try_to_send", "lost", "delivered"], "initialStates": ["start"], - "atomicPropositions": ["start","try_to_send","lost","delivered"], + "successors": { + "start": ["try_to_send"], + "try_to_send": ["lost", "delivered"], + "lost": ["try_to_send"], + "delivered": ["start"] + }, + "atomicPropositions": ["start", "try_to_send", "lost", "delivered"], "labelingFunction": { "start": ["start"], "try_to_send": ["try_to_send"],