-
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.
Add false and logical or to CTL* grammar
- Loading branch information
BuildTools
committed
Sep 28, 2023
1 parent
2874b8f
commit 2046ead
Showing
8 changed files
with
380 additions
and
47 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
56 changes: 56 additions & 0 deletions
56
src/main/java/me/paultristanwagner/modelchecking/ctlstar/formula/CTLStarFalseFormula.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,56 @@ | ||
| package me.paultristanwagner.modelchecking.ctlstar.formula; | ||
|
|
||
| import java.util.HashSet; | ||
| import java.util.Objects; | ||
| import java.util.Set; | ||
| import me.paultristanwagner.modelchecking.ltl.formula.LTLFalseFormula; | ||
| import me.paultristanwagner.modelchecking.ltl.formula.LTLFormula; | ||
|
|
||
| public class CTLStarFalseFormula extends CTLStarFormula { | ||
|
|
||
| private CTLStarFalseFormula() { | ||
|
|
||
| } | ||
|
|
||
| public static CTLStarFalseFormula FALSE() { | ||
| return new CTLStarFalseFormula(); | ||
| } | ||
|
|
||
|
|
||
| @Override | ||
| public int getDepth() { | ||
| return 1; | ||
| } | ||
|
|
||
| @Override | ||
| public void replaceFormula(CTLStarFormula target, String freshVariable) { | ||
| // nothing to do | ||
| } | ||
|
|
||
| @Override | ||
| public Set<CTLStarFormula> getSubFormulas() { | ||
| Set<CTLStarFormula> subFormulas = new HashSet<>(); | ||
| subFormulas.add(this); | ||
| return subFormulas; | ||
| } | ||
|
|
||
| @Override | ||
| public LTLFormula toLTL() { | ||
| return LTLFalseFormula.FALSE(); | ||
| } | ||
|
|
||
| @Override | ||
| public String toString() { | ||
| return "false"; | ||
| } | ||
|
|
||
| @Override | ||
| public boolean equals(Object obj) { | ||
| return obj instanceof CTLStarFalseFormula; | ||
| } | ||
|
|
||
| @Override | ||
| public int hashCode() { | ||
| return Objects.hash(false); | ||
| } | ||
| } |
98 changes: 98 additions & 0 deletions
98
src/main/java/me/paultristanwagner/modelchecking/ctlstar/formula/CTLStarOrFormula.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,98 @@ | ||
| package me.paultristanwagner.modelchecking.ctlstar.formula; | ||
|
|
||
| import static me.paultristanwagner.modelchecking.util.Symbol.OR_SYMBOL; | ||
|
|
||
| import java.util.*; | ||
| import me.paultristanwagner.modelchecking.ltl.formula.LTLFormula; | ||
| import me.paultristanwagner.modelchecking.ltl.formula.LTLOrFormula; | ||
|
|
||
| public class CTLStarOrFormula extends CTLStarFormula { | ||
|
|
||
| private final List<CTLStarFormula> components; | ||
|
|
||
| private CTLStarOrFormula( List<CTLStarFormula> components ) { | ||
| this.components = components; | ||
| } | ||
|
|
||
| public static CTLStarOrFormula or( List<CTLStarFormula> components ) { | ||
| return new CTLStarOrFormula( components ); | ||
| } | ||
|
|
||
| public static CTLStarOrFormula or( CTLStarFormula... components ) { | ||
| return new CTLStarOrFormula( List.of( components ) ); | ||
| } | ||
|
|
||
| @Override | ||
| public int getDepth() { | ||
| int maxDepth = 0; | ||
| for (CTLStarFormula component : components) { | ||
| maxDepth = Math.max(maxDepth, component.getDepth()); | ||
| } | ||
| return maxDepth + 1; | ||
| } | ||
|
|
||
| @Override | ||
| public void replaceFormula(CTLStarFormula target, String freshVariable) { | ||
| components.replaceAll( | ||
| component -> { | ||
| if (component.equals(target)) { | ||
| return CTLStarIdentifierFormula.identifier(freshVariable); | ||
| } else { | ||
| component.replaceFormula(target, freshVariable); | ||
| return component; | ||
| } | ||
| }); | ||
| } | ||
|
|
||
| @Override | ||
| public Set<CTLStarFormula> getSubFormulas() { | ||
| Set<CTLStarFormula> subFormulas = new HashSet<>(); | ||
| for (CTLStarFormula component : components) { | ||
| subFormulas.addAll(component.getSubFormulas()); | ||
| } | ||
| subFormulas.add(this); | ||
| return subFormulas; | ||
| } | ||
|
|
||
| @Override | ||
| public LTLFormula toLTL() { | ||
| List<LTLFormula> ltlComponents = new ArrayList<>(); | ||
| for (CTLStarFormula component : components) { | ||
| ltlComponents.add(component.toLTL()); | ||
| } | ||
| return LTLOrFormula.or(ltlComponents); | ||
| } | ||
|
|
||
| public List<CTLStarFormula> getComponents() { | ||
| return components; | ||
| } | ||
|
|
||
| @Override | ||
| public String toString() { | ||
| StringBuilder builder = new StringBuilder(); | ||
| for (int i = 0; i < components.size(); i++) { | ||
| builder.append(components.get(i).toString()); | ||
|
|
||
| if (i < components.size() - 1) { | ||
| builder.append(" "); | ||
| builder.append(OR_SYMBOL); | ||
| builder.append(" "); | ||
| } | ||
| } | ||
|
|
||
| return builder.toString(); | ||
| } | ||
|
|
||
| @Override | ||
| public boolean equals(Object o) { | ||
| if (this == o) return true; | ||
| if (o == null || getClass() != o.getClass()) return false; | ||
| CTLStarOrFormula that = (CTLStarOrFormula) o; | ||
| return Objects.equals(components, that.components); | ||
| } | ||
|
|
||
| @Override | ||
| public int hashCode() { | ||
| return Objects.hash(components); | ||
| } | ||
| } |
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
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
Oops, something went wrong.