Conversation
CatarinaGamboa
left a comment
CatarinaGamboa
left a comment
There was a problem hiding this comment.
looks good, check the comments
|
|
||
| public StateConflictError(CtElement element, Predicate predicate, String className) { | ||
| super("State Conflict Error", "Found multiple disjoint states from a StateSet in refinement", element); | ||
| super("State Conflict Error", "Found multiple disjoint states in state transition", element); |
There was a problem hiding this comment.
We could even improve this message to something like "Found multiple disjoint states in state transition - State transition can only go to one state of each state set"
| String name = String.format(freshFormat, context.getCounter()); | ||
| if (c.getVariableNames().contains(WILD_VAR)) { | ||
| c = c.substituteVariable(WILD_VAR, name); | ||
| String name = String.format(Formats.RET, context.getCounter()); |
There was a problem hiding this comment.
why are we changing from fresh to return?
| System.out.println("\nSMT subtyping:" + stringSMT + " <: " + expectedType.toString()); | ||
| System.out.println("--------------------------------------------------------------"); | ||
| } | ||
| // private void printVCs(String string, String stringSMT, Predicate expectedType) { |
There was a problem hiding this comment.
eliminate this code already, we can always go a previous version in git to get them
| Predicate cSMTMessageReady = premises; // substituteByMap(premises, map); | ||
| ErrorHandler.printError(element, s, etMessageReady, cSMTMessageReady, map, errorEmitter); | ||
| } | ||
| // private void printError(Predicate premises, Predicate expectedType, CtElement element, |
| // TODO COMPLETE WITH MORE OPERANDS | ||
| } | ||
| return switch (kind) { | ||
| case PLUS -> Ops.PLUS; |
| } | ||
| return noOld; | ||
| } | ||
| // private static Predicate changeVarsFields(Predicate pred, TypeChecker tc) { |
| case Types.BOOLEAN -> new LiteralBoolean(value); | ||
| case Types.INT, Types.SHORT -> new LiteralInt(value); | ||
| case Types.DOUBLE, Types.LONG -> new LiteralReal(value); | ||
| default -> new LiteralReal(value); |
There was a problem hiding this comment.
in the future if we want to add strings this default can be a problem, maybe we can emit an error or smt
CatarinaGamboa
left a comment
CatarinaGamboa
left a comment
There was a problem hiding this comment.
In a followup for cleanup feel free to remove all code in comments, its just polluting the codebase
2 participants
Cleaned up some code by:
Formats,Keys,Ops,PatternsandTypes