Skip to content

Commit

Permalink
Add printing of witnesses in documentation.
Browse files Browse the repository at this point in the history
  • Loading branch information
@weetmuts
weetmuts committed May 23, 2021
1 parent dcdf73c commit ef15f40
Show file tree
Hide file tree
Showing 26 changed files with 1,036 additions and 71 deletions.
10 changes: 10 additions & 0 deletions .gitignore
View file
Original file line number Diff line number Diff line change
@@ -1 +1,11 @@
build
*.bpo
*.bps
*.bcc
*.bcm
*.aux
*.bcf
*.log
*.rai
*.rao
*.toc
2 changes: 1 addition & 1 deletion src/main/java/com/viklauverk/eventbtools/core/BaseDocGen.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -94,7 +94,7 @@ public String suffix()

public abstract String generateDocument() throws Exception;

public String renderParts(Canvas cnvs, String pattern) throws Exception
public String renderParts(Canvas cnvs, String pattern)
{
AllRenders ar = sys().lookupRenders(cnvs.renderTarget(),
cnvs);
Expand Down
34 changes: 34 additions & 0 deletions src/main/java/com/viklauverk/eventbtools/core/Canvas.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -779,6 +779,40 @@ public void stopGuard()
assert (false) : "Unknown encoding "+render_target_;
}

public void startWitness()
{
switch (render_target_)
{
case PLAIN:
return;
case TERMINAL:
return;
case TEX:
append("\\WIT{");
return;
case HTMQ:
return;
}
assert (false) : "Unknown encoding "+render_target_;
}

public void stopWitness()
{
switch (render_target_)
{
case PLAIN:
return;
case TERMINAL:
return;
case TEX:
append("}");
return;
case HTMQ:
return;
}
assert (false) : "Unknown encoding "+render_target_;
}

public void startAction()
{
switch (render_target_)
Expand Down
98 changes: 47 additions & 51 deletions src/main/java/com/viklauverk/eventbtools/core/Console.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -126,21 +126,15 @@ String renderPart(String name, RenderTarget rt, RenderAttributes ra)
BaseDocGen bdg = DocGen.lookup(cs, ds, sys_);

String result = "";
try
{
Canvas cnvs = sys().console().currentCanvas();
cnvs.setRenderTarget(rt);
cnvs.setRenderAttributes(ra);
cnvs.clear();
result = bdg.renderParts(cnvs, name);
if (ra.frame())
{
result = cnvs.frame("", result, Canvas.sline);
}
}
catch (Exception e)

Canvas cnvs = sys().console().currentCanvas();
cnvs.setRenderTarget(rt);
cnvs.setRenderAttributes(ra);
cnvs.clear();
result = bdg.renderParts(cnvs, name);
if (ra.frame())
{
return e.getMessage();
result = cnvs.frame("", result, Canvas.sline);
}
return result;
}
Expand Down Expand Up @@ -282,50 +276,52 @@ public String go(String line_in)
{
log.debug("expanded command: '%s' to '%s'", line_in, line);
}
CharStream lineStream = CharStreams.fromString(line);

ConsoleLexer lexer = new ConsoleLexer(lineStream);
CommonTokenStream tokens = new CommonTokenStream(lexer);
ConsoleParser parser = new ConsoleParser(tokens);
//parser.setTrace(true);
lexer.removeErrorListeners();
parser.removeErrorListeners();
parser.addErrorListener(ThrowingErrorListener.INSTANCE);

log.debug("go: %s", line);
ParseTree tree = null;
try
{
CharStream lineStream = CharStreams.fromString(line);

ConsoleLexer lexer = new ConsoleLexer(lineStream);
CommonTokenStream tokens = new CommonTokenStream(lexer);
ConsoleParser parser = new ConsoleParser(tokens);
//parser.setTrace(true);
lexer.removeErrorListeners();
parser.removeErrorListeners();
parser.addErrorListener(ThrowingErrorListener.INSTANCE);

try
{
log.debug("go: %s", line);
ParseTree tree = parser.start();
if (parser.getNumberOfSyntaxErrors() > 0)
{
String info = "Could not parse: \""+line+"\" since it has "+
parser.getNumberOfSyntaxErrors()+
" syntax errors.\n";
tree = parser.start();
}
catch (Exception e)
{
String info = "Could not parse command: \""+line+"\"\n"+e.getMessage();
log.info("%s", info);
/*
System.out.println("========================");
System.out.println(ReflectionToStringBuilder.toString(parser));
System.out.println("========================");*/
return info;
}
if (parser.getNumberOfSyntaxErrors() > 0)
{
String info = "Could not parse: \""+line+"\" since it has "+
parser.getNumberOfSyntaxErrors()+
" syntax errors.\n";

log.debug(info);
return info;
}
log.debug("%s", info);
return info;
}

ConsoleExecutor ce = new ConsoleExecutor(this, tokens);
return ce.visit(tree);
}
catch (Exception e)
{
String info = "Could not parse command: \""+line+"\"\n"+e.getMessage();
log.info(info);
System.out.println("========================");
System.out.println(ReflectionToStringBuilder.toString(parser));
System.out.println("========================");
return info;
}
try
{
ConsoleExecutor ce = new ConsoleExecutor(this, tokens);
return ce.visit(tree);
}
catch (Exception e)
{
String info = "Exception when parsing: \""+line+"\"\n"+e.getMessage();
log.debug(info);
return info;
e.printStackTrace();
log.info("Could not execute command \"%s\"", line);
return "FAILED COMMAND \""+line+"\"";
}
}

Expand Down
2 changes: 1 addition & 1 deletion src/main/java/com/viklauverk/eventbtools/core/ConsoleExecutor.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -449,7 +449,7 @@ public String visitShowPart(ConsoleParser.ShowPartContext ctx)
String content = console_.renderPart(pattern, rt, ra);
if (content == null)
{
return "EVBT_ERROR: Part "+pattern+" not found!";
return "EVBT_ERROR: Part \""+pattern+"\" not found!";
}
return content;
}
Expand Down
46 changes: 46 additions & 0 deletions src/main/java/com/viklauverk/eventbtools/core/Event.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -47,6 +47,9 @@ public class Event
private Map<String,Guard> guards_;
private List<Guard> guard_ordering_;
private List<String> guard_names_;
private Map<String,Witness> witnesses_;
private List<Witness> witness_ordering_;
private List<String> witness_names_;
private Map<String,Action> actions_;
private List<Action> action_ordering_;
private List<String> action_names_;
Expand All @@ -73,6 +76,10 @@ public Event(String n, boolean e, String comment, Machine m, Convergence c)
guard_ordering_ = new ArrayList<>();
guard_names_ = new ArrayList<>();

witnesses_ = new HashMap<>();
witness_ordering_ = new ArrayList<>();
witness_names_ = new ArrayList<>();

actions_ = new HashMap<>();
action_ordering_ = new ArrayList<>();
action_names_ = new ArrayList<>();
Expand Down Expand Up @@ -163,6 +170,11 @@ public boolean hasGuards()
return guards_.size() > 0;
}

public boolean hasWitnesses()
{
return witnesses_.size() > 0;
}

public boolean hasActions()
{
return actions_.size() > 0;
Expand Down Expand Up @@ -218,6 +230,28 @@ public Guard getGuard(String name)
return guards_.get(name);
}

public void addWitness(Witness witness)
{
witnesses_.put(witness.name(), witness);
witness_ordering_.add(witness);
witness_names_ = witnesses_.keySet().stream().sorted().collect(Collectors.toList());
}

public List<Witness> witnessOrdering()
{
return witness_ordering_;
}

public List<String> witnessNames()
{
return witness_names_;
}

public Witness getWitness(String name)
{
return witnesses_.get(name);
}

public void addAction(Action action)
{
actions_.put(action.name(), action);
Expand Down Expand Up @@ -340,6 +374,18 @@ public void parse()
sys().typing().extractInfoFromGuard(g, symbol_table_);
}

for (String name : witnessNames())
{
Witness w = getWitness(name);
// The witness formula contains a variable that does not exist in this symbol table!
// This is the disappearing variable for which the witness establishes a replacement relation.
// The Rodin format specifies the witnes name as the label. Odd location perhaps. But it works.
// Lets add the symbol to the symbol table before parsing.
symbol_table_.addVariableSymbol(w.name());
w.parse(symbol_table_);
sys().typing().extractInfoFromWitness(w, symbol_table_);
}

for (String name : actionNames())
{
Action a = getAction(name);
Expand Down
38 changes: 26 additions & 12 deletions src/main/java/com/viklauverk/eventbtools/core/LogModule.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -131,52 +131,66 @@ public static void setLogLevelFor(String modules, LogLevel ll)
}
}

static String safeFormat(String msg, Object... args)
{
try
{
return String.format(msg, args);
}
catch (Exception e)
{
e.printStackTrace();
System.exit(1);
}
return "ERROR_FORMATTING "+msg;
}

public void error(String msg, Object... args)
{
String m = "("+module_+") "+String.format(msg, args);
String m = "("+module_+") "+safeFormat(msg, args);
System.err.println(m);
System.exit(1);
}

public void usageError(String msg, Object... args)
{
String out = String.format(msg, args);
String out = safeFormat(msg, args);
System.out.println(out);
System.exit(1);
}

public static void usageErrorStatic(String msg, Object... args)
{
String out = String.format(msg, args);
String out = safeFormat(msg, args);
System.out.println(out);
System.exit(1);
}

public void internalError(String msg, Object... args)
{
String out = "("+module_+") internal error "+String.format(msg, args);
String out = "("+module_+") internal error "+safeFormat(msg, args);
System.out.println(out);
System.exit(1);
}

private static void internalErrorStatic(String msg, Object... args)
{
String out = "(log) internal error "+String.format(msg, args);
String out = "(log) internal error "+safeFormat(msg, args);
System.out.println(out);
System.exit(1);
}

public void failure(String msg, Object... args)
{
String out = "("+module_+") failure "+String.format(msg, args);
String out = "("+module_+") failure "+safeFormat(msg, args);
System.out.println(out);
}

public void warn(String msg, Object... args)
{
if (log_level_.value() >= LogLevel.WARN.value())
{
String out = "("+module_+") warning "+String.format(msg, args);
String out = "("+module_+") warning "+safeFormat(msg, args);
System.out.println(out);
}
}
Expand All @@ -185,7 +199,7 @@ public void info(String msg, Object... args)
{
if (log_level_.value() >= LogLevel.INFO.value())
{
String out = String.format(msg, args);
String out = safeFormat(msg, args);
System.out.println(out);
}
}
Expand All @@ -194,7 +208,7 @@ public void verbose(String msg, Object... args)
{
if (log_level_.value() >= LogLevel.VERBOSE.value())
{
String out = String.format(msg, args);
String out = safeFormat(msg, args);
System.out.println(out);
}
}
Expand All @@ -203,7 +217,7 @@ public void debug(String msg, Object... args)
{
if (log_level_.value() >= LogLevel.DEBUG.value())
{
String out = "("+module_+") "+String.format(msg, args);
String out = "("+module_+") "+safeFormat(msg, args);
System.out.println(out);
}
}
Expand All @@ -212,7 +226,7 @@ public void debugp(String part, String msg, Object... args)
{
if (log_level_.value() >= LogLevel.DEBUG.value())
{
String out = "("+module_+"-"+part+") "+String.format(msg, args);
String out = "("+module_+"-"+part+") "+safeFormat(msg, args);
System.out.println(out);
}
}
Expand All @@ -221,7 +235,7 @@ public void trace(String msg, Object... args)
{
if (log_level_.value() >= LogLevel.TRACE.value())
{
String out = "("+module_+") "+String.format(msg, args);
String out = "("+module_+") "+safeFormat(msg, args);
System.out.println(out);
}
}
Expand Down
1 change: 1 addition & 0 deletions src/main/java/com/viklauverk/eventbtools/core/LogModuleNames.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,7 @@ public enum LogModuleNames
htmq,
machine,
main,
match,
parser,
pattern,
renderformula,
Expand Down
Loading

0 comments on commit ef15f40

Please sign in to comment.