-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Generify TS, modify transitions and general clean up
- Loading branch information
1 parent
25a41d9
commit d3891f5
Showing
68 changed files
with
1,004 additions
and
944 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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"] | ||
| } | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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"] | ||
| } | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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": [] | ||
| } | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
7 changes: 4 additions & 3 deletions
7
src/main/java/me/paultristanwagner/modelchecking/ModelChecker.java
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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<T extends Formula, R extends ModelCheckingResult> { | ||
|
|
||
| R check(TransitionSystem ts, T formula); | ||
| R check(BasicTransitionSystem ts, T formula); | ||
|
|
||
| Set<String> sat(TransitionSystem ts, T formula); | ||
| Set<State> sat(BasicTransitionSystem ts, T formula); | ||
| } |
48 changes: 48 additions & 0 deletions
48
src/main/java/me/paultristanwagner/modelchecking/automaton/BasicState.java
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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<BasicState>, JsonDeserializer<BasicState> { | ||
|
|
||
| @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); | ||
| } | ||
| } | ||
| } |
Oops, something went wrong.