Version 1.2- project has been converted to a maven project

This commit is contained in:
ulfur 2020-03-15 16:52:05 +01:00
commit 9cbeb3b1dd
470 changed files with 18663 additions and 0 deletions

21
.classpath Normal file
View File

@ -0,0 +1,21 @@
<?xml version="1.0" encoding="UTF-8"?>
<classpath>
<classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER/org.eclipse.jdt.internal.debug.ui.launcher.StandardVMType/JavaSE-11">
<attributes>
<attribute name="maven.pomderived" value="true"/>
</attributes>
</classpathentry>
<classpathentry kind="con" path="org.eclipse.m2e.MAVEN2_CLASSPATH_CONTAINER">
<attributes>
<attribute name="maven.pomderived" value="true"/>
<attribute name="module" value="true"/>
</attributes>
</classpathentry>
<classpathentry kind="src" output="target/classes" path="src">
<attributes>
<attribute name="optional" value="true"/>
<attribute name="maven.pomderived" value="true"/>
</attributes>
</classpathentry>
<classpathentry kind="output" path="target/classes"/>
</classpath>

23
.project Normal file
View File

@ -0,0 +1,23 @@
<?xml version="1.0" encoding="UTF-8"?>
<projectDescription>
<name>OFMCGUI</name>
<comment></comment>
<projects>
</projects>
<buildSpec>
<buildCommand>
<name>org.eclipse.jdt.core.javabuilder</name>
<arguments>
</arguments>
</buildCommand>
<buildCommand>
<name>org.eclipse.m2e.core.maven2Builder</name>
<arguments>
</arguments>
</buildCommand>
</buildSpec>
<natures>
<nature>org.eclipse.m2e.core.maven2Nature</nature>
<nature>org.eclipse.jdt.core.javanature</nature>
</natures>
</projectDescription>

View File

@ -0,0 +1,3 @@
eclipse.preferences.version=1
encoding/<project>=UTF-8
encoding/src=UTF-8

View File

@ -0,0 +1,114 @@
eclipse.preferences.version=1
org.eclipse.jdt.core.compiler.annotation.inheritNullAnnotations=disabled
org.eclipse.jdt.core.compiler.annotation.missingNonNullByDefaultAnnotation=ignore
org.eclipse.jdt.core.compiler.annotation.nonnull=org.eclipse.jdt.annotation.NonNull
org.eclipse.jdt.core.compiler.annotation.nonnull.secondary=
org.eclipse.jdt.core.compiler.annotation.nonnullbydefault=org.eclipse.jdt.annotation.NonNullByDefault
org.eclipse.jdt.core.compiler.annotation.nonnullbydefault.secondary=
org.eclipse.jdt.core.compiler.annotation.nullable=org.eclipse.jdt.annotation.Nullable
org.eclipse.jdt.core.compiler.annotation.nullable.secondary=
org.eclipse.jdt.core.compiler.annotation.nullanalysis=disabled
org.eclipse.jdt.core.compiler.codegen.inlineJsrBytecode=enabled
org.eclipse.jdt.core.compiler.codegen.targetPlatform=11
org.eclipse.jdt.core.compiler.codegen.unusedLocal=preserve
org.eclipse.jdt.core.compiler.compliance=11
org.eclipse.jdt.core.compiler.debug.lineNumber=generate
org.eclipse.jdt.core.compiler.debug.localVariable=generate
org.eclipse.jdt.core.compiler.debug.sourceFile=generate
org.eclipse.jdt.core.compiler.problem.APILeak=warning
org.eclipse.jdt.core.compiler.problem.annotationSuperInterface=warning
org.eclipse.jdt.core.compiler.problem.assertIdentifier=error
org.eclipse.jdt.core.compiler.problem.autoboxing=ignore
org.eclipse.jdt.core.compiler.problem.comparingIdentical=warning
org.eclipse.jdt.core.compiler.problem.deadCode=warning
org.eclipse.jdt.core.compiler.problem.deprecation=warning
org.eclipse.jdt.core.compiler.problem.deprecationInDeprecatedCode=disabled
org.eclipse.jdt.core.compiler.problem.deprecationWhenOverridingDeprecatedMethod=disabled
org.eclipse.jdt.core.compiler.problem.discouragedReference=warning
org.eclipse.jdt.core.compiler.problem.emptyStatement=ignore
org.eclipse.jdt.core.compiler.problem.enablePreviewFeatures=disabled
org.eclipse.jdt.core.compiler.problem.enumIdentifier=error
org.eclipse.jdt.core.compiler.problem.explicitlyClosedAutoCloseable=ignore
org.eclipse.jdt.core.compiler.problem.fallthroughCase=ignore
org.eclipse.jdt.core.compiler.problem.fatalOptionalError=disabled
org.eclipse.jdt.core.compiler.problem.fieldHiding=ignore
org.eclipse.jdt.core.compiler.problem.finalParameterBound=warning
org.eclipse.jdt.core.compiler.problem.finallyBlockNotCompletingNormally=warning
org.eclipse.jdt.core.compiler.problem.forbiddenReference=warning
org.eclipse.jdt.core.compiler.problem.hiddenCatchBlock=warning
org.eclipse.jdt.core.compiler.problem.includeNullInfoFromAsserts=disabled
org.eclipse.jdt.core.compiler.problem.incompatibleNonInheritedInterfaceMethod=warning
org.eclipse.jdt.core.compiler.problem.incompleteEnumSwitch=warning
org.eclipse.jdt.core.compiler.problem.indirectStaticAccess=ignore
org.eclipse.jdt.core.compiler.problem.localVariableHiding=ignore
org.eclipse.jdt.core.compiler.problem.methodWithConstructorName=warning
org.eclipse.jdt.core.compiler.problem.missingDefaultCase=ignore
org.eclipse.jdt.core.compiler.problem.missingDeprecatedAnnotation=ignore
org.eclipse.jdt.core.compiler.problem.missingEnumCaseDespiteDefault=disabled
org.eclipse.jdt.core.compiler.problem.missingHashCodeMethod=ignore
org.eclipse.jdt.core.compiler.problem.missingOverrideAnnotation=ignore
org.eclipse.jdt.core.compiler.problem.missingOverrideAnnotationForInterfaceMethodImplementation=enabled
org.eclipse.jdt.core.compiler.problem.missingSerialVersion=warning
org.eclipse.jdt.core.compiler.problem.missingSynchronizedOnInheritedMethod=ignore
org.eclipse.jdt.core.compiler.problem.noEffectAssignment=warning
org.eclipse.jdt.core.compiler.problem.noImplicitStringConversion=warning
org.eclipse.jdt.core.compiler.problem.nonExternalizedStringLiteral=ignore
org.eclipse.jdt.core.compiler.problem.nonnullParameterAnnotationDropped=warning
org.eclipse.jdt.core.compiler.problem.nonnullTypeVariableFromLegacyInvocation=warning
org.eclipse.jdt.core.compiler.problem.nullAnnotationInferenceConflict=error
org.eclipse.jdt.core.compiler.problem.nullReference=warning
org.eclipse.jdt.core.compiler.problem.nullSpecViolation=error
org.eclipse.jdt.core.compiler.problem.nullUncheckedConversion=warning
org.eclipse.jdt.core.compiler.problem.overridingPackageDefaultMethod=warning
org.eclipse.jdt.core.compiler.problem.parameterAssignment=ignore
org.eclipse.jdt.core.compiler.problem.pessimisticNullAnalysisForFreeTypeVariables=warning
org.eclipse.jdt.core.compiler.problem.possibleAccidentalBooleanAssignment=ignore
org.eclipse.jdt.core.compiler.problem.potentialNullReference=ignore
org.eclipse.jdt.core.compiler.problem.potentiallyUnclosedCloseable=ignore
org.eclipse.jdt.core.compiler.problem.rawTypeReference=warning
org.eclipse.jdt.core.compiler.problem.redundantNullAnnotation=warning
org.eclipse.jdt.core.compiler.problem.redundantNullCheck=ignore
org.eclipse.jdt.core.compiler.problem.redundantSpecificationOfTypeArguments=ignore
org.eclipse.jdt.core.compiler.problem.redundantSuperinterface=ignore
org.eclipse.jdt.core.compiler.problem.reportMethodCanBePotentiallyStatic=ignore
org.eclipse.jdt.core.compiler.problem.reportMethodCanBeStatic=ignore
org.eclipse.jdt.core.compiler.problem.reportPreviewFeatures=warning
org.eclipse.jdt.core.compiler.problem.specialParameterHidingField=disabled
org.eclipse.jdt.core.compiler.problem.staticAccessReceiver=warning
org.eclipse.jdt.core.compiler.problem.suppressOptionalErrors=disabled
org.eclipse.jdt.core.compiler.problem.suppressWarnings=enabled
org.eclipse.jdt.core.compiler.problem.syntacticNullAnalysisForFields=disabled
org.eclipse.jdt.core.compiler.problem.syntheticAccessEmulation=ignore
org.eclipse.jdt.core.compiler.problem.terminalDeprecation=warning
org.eclipse.jdt.core.compiler.problem.typeParameterHiding=warning
org.eclipse.jdt.core.compiler.problem.unavoidableGenericTypeProblems=enabled
org.eclipse.jdt.core.compiler.problem.uncheckedTypeOperation=warning
org.eclipse.jdt.core.compiler.problem.unclosedCloseable=warning
org.eclipse.jdt.core.compiler.problem.undocumentedEmptyBlock=ignore
org.eclipse.jdt.core.compiler.problem.unhandledWarningToken=warning
org.eclipse.jdt.core.compiler.problem.unlikelyCollectionMethodArgumentType=warning
org.eclipse.jdt.core.compiler.problem.unlikelyCollectionMethodArgumentTypeStrict=disabled
org.eclipse.jdt.core.compiler.problem.unlikelyEqualsArgumentType=info
org.eclipse.jdt.core.compiler.problem.unnecessaryElse=ignore
org.eclipse.jdt.core.compiler.problem.unnecessaryTypeCheck=ignore
org.eclipse.jdt.core.compiler.problem.unqualifiedFieldAccess=ignore
org.eclipse.jdt.core.compiler.problem.unstableAutoModuleName=warning
org.eclipse.jdt.core.compiler.problem.unusedDeclaredThrownException=ignore
org.eclipse.jdt.core.compiler.problem.unusedDeclaredThrownExceptionExemptExceptionAndThrowable=enabled
org.eclipse.jdt.core.compiler.problem.unusedDeclaredThrownExceptionIncludeDocCommentReference=enabled
org.eclipse.jdt.core.compiler.problem.unusedDeclaredThrownExceptionWhenOverriding=disabled
org.eclipse.jdt.core.compiler.problem.unusedExceptionParameter=ignore
org.eclipse.jdt.core.compiler.problem.unusedImport=warning
org.eclipse.jdt.core.compiler.problem.unusedLabel=warning
org.eclipse.jdt.core.compiler.problem.unusedLocal=warning
org.eclipse.jdt.core.compiler.problem.unusedObjectAllocation=ignore
org.eclipse.jdt.core.compiler.problem.unusedParameter=ignore
org.eclipse.jdt.core.compiler.problem.unusedParameterIncludeDocCommentReference=enabled
org.eclipse.jdt.core.compiler.problem.unusedParameterWhenImplementingAbstract=disabled
org.eclipse.jdt.core.compiler.problem.unusedParameterWhenOverridingConcrete=disabled
org.eclipse.jdt.core.compiler.problem.unusedPrivateMember=warning
org.eclipse.jdt.core.compiler.problem.unusedTypeParameter=ignore
org.eclipse.jdt.core.compiler.problem.unusedWarningToken=warning
org.eclipse.jdt.core.compiler.problem.varargsArgumentNeedCast=warning
org.eclipse.jdt.core.compiler.release=disabled
org.eclipse.jdt.core.compiler.source=11

View File

@ -0,0 +1,4 @@
activeProfiles=
eclipse.preferences.version=1
resolveWorkspaceProjects=true
version=1

BIN
bin/Main.class Normal file

Binary file not shown.

View File

@ -0,0 +1,69 @@
<?xml version="1.0" encoding="UTF-8"?>
<project xmlns="http://maven.apache.org/POM/4.0.0" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/maven-v4_0_0.xsd">
<modelVersion>4.0.0</modelVersion>
<groupId>OFMCGUI</groupId>
<artifactId>OFMCGUI</artifactId>
<version>1.2</version>
<build>
<sourceDirectory>src</sourceDirectory>
<plugins>
<plugin>
<artifactId>maven-compiler-plugin</artifactId>
<version>3.8.0</version>
<configuration>
<source>11</source>
<target>11</target>
</configuration>
</plugin>
<plugin>
<groupId>org.codehaus.mojo</groupId>
<artifactId>exec-maven-plugin</artifactId>
<version>1.6.0</version>
<executions>
<execution>
<goals>
<goal>java</goal>
</goals>
</execution>
</executions>
<configuration>
<mainClass>Pack.Main</mainClass>
</configuration>
</plugin>
<plugin>
<artifactId>maven-shade-plugin</artifactId>
<version>3.0.0</version>
<executions>
<execution>
<phase>package</phase>
<goals>
<goal>shade</goal>
</goals>
<configuration>
<transformers>
<transformer>
<mainClass>Pack.Main</mainClass>
</transformer>
</transformers>
</configuration>
</execution>
</executions>
</plugin>
</plugins>
</build>
<repositories>
<repository>
<id>javafx</id>
<url>http://nexus.gluonhq.com/nexus/content/repositories/releases/</url>
</repository>
<repository>
<id>javafxml</id>
<url>https://nexus.gluonhq.com/nexus/content/repositories/releases/org/openjfx/javafx.fxml/</url>
</repository>
</repositories>
<properties>
<java.version>11</java.version>
<project.build.sourceEncoding>UTF-8</project.build.sourceEncoding>
</properties>
</project>

106
pom.xml Normal file
View File

@ -0,0 +1,106 @@
<project xmlns="http://maven.apache.org/POM/4.0.0"
xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/xsd/maven-4.0.0.xsd">
<modelVersion>4.0.0</modelVersion>
<groupId>OFMCGUI</groupId>
<artifactId>OFMCGUI</artifactId>
<version>1.2</version>
<properties>
<project.build.sourceEncoding>UTF-8</project.build.sourceEncoding>
<java.version>11</java.version>
</properties>
<repositories>
<repository>
<id> javafx </id>
<url>http://nexus.gluonhq.com/nexus/content/repositories/releases/</url>
</repository>
<repository>
<id> javafxml </id>
<url>https://nexus.gluonhq.com/nexus/content/repositories/releases/org/openjfx/javafx.fxml/</url>
</repository>
</repositories>
<build>
<sourceDirectory>src</sourceDirectory>
<plugins>
<plugin>
<groupId>org.apache.maven.plugins</groupId>
<artifactId>maven-compiler-plugin</artifactId>
<version>3.8.0</version>
<configuration>
<source>11</source>
<target>11</target>
</configuration>
</plugin>
<plugin>
<groupId>org.codehaus.mojo</groupId>
<artifactId>exec-maven-plugin</artifactId>
<version>1.6.0</version>
<executions>
<execution>
<goals>
<goal>java</goal>
</goals>
</execution>
</executions>
<configuration>
<mainClass>Pack.Main</mainClass>
</configuration>
</plugin>
<plugin>
<groupId>org.apache.maven.plugins</groupId>
<artifactId>maven-shade-plugin</artifactId>
<version>3.0.0</version>
<executions>
<execution>
<phase>package</phase>
<goals>
<goal>shade</goal>
</goals>
<configuration>
<transformers>
<transformer
implementation="org.apache.maven.plugins.shade.resource.ManifestResourceTransformer">
<mainClass>Pack.Main</mainClass>
</transformer>
</transformers>
</configuration>
</execution>
</executions>
</plugin>
</plugins>
</build>
<dependencies>
<dependency>
<groupId>org.openjfx</groupId>
<artifactId>javafx-controls</artifactId>
<version>11.0.1</version>
</dependency>
<dependency>
<groupId>org.openjfx</groupId>
<artifactId>javafx-media</artifactId>
<version>11.0.1</version>
</dependency>
<dependency>
<groupId>org.openjfx</groupId>
<artifactId>javafx-graphics</artifactId>
<version>11.0.1</version>
</dependency>
<dependency>
<groupId>org.openjfx</groupId>
<artifactId>javafx-fxml</artifactId>
<version>11.0.1</version>
</dependency>
<dependency>
<groupId>org.fxmisc.richtext</groupId>
<artifactId>richtextfx</artifactId>
<version>0.9.3</version>
</dependency>
<dependency>
<groupId>org.antlr</groupId>
<artifactId>antlr4-runtime</artifactId>
<version>4.7.1</version>
</dependency>
</dependencies>
</project>

View File

@ -0,0 +1,415 @@
/*
* BSD License
*
* Open Source Fixedpoint Model-Checker Graphical User Interface version 2019
*
* (C) Copyright Úlfur Jóhann Edvardsson 2019
* (C) Copyright Veronica Julie Lodskov Hoffmann 2019
*
* All Rights Reserved.
*
*/
package Controller;
import Model.AnalyseProtocol;
import Model.Config;
import Model.TheParser;
import Model.Tracer;
import javafx.fxml.FXML;
import javafx.fxml.FXMLLoader;
import javafx.fxml.Initializable;
import javafx.scene.Node;
import javafx.scene.control.*;
import javafx.scene.layout.*;
import javafx.scene.text.TextFlow;
import javafx.stage.FileChooser;
import org.fxmisc.richtext.CodeArea;
import java.io.BufferedReader;
import java.io.File;
import java.io.IOException;
import java.io.PrintWriter;
import java.net.URL;
import java.nio.file.Files;
import java.nio.file.Paths;
import java.util.ArrayList;
import java.util.List;
import java.util.ResourceBundle;
import java.util.stream.Collectors;
public class Controller implements Initializable{
private File file;
private List<String> list;
private AnalyseProtocol ap;
private Tracer tracer;
private Config config;
private TheParser parser;
private String protocol;
private SimpleTab simpleProtocol, simpleAttack;
private DiagramTab protocolDiagram, attackDiagram;
private Highlighting highlighting;
private TraceTab traceTab;
private String oldText;
private CodeArea protocolCodeArea;
@FXML
Button traceBtn, analyseBtn;
@FXML
SplitPane splitPane;
@FXML
BorderPane applicationPane;
@FXML
TabPane attackTabPane;
@FXML
Tab protocolEditorTab, simplifiedTab, simplifiedAttackTab, protocolDiagramTab, attackDiagramTab;
@FXML private TextArea textRight;
@FXML private Label statusBar;
@FXML
ToggleButton toggleThemeBtn;
@Override
public void initialize(URL url, ResourceBundle resourceBundle) {
// Load content for all tabs
try {
loadProtocolEditorTab();
loadDiagramTab(true);
loadDiagramTab(false);
loadSimpleTab(true);
loadSimpleTab(false);
} catch (IOException e) {
e.printStackTrace();
}
disableTrace();
disableAnalyse();
// Initialize variables
this.protocol = "";
this.config = new Config();
this.tracer = new Tracer(null);
this.list = new ArrayList<>();
ap = new AnalyseProtocol();
oldText = "";
// Update max width for simple view when moving divider
splitPane.getDividers().get(0).positionProperty().addListener(event->{
updateMaxWidth(simpleProtocol.getTextFlow());
updateMaxWidth(simpleAttack.getTextFlow());
});
}
// Disable trace button if protocol editor is empty
void disableTrace() {
traceBtn.setDisable(protocolCodeArea.getText().trim().isEmpty());
}
// Disable analysis if protocol editor is empty
void disableAnalyse() {
analyseBtn.setDisable(protocolCodeArea.getText().trim().isEmpty());
}
// Update max width of text flow
private void updateMaxWidth(TextFlow simpleView) {
for (Node node : simpleView.getChildren()) {
if (node instanceof Label) {
((Label)node).setMaxWidth(simpleView.getWidth());
}
}
}
// Set the text in the protocol editor
private void setProtocolCodeArea(String text) {
if (!text.equals(protocolCodeArea.getText())) {
protocolCodeArea.replaceText(0, protocolCodeArea.getText().length(), text);
}
}
// Analyze the protocol
@FXML
protected void handleAnalyseButtonAction() throws IOException, InterruptedException {
// Check if the tabs has changed
tabChange();
// Set configurations
if(!config.locationCheck()) {
config.locateOFMC();
}
ap.setConfigs(config.getConfigs());
if(ap.getSyntaxError()) {
statusBar.setText("Syntax Error!");
statusBar.setId("redID");
// create some error ?
// return;
}
ap.run(protocolCodeArea.getText());
if (ap.getSyntaxError()) {
textRight.setText(ap.geterrormsg());
return;
}
textRight.setText(ap.getAnalysis());
// Initialize tabs in attack trace
attackDiagram.initData(this, false);
simpleAttack.initData(this, false);
// Apply highlighting
try{
highlighting = new Highlighting(simpleAttack, attackDiagram, simpleProtocol, protocolDiagram);
} catch (Exception ignore){}
if(ap.getAttackFound()) {
statusBar.setText("Attack Found!");
statusBar.setId("orangeID");
} else {
statusBar.setText("No Attack Found!");
statusBar.setId("greenID");
}
}
// Load a protocol to the protocol editor
@FXML protected void handleBrowseButtonAction() throws IOException {
ap = new AnalyseProtocol();
this.parser = new TheParser("p");
FileChooser chooser = new FileChooser();
chooser.getExtensionFilters().add(new FileChooser.ExtensionFilter( "AnB Files", "*.AnB"));
file = chooser.showOpenDialog(null);
this.list = new ArrayList<>();
if (file != null) {
try (BufferedReader br = Files.newBufferedReader(Paths.get(file.getPath()))) {
list = br.lines().collect(Collectors.toList());
} catch (IOException e) {
return;
}
}
protocol = "";
for (String line : list) {
protocol = String.format("%s%s\n", protocol, line);
}
if(protocol.equals("")) {
return;
}
ap.modifyProtocol(protocol);
if(ap.getSyntaxError()) {
statusBar.setText("Syntax Error!");
statusBar.setId("redID");
} else {
statusBar.setText("Syntax OK");
statusBar.setId("greenID");
}
setProtocolCodeArea(protocol);
tabChange();
}
// Trace through a protocol
@FXML protected void handleTraceButtonAction() throws IOException {
this.parser = new TheParser("p");
statusBar.setText("Tracing");
this.tracer = new Tracer(parser);
if(!config.locationCheck()) {
config.locateOFMC();
if (!config.locationCheck()) return;
}
tracer.setConfigs(config.getConfigs());
tracer.modifyProtocol(protocolCodeArea.getText());
if(parser.syntaxError) {
statusBar.setText("Syntax Error!");
statusBar.setId("redID");
return;
}
tracer.runTrace();
createTracerTab();
}
// Save the protocol to a file
@FXML protected void handleSaveButtonAction() {
FileChooser chooser = new FileChooser();
chooser.getExtensionFilters().add(new FileChooser.ExtensionFilter( "AnB Files", "*.AnB"));
try{
file = chooser.showSaveDialog(null);
} catch (Exception e) {
return;
}
if (file != null) {
saveTextToFile(protocolCodeArea.getText(), file);
protocol = protocolCodeArea.getText();
}
}
@FXML protected void handleConfigButtonAction() {
config.sConfig();
}
private void saveTextToFile(String content, File file) {
try {
PrintWriter writer;
writer = new PrintWriter(file);
writer.println(content);
writer.close();
} catch (IOException ignored) {
}
}
// Load FXML
private FXMLLoader load(String fxmlURL, Tab tab) throws IOException {
FXMLLoader loader = new FXMLLoader(getClass().getResource(fxmlURL));
tab.setContent(loader.load());
return loader;
}
private void loadProtocolEditorTab() throws IOException {
FXMLLoader loader = load("/View/protocolEditor.fxml", protocolEditorTab);
ProtocolEditor protocolEditor = loader.getController();
protocolEditor.initData(this);
protocolCodeArea = protocolEditor.getProtocolCodeArea();
}
private void loadDiagramTab(boolean isProtocol) throws IOException {
if (isProtocol) {
FXMLLoader loader = load("/View/diagramTab.fxml", protocolDiagramTab);
protocolDiagram = loader.getController();
} else {
FXMLLoader loader = load("/View/diagramTab.fxml", attackDiagramTab);
attackDiagram = loader.getController();
attackDiagram.initData(this, false);
}
}
private void loadSimpleTab(boolean isProtocol) throws IOException {
if (isProtocol) {
FXMLLoader loader = load("/View/simpleTab.fxml", simplifiedTab);
simpleProtocol = loader.getController();
} else {
FXMLLoader loader = load("/View/simpleTab.fxml", simplifiedAttackTab);
simpleAttack = loader.getController();
simpleAttack.initData(this, false);
}
}
private void createTracerTab() throws IOException {
Tab newTab = new Tab("Tracer");
FXMLLoader loader = new FXMLLoader(getClass().getResource("/View/traceTab.fxml"));
newTab.setContent(loader.load());
attackTabPane.getTabs().add(newTab);
traceTab = loader.getController();
traceTab.initData(simpleProtocol, protocolDiagram, tracer);
attackTabPane.getSelectionModel().select(newTab);
}
// The dialog that pops up on exit if theres unsaved work
public void promptSaveDialog() {
if (this.protocol.equals(protocolCodeArea.getText())) {
javafx.application.Platform.exit();
System.exit(0);
}
Alert alert = new Alert(Alert.AlertType.NONE);
alert.setTitle("Current Protocol has been modified");
alert.setContentText("Do you want to save the protocol?");
ButtonType yesButton = new ButtonType("Yes", ButtonBar.ButtonData.YES);
ButtonType noButton = new ButtonType("No", ButtonBar.ButtonData.NO);
ButtonType cancelButton = new ButtonType("Cancel", ButtonBar.ButtonData.CANCEL_CLOSE);
alert.getButtonTypes().setAll(yesButton, noButton, cancelButton);
alert.showAndWait().ifPresent(type -> {
if (type.toString().contains("Yes")) {
handleSaveButtonAction();
} else if (type.toString().contains("No")) {
javafx.application.Platform.exit();
System.exit(0);
} else {
return;
}
});
}
// Update the tabs
private void updateTabs() {
ap = new AnalyseProtocol();
ap.modifyProtocol(protocolCodeArea.getText());
if (ap.getSyntaxError()) {
statusBar.setText("Syntax Error!");
statusBar.setId("redID");
// create some error ?
} else {
statusBar.setText("Syntax OK!");
statusBar.setId("greenID");
protocolDiagram.initData(this, true);
simpleProtocol.initData(this, true);
}
if (attackDiagram != null) {
attackDiagram.clearDiagram();
attackDiagram.nothingToShow();
simpleAttack.clearSimple();
simpleAttack.nothingToShow();
}
}
// When protocol text has changed then update tabs
public void tabChange() throws IOException {
if (!oldText.equals(protocolCodeArea.getText())) {
updateTabs();
oldText = protocolCodeArea.getText();
}
}
// Change theme
public void toggleTheme() {
if (toggleThemeBtn.isSelected()) {
setTheme("/View/lightTheme.css", "Dark Theme");
} else {
setTheme("/View/darkTheme.css", "Light Theme");
}
}
void setTheme(String css, String newText) {
applicationPane.getStylesheets().clear();
applicationPane.getStylesheets().add(getClass().getResource(css).toExternalForm());
toggleThemeBtn.setText(newText);
}
void updateHighlight() {
// Update the highlighting
try {
highlighting.updateHighlighting();
} catch (Exception ignored) {}
try {
traceTab.updateHighlighting();
} catch (Exception ignored) {}
}
AnalyseProtocol getAp() {
return ap;
}
}

View File

@ -0,0 +1,267 @@
/*
* BSD License
*
* Open Source Fixedpoint Model-Checker Graphical User Interface version 2019
*
* (C) Copyright Úlfur Jóhann Edvardsson 2019
* (C) Copyright Veronica Julie Lodskov Hoffmann 2019
*
* All Rights Reserved.
*
*/
package Controller;
import javafx.fxml.FXML;
import javafx.scene.control.CheckBox;
import javafx.scene.control.Label;
import javafx.scene.control.Tooltip;
import javafx.scene.image.Image;
import javafx.scene.image.ImageView;
import javafx.scene.layout.*;
import Model.Parser.AST;
import java.util.ArrayList;
import java.util.Arrays;
import java.util.List;
public class DiagramTab {
private HBox diagramLines;
private VBox diagramActionsBox;
private List<String> agents;
private List<AST> actions;
private double PREF_WIDTH = 150;
private int agentCounter;
private int actionCounter;
private boolean initialized;
private List<VBox> steps;
private Boolean[] diagramFilterValues = {true, true};
private Controller controller;
@FXML
private HBox diagramFilter, diagramAgents;
@FXML
private StackPane diagramActions;
void initData(Controller controller, boolean isProtocol) {
this.controller = controller;
steps = new ArrayList<>();
agents = new ArrayList<>();
actions = new ArrayList<>();
diagramLines = (HBox) diagramActions.getChildren().get(0);
diagramLines.setId("diagramHLine");
diagramActionsBox = (VBox) diagramActions.getChildren().get(1);
diagramActionsBox.setId("diagramActionBox");
initialized = false;
agentCounter = 0;
actionCounter = 0;
clearDiagram();
// Get the agents and actions
if (isProtocol) {
agents = Arrays.asList(controller.getAp().getAgents().split("[,;]"));
actions = controller.getAp().getActions();
} else {
try {
getAttackTraceAgents(controller);
} catch (Exception e) {
nothingToShow();
return;
}
}
initDiagram();
}
void clearDiagram() {
diagramAgents.getChildren().clear();
diagramLines.getChildren().clear();
diagramActionsBox.getChildren().clear();
}
void nothingToShow() {
Label label = new Label("Nothing to show");
label.setId("step");
diagramAgents.getChildren().add(label);
}
private void getAttackTraceAgents(Controller controller) {
actions = controller.getAp().getSimpleAnalysis();
if (actions.isEmpty()) {
nothingToShow();
}
for (AST action : actions) {
String[] split = action.toString().replaceAll(" ", "").split("->|:");
if (!agents.contains(split[0])) {
agents.add(split[0]);
}
if (!agents.contains(split[1])) {
agents.add(split[1]);
}
}
}
private void initDiagram() {
if (!initialized) {
diagramAgents.setId("diagramActionBox");
// Add labels for the agents
for (String agent : agents) {
addAgent(agent);
}
// Add extra space at the end
addAgent(null);
initialized = true;
} else {
actionCounter = 0;
diagramActionsBox.getChildren().clear();
steps.clear();
}
setDiagramFilter();
// Add actions between the agents
for (AST action : actions) {
addAction(Arrays.asList(action.toString().replaceAll(" ", "").split("->|:")));
}
}
private void setDiagramFilter() {
for (int i = 0; i < diagramFilter.getChildren().size(); i++) {
CheckBox checkBox = (CheckBox) diagramFilter.getChildren().get(i);
diagramFilterValues[i] = checkBox.isSelected();
}
}
private void addAgent(String agent) {
Label agentLabel = new Label();
agentLabel.setId("diagramLabel");
// Add the agent to the diagram
if (agent != null) {
agentLabel.setText(agent);
VBox iVBox = new VBox(new Label());
iVBox.setId("diagramLine");
diagramLines.getChildren().add(agentCounter, iVBox);
agentCounter++;
}
diagramAgents.getChildren().add(agentLabel);
}
private void addAction(List<String> action) {
// Get the names of the interacting agents
int index1 = getIndex(action, 0);
int index2 = getIndex(action, 1);
// Get the min and max index values
int minIndex = Math.min(index1,index2);
// Get length for the action label
int length = Math.abs(index1-index2);
HBox diagramAction = new HBox();
diagramAction.setId("diagramActionBox");
if (minIndex > 0) {
addSpace(diagramAction, minIndex);
}
// Add the action to the diagram
VBox actionBox = new VBox();
actionBox.setId("diagramActionBox");
actionBox.setMaxWidth(length*PREF_WIDTH-2);
if (diagramFilterValues[0]) {
actionBox.getChildren().add(makeActionLabel(action, "Step " + ++actionCounter));
}
if (diagramFilterValues[1]) {
actionBox.getChildren().add(makeActionLabel(action, action.get(2).replaceAll("step" + "\\d" + ",","")));
}
actionBox.getChildren().add(getArrow(action, length));
steps.add(actionBox);
diagramAction.getChildren().add(actionBox);
addSpace(diagramAction, (agentCounter-length-minIndex));
diagramActionsBox.getChildren().add(diagramAction);
}
private Label makeActionLabel(List<String> action, String text) {
Label actionLabel = new Label(text);
actionLabel.setId("diagramAction");
VBox.setVgrow(actionLabel,Priority.ALWAYS);
actionLabel.setTooltip(new Tooltip(action.get(2).replaceAll("step" + "\\d" + ",","")));
return actionLabel;
}
private void addSpace(HBox box, int length) {
for (int i = 0; i <length; i++) {
Label space = new Label();
space.setId("diagramLabel");
box.getChildren().add(space);
}
}
private int getIndex(List<String> action, int index) {
return agents.indexOf(action.get(index));
}
private HBox getArrow(List<String> action, int length) {
HBox completeArrow = new HBox();
completeArrow.setSpacing(2);
// Get arrow lines
for (int i = 1; i < length; i++) {
ImageView line = new ImageView(new Image(getClass().getResourceAsStream("/Resources/arrow_line_light.png")));
line.setFitWidth(PREF_WIDTH-2);
completeArrow.getChildren().add(line);
}
ImageView arrow = new ImageView(new Image(getClass().getResourceAsStream(
getIndex(action,0) < getIndex(action, 1)
? "/Resources/arrow_right_light.png"
: "/Resources/arrow_left_light.png"
)));
arrow.setFitWidth(PREF_WIDTH-2);
// Check the direction of the arrow
if (getIndex(action,0) < getIndex(action, 1)) {
arrow.setFitWidth(PREF_WIDTH-2);
completeArrow.getChildren().add(arrow);
} else {
arrow.setFitWidth(PREF_WIDTH-2);
completeArrow.getChildren().add(0,arrow);
}
return completeArrow;
}
List<VBox> getSteps() {
return steps;
}
@FXML
private void applyFilter() {
// Apply filter to diagram area
initDiagram();
controller.updateHighlight();
}
List<AST> getActions() {
return actions;
}
}

View File

@ -0,0 +1,256 @@
/*
* BSD License
*
* Open Source Fixedpoint Model-Checker Graphical User Interface version 2019
*
* (C) Copyright Úlfur Jóhann Edvardsson 2019
* (C) Copyright Veronica Julie Lodskov Hoffmann 2019
*
* All Rights Reserved.
*
*/
package Controller;
import javafx.scene.Node;
import javafx.scene.control.Button;
import javafx.scene.control.Label;
import javafx.scene.layout.VBox;
import Model.Parser.AST;
import Model.Parser.Option;
import java.util.ArrayList;
import java.util.List;
import java.util.regex.Matcher;
import java.util.regex.Pattern;
class Highlighting {
private SimpleTab simpleBase;
private DiagramTab diagramBase;
private SimpleTab simpleLink;
private DiagramTab diagramLink;
private TraceTab traceTab;
private List<Label> simpleConnection;
private List<VBox> diagramConnection;
private List<List<Label>> traceSimpleConnection;
private List<List<VBox>> traceDiagramConnection;
private List<Label> simpleSteps;
private List<VBox> diagramSteps;
private List<Button> traceSteps;
private List<AST> actions;
private List<Option> traceActions;
Highlighting(SimpleTab simpleBase, DiagramTab diagramBase, SimpleTab simpleLink, DiagramTab diagramLink) {
// Initialisation of variables
this.simpleBase = simpleBase;
this.diagramBase = diagramBase;
this.simpleLink = simpleLink;
this.diagramLink = diagramLink;
simpleConnection = new ArrayList<>();
diagramConnection = new ArrayList<>();
simpleSteps = simpleBase.getSteps();
diagramSteps = diagramBase.getSteps();
actions = simpleBase.getActions();
// Create the highlighting
initHighlighting();
}
Highlighting(TraceTab traceTab, SimpleTab simpleLink, DiagramTab diagramLink) {
// Initializing the variables
this.traceTab = traceTab;
this.simpleLink = simpleLink;
this.diagramLink = diagramLink;
traceSteps = traceTab.getTraceButtons();
traceSimpleConnection = new ArrayList<>();
traceDiagramConnection = new ArrayList<>();
traceActions = traceTab.getTracer().getOptions();
}
void updateHighlighting() {
// Clearing the area
simpleConnection.clear();
diagramConnection.clear();
// Update
initHighlighting();
}
private void initHighlighting() {
// Update hovering
for (int i = 0; i < actions.size(); i++) {
addStepLinks(actions.get(i).toString(), false);
hoveringHighlight(simpleSteps.get(i), diagramSteps.get(i), simpleBase.isProtocol());
}
for (int i = 0; i < simpleConnection.size(); i++) {
hoveringHighlight(simpleConnection.get(i), diagramConnection.get(i), simpleLink.isProtocol());
}
}
private void addStepLinks(String action, boolean isTrace) {
// Initialize pattern and mather for getting step links
Pattern pattern = Pattern.compile("step(\\d),");
Matcher matcher = pattern.matcher(action);
List<Label> labels = new ArrayList<>();
List<VBox> vBoxes = new ArrayList<>();
// Find the step to link
while (matcher.find()) {
int step = Integer.parseInt(matcher.group(1));
// Get label for the linked step and add it to link connections
Label label = simpleLink.getSteps().get(step-1);
VBox vBox = diagramLink.getSteps().get(step-1);
if (isTrace) {
labels.add(label);
vBoxes.add(vBox);
} else {
simpleConnection.add(label);
diagramConnection.add(vBox);
}
}
if (isTrace) {
traceSimpleConnection.add(labels);
traceDiagramConnection.add(vBoxes);
}
}
private void hoveringHighlight(Label label, VBox vBox, boolean isProtocol) {
// Register start of hovering
label.setOnMouseEntered(mouseEvent -> {
label.setId("hover-highlight");
vBox.setId("hover-highlight");
linkHighlighting(label, vBox, isProtocol);
});
// Register end of hovering
label.setOnMouseExited(mouseEvent -> {
label.setId("action");
vBox.setId("diagramActionBox");
linkHighlighting(label, vBox, isProtocol);
});
// Register start of hovering
vBox.setOnMouseEntered(mouseEvent -> {
label.setId("hover-highlight");
vBox.setId("hover-highlight");
linkHighlighting(label, vBox, isProtocol);
});
// Register end of hovering
vBox.setOnMouseExited(mouseEvent -> {
label.setId("action");
vBox.setId("diagramActionBox");
linkHighlighting(label, vBox, isProtocol);
});
}
private void linkHighlighting(Label label, VBox vBox, boolean isProtocol) {
// Check if protocol and other tab is loaded
if (isProtocol) {
// Search for current step in the step connection list
for (int i = 0; i < simpleConnection.size(); i++) {
// If the step is found then add/remove highlighting
if (simpleConnection.get(i).equals(label)) {
simpleBase.getSteps().get(i).setId(label.getId());
diagramBase.getSteps().get(i).setId(vBox.getId());
}
}
}
// Else if it is not the protocol then just add/remove the highlighting
else {
if (simpleSteps.indexOf(label)< simpleConnection.size()) {
simpleConnection.get(simpleSteps.indexOf(label)).setId(label.getId());
diagramConnection.get(diagramSteps.indexOf(vBox)).setId(vBox.getId());
}
}
}
void updateTracerLink() {
// Clear the connections
traceSimpleConnection.clear();
traceDiagramConnection.clear();
traceActions = traceTab.getTracer().getOptions();
// update the hovering
for (int i = 0; i < traceActions.size(); i++) {
addStepLinks(traceActions.get(i).toString(), true);
traceHoveringHighlight(traceSteps.get(i),traceSimpleConnection.get(i), traceDiagramConnection.get(i));
}
}
private void traceHoveringHighlight(Node node, List<Label> labels, List<VBox> vBoxes) {
// Register start of hovering
node.setOnMouseEntered(mouseEvent -> {
for (int i = 0; i < labels.size(); i++) {
linkTraceHighlighting(labels.get(i), vBoxes.get(i), true);
}
});
// Register end of hovering
node.setOnMouseExited(mouseEvent -> {
for (int i = 0; i < labels.size(); i++) {
linkTraceHighlighting(labels.get(i), vBoxes.get(i), false);
}
});
// Hovering over the connections
for (Label label : labels) {
label.setOnMouseEntered(e -> {
label.setId("hover-highlight");
for (int i = 0; i<traceSimpleConnection.size(); i++) {
if (traceSimpleConnection.get(i).contains(label)) {
traceSteps.get(i).setId("traceHover");
}
}
});
label.setOnMouseExited(e-> {
label.setId("action");
for (int i = 0; i<traceSimpleConnection.size(); i++) {
if (traceSimpleConnection.get(i).contains(label)) {
traceSteps.get(i).setId("traceOptionButton");
}
}
});
}
for (VBox vBox : vBoxes) {
vBox.setOnMouseEntered(e-> {
vBox.setId("hover-highlight");
for (int i = 0; i<traceDiagramConnection.size(); i++) {
if (traceDiagramConnection.get(i).contains(vBox)) {
traceSteps.get(i).setId("traceHover");
}
}
});
vBox.setOnMouseExited(e-> {
vBox.setId("diagramActionBox");
for (int i = 0; i<traceDiagramConnection.size(); i++) {
if (traceDiagramConnection.get(i).contains(vBox)) {
traceSteps.get(i).setId("traceOptionButton");
}
}
});
}
}
private void linkTraceHighlighting(Label label, VBox vBox, boolean isHovering) {
if (isHovering) {
label.setId("hover-highlight");
vBox.setId("hover-highlight");
} else {
label.setId("action");
vBox.setId("diagramActionBox");
}
}
}

View File

@ -0,0 +1,212 @@
/*
* BSD License
*
* Open Source Fixedpoint Model-Checker Graphical User Interface version 2019
*
* (C) Copyright Úlfur Jóhann Edvardsson 2019
* (C) Copyright Veronica Julie Lodskov Hoffmann 2019
*
* All Rights Reserved.
*
*/
package Controller;
import javafx.fxml.FXML;
import org.fxmisc.richtext.*;
import org.fxmisc.richtext.model.PlainTextChange;
import org.fxmisc.richtext.model.StyleSpans;
import org.fxmisc.richtext.model.StyleSpansBuilder;
import org.reactfx.AwaitingEventStream;
import java.time.Duration;
import java.util.Collection;
import java.util.Collections;
import java.util.List;
import java.util.regex.Matcher;
import java.util.regex.Pattern;
public class ProtocolEditor {
private static Pattern PATTERN;
@FXML
private CodeArea protocolCodeArea;
// Defining keywords for syntax
private static final String[] KEYWORDS = new String[] {
"Protocol", "Types", "Knowledge", "Actions", "Goals"
};
private static final String[] TYPES = new String[] {
"Agent", "Number", "Function", "Symmetric_key"
};
private static final String[] BUILDIN_FUNCTIONS = new String[] {
"sk", "exp", "inv", "pk"
};
private static final String[] OTHER = new String[] {
"weakly", "authenticates", "where", "on", "secret", "between"
};
private static String[] AGENTS = new String[0];
private static String[] NUMBERS = new String[0];
private static String[] FUNCTIONS = new String[0];
private static String[] SYMMETRIC_KEY = new String[0];
// Defining patterns for syntax
private static final String KEYWORD_PATTERN = createPattern(KEYWORDS);
private static final String TYPES_PATTERN = createPattern(TYPES);
private static final String BUILDIN_FUNCTIONS_PATTERN = createPattern(BUILDIN_FUNCTIONS);
private static final String OTHER_PATTERN = createPattern(OTHER);
private static String AGENTS_PATTERN;
private static String NUMBERS_PATTERN;
private static String FUNCTIONS_PATTERN;
private static String SYMMETRIC_KEY_PATTERN;
private static final String COMMENT_PATTERN = "#[^\\n]*";
// Defining pattern for adding new agents
private static final Pattern MATCHING_AGENTS_PATTERN = generateMatchingPattern("Agent");
private static final Pattern MATCHING_NUMBERS_PATTERN = generateMatchingPattern("Number");
private static final Pattern MATCHING_FUNCTIONS_PATTERN = generateMatchingPattern("Function");
private static final Pattern MATCHING_SYMMETRIC_KEY_PATTERN = generateMatchingPattern("Symmetric_key");
void initData(Controller controller) {
// Get line numbering
protocolCodeArea.setParagraphGraphicFactory(LineNumberFactory.get(protocolCodeArea));
// Updates after changes are made
onChange().subscribe(updateTypes -> updateTypes());
onChange().subscribe(highlight -> updateSyntaxHighlighting(protocolCodeArea.getText()));
onChange().subscribe(disableTrace -> controller.disableTrace());
onChange().subscribe(disableAnalyse -> controller.disableAnalyse());
}
// Standard word pattern matching
private static String createPattern(String[] typeToMatch) {
return "\\b(" + String.join("|", typeToMatch) + ")\\b";
}
// Generate matching pattern for types
private static Pattern generateMatchingPattern(String matchingType) {
return Pattern.compile(matchingType + "\\s(\\w+(\\s*,\\s*\\w+)*)");
}
// Redefining patterns
private static void redefinePatterns() {
if (AGENTS.length != 0) {
AGENTS_PATTERN = createPattern(AGENTS);
}
if (NUMBERS.length != 0) {
NUMBERS_PATTERN = createPattern(NUMBERS);
}
if (FUNCTIONS.length != 0) {
FUNCTIONS_PATTERN = createPattern(FUNCTIONS);
}
if (SYMMETRIC_KEY.length != 0) {
SYMMETRIC_KEY_PATTERN = createPattern(SYMMETRIC_KEY);
}
compilePattern();
}
// Setting patterns for syntax
private static void compilePattern() {
PATTERN = Pattern.compile(
"(?<COMMENT>" + COMMENT_PATTERN + ")" +
"|(?<KEYWORD>" + KEYWORD_PATTERN + ")" +
"|(?<TYPES>" + TYPES_PATTERN + ")" +
"|(?<BUILDINFUNCTIONS>" + BUILDIN_FUNCTIONS_PATTERN + ")" +
"|(?<OTHER>" + OTHER_PATTERN + ")" +
"|(?<AGENTS>" + AGENTS_PATTERN + ")" +
"|(?<NUMBERS>" + NUMBERS_PATTERN + ")" +
"|(?<FUNCTIONS>" + FUNCTIONS_PATTERN + ")" +
"|(?<SYMMETRICKEY>" + SYMMETRIC_KEY_PATTERN + ")"
);
}
private void updateSyntaxHighlighting(String text) {
protocolCodeArea.setStyleSpans(0, syntaxHighlighting(text));
}
private AwaitingEventStream<List<PlainTextChange>> onChange() {
return protocolCodeArea.multiPlainChanges().successionEnds(Duration.ofMillis(500));
}
// Update arrays for types and redefine the patterns
private void updateTypes() {
AGENTS = getNewTypes(MATCHING_AGENTS_PATTERN);
NUMBERS = getNewTypes(MATCHING_NUMBERS_PATTERN);
FUNCTIONS = getNewTypes(MATCHING_FUNCTIONS_PATTERN);
SYMMETRIC_KEY = getNewTypes(MATCHING_SYMMETRIC_KEY_PATTERN);
redefinePatterns();
}
// Get types matching the given pattern
private String[] getNewTypes(Pattern matchingPattern) {
Matcher matcher = matchingPattern.matcher(protocolCodeArea.getText());
StringBuilder newPatterns = new StringBuilder();
boolean firstMatch = true;
while (matcher.find()) {
if (!firstMatch) {
newPatterns.append(",");
} else {
firstMatch=false;
}
newPatterns.append(matcher.group(1));
}
if (newPatterns.length() != 0) {
return newPatterns.toString().split(",");
} else {
return new String[0];
}
}
// Generate the syntax highlighting
private static StyleSpans<Collection<String>> syntaxHighlighting(String text) {
Matcher matcher = PATTERN.matcher(text);
int lastKeywordEnd = 0;
StyleSpansBuilder<Collection<String>> spansBuilder = new StyleSpansBuilder<>();
while(matcher.find()) {
String styleClass =
matcher.group("COMMENT") != null ? "comment" :
matcher.group("KEYWORD") != null ? "keyword" :
matcher.group("TYPES") != null ? "types" :
matcher.group("BUILDINFUNCTIONS") != null ? "functions" :
matcher.group("OTHER") != null ? "other" :
matcher.group("AGENTS") != null ? "agents" :
matcher.group("NUMBERS") != null ? "numbers" :
matcher.group("FUNCTIONS") != null ? "functions" :
matcher.group("SYMMETRICKEY") != null ? "symmetric-key" :
null;
assert styleClass != null;
spansBuilder.add(Collections.emptyList(), matcher.start() - lastKeywordEnd);
spansBuilder.add(Collections.singleton(styleClass), matcher.end() - matcher.start());
lastKeywordEnd = matcher.end();
}
spansBuilder.add(Collections.emptyList(),text.length() - lastKeywordEnd);
return spansBuilder.create();
}
public CodeArea getProtocolCodeArea() {
return protocolCodeArea;
}
}

View File

@ -0,0 +1,121 @@
/*
* BSD License
*
* Open Source Fixedpoint Model-Checker Graphical User Interface version 2019
*
* (C) Copyright Úlfur Jóhann Edvardsson 2019
* (C) Copyright Veronica Julie Lodskov Hoffmann 2019
*
* All Rights Reserved.
*
*/
package Controller;
import javafx.fxml.FXML;
import javafx.scene.control.Label;
import javafx.scene.text.Text;
import javafx.scene.text.TextFlow;
import Model.Parser.AST;
import java.util.ArrayList;
import java.util.List;
public class SimpleTab {
private List<AST> actions;
private boolean isProtocol;
private List<Label> steps;
@FXML
private TextFlow textFlow;
void initData(Controller controller, boolean isProtocol) {
clearSimple();
// Get actions
if (isProtocol) {
actions = controller.getAp().getActions();
} else {
try {
actions = controller.getAp().getSimpleAnalysis();
} catch (Exception e) {
nothingToShow();
return;
}
}
if (actions.isEmpty()) nothingToShow();
this.isProtocol = isProtocol;
steps = new ArrayList<>();
// Add steps to the text flow
if (actions != null) {
addSteps();
}
}
void clearSimple() {
textFlow.getChildren().clear();
}
void nothingToShow() {
Label label = new Label("Nothing to show");
label.setId("step");
textFlow.getChildren().add(label);
}
private void addSteps() {
int i = 1;
for (AST action: actions) {
// Add Step to the Text Flow
addProtocolTextFlow("Step " + i++, "step");
Label actionLabel = addProtocolTextFlow(action.toString().replaceAll("step" + "\\d" + ",",""), "action");
// Save the step's action
steps.add(actionLabel);
}
}
private Label addProtocolTextFlow(String string, String id) {
Label label;
if (isProtocol) {
// If protocol add the given string
label = new Label(string);
} else {
// Else remove the step from the string
label = new Label(string.replaceAll("step" + "\\d" + ",",""));
}
// Set layout attributes
label.setId(id);
label.setMaxWidth(textFlow.getWidth());
// Add label to text flow
textFlow.getChildren().addAll(label, new Text("\n"));
return label;
}
List<Label> getSteps() {
return steps;
}
void setActions(List<AST> actions) {
this.actions = actions;
}
List<AST> getActions() {
return actions;
}
boolean isProtocol() {
return isProtocol;
}
TextFlow getTextFlow() {
return textFlow;
}
}

View File

@ -0,0 +1,165 @@
/*
* BSD License
*
* Open Source Fixedpoint Model-Checker Graphical User Interface version 2019
*
* (C) Copyright Úlfur Jóhann Edvardsson 2019
* (C) Copyright Veronica Julie Lodskov Hoffmann 2019
*
* All Rights Reserved.
*
*/
package Controller;
import Model.Tracer;
import javafx.fxml.FXML;
import javafx.scene.control.Button;
import javafx.scene.control.Label;
import javafx.scene.layout.VBox;
import Model.Parser.Option;
import java.util.ArrayList;
import java.util.List;
public class TraceTab {
@FXML
public Button backBtn, forwardBtn;
@FXML
public VBox traceOptions, traceHistory;
private Tracer tracer;
private List<Button> traceButtons;
private List<Integer> tracePath;
private Highlighting highlighting;
private int traceCounter = 0;
void initData(SimpleTab simpleTab, DiagramTab diagramTab, Tracer tracer) {
this.tracer = tracer;
traceButtons = new ArrayList<>();
highlighting = new Highlighting(this, simpleTab, diagramTab);
tracePath = new ArrayList<>();
showTracerOptions();
}
private void showTracerOptions() {
// Clear the trace buttons
if (!traceButtons.isEmpty() || !traceOptions.getChildren().isEmpty()) {
traceButtons.clear();
traceOptions.getChildren().clear();
}
List<Option> options = tracer.getOptions();
// Add the buttons to the view
for (int i = 0 ; i < options.size(); i++) {
Button b = new Button(options.get(i).toString().replaceAll("step\\d,", ""));
b.setId("traceOptionButton");
Label label = new Label("Option " + (i + 1));
label.setId("step");
traceOptions.getChildren().addAll(label, b);
traceButtons.add(b);
traceButtonPressed(b, i);
}
updateHighlighting();
}
void updateHighlighting() {
highlighting.updateTracerLink();
}
// Register button press
private void traceButtonPressed(Button b, int i) {
b.setOnAction(actionEvent -> {
if (!forwardBtn.isDisabled()) {
tracePath.subList(traceCounter, tracePath.size() - 1).clear();
}
tracePath.add(i);
// Chosen tracing action
tracer.addToStepsTaken(i, b.getText());
tracer.runTrace();
traceHistory.getChildren().add(new Label(tracer.getHistory().get(traceCounter)));
traceCounter++;
if (traceCounter > 0) {
backBtn.setDisable(false);
}
forwardBtn.setDisable(true);
generateTracerOptions();
});
}
public void backTrace() {
// Chosen tracing action
tracer.removeStepTaken();
tracer.runTrace();
traceHistory.getChildren().remove(traceHistory.getChildren().size()-1);
traceCounter--;
if (traceCounter > 0) {
backBtn.setDisable(false);
} else {
backBtn.setDisable(true);
}
forwardBtn.setDisable(false);
try {
showTracerOptions();
} catch (Exception ignored) {
}
}
public void forwardTrace() {
int nextOption = tracePath.get(traceCounter);
Button btn = (Button)traceOptions.getChildren().get(nextOption*2 + 1);
// Chosen tracing action
tracer.addToStepsTaken(nextOption, btn.getText());
tracer.runTrace();
traceHistory.getChildren().add(new Label(tracer.getHistory().get(traceCounter)));
traceCounter++;
if (traceCounter == tracePath.size()) {
forwardBtn.setDisable(true);
}
backBtn.setDisable(false);
generateTracerOptions();
}
private void generateTracerOptions() {
try {
showTracerOptions();
} catch (Exception e) {
traceButtons.clear();
traceOptions.getChildren().clear();
Label empty = new Label("End of trace");
empty.setId("step");
traceOptions.getChildren().add(empty);
}
}
List<Button> getTraceButtons() {
return traceButtons;
}
Tracer getTracer() {
return tracer;
}
}

View File

@ -0,0 +1,195 @@
/*
* BSD License
*
* Open Source Fixedpoint Model-Checker Graphical User Interface version 2019
*
* (C) Copyright Úlfur Jóhann Edvardsson 2019
* (C) Copyright Veronica Julie Lodskov Hoffmann 2019
*
* All Rights Reserved.
*
*/
package Model;
import java.io.BufferedReader;
import java.io.File;
import java.io.IOException;
import java.io.InputStreamReader;
import java.io.PrintWriter;
import java.util.ArrayList;
import java.util.List;
import java.util.Scanner;
import Model.Parser.AST;
public class AnalyseProtocol {
private String userDir,OS, errormsg;
private List<String> originalAnalysis, configs;
private File analysis, anbfile, errorAnB;
private TheParser pp;
public AnalyseProtocol() {
userDir = System.getProperty("user.dir");
analysis = new File(userDir+"//analysis.txt");
anbfile = new File(userDir+"//temp.AnB");
errorAnB = new File(userDir+"//error.AnB");
originalAnalysis = new ArrayList<String>();
this.OS = System.getProperty("os.name");
this.pp = new TheParser("p");
this.errormsg = "";
}
public List<AST> getActions() {
return pp.getActions();
}
public String getAgents() {
return pp.getAgents();
}
// Runs OFMC through cmd / terminal with supplied arguments
public void run(String content) {
try {
buildModifiedProtocol(pp.getParsedProtocol());
String s = "";
Process p;
if (this.OS.startsWith("Windows")) {
s ="C:\\Windows\\system32\\cmd.exe /C start /wait /MIN ofmc -o " + "\"" + userDir + "\\analysis.txt\" " + configs.get(0) + " \"" + anbfile.getAbsolutePath().replaceAll("\\\\","\\\\\\\\") + "\"";
p = Runtime.getRuntime().exec(s , null, new File( configs.get(1) ));
p.waitFor();
}
else if (this.OS.startsWith("Mac")) {
if (!configs.get(2).equals("")) p = new ProcessBuilder(configs.get(1) + "/./ofmc", "-o", userDir + "/analysis.txt", "--numSess",configs.get(0), "--depth", configs.get(2), anbfile.getAbsolutePath()).start();
else p = new ProcessBuilder(configs.get(1) + "/./ofmc", "-o", userDir + "/analysis.txt", "--numSess",configs.get(0), anbfile.getAbsolutePath()).start();
p.waitFor();
}
else if (this.OS.startsWith("Linux")) {
if (!configs.get(2).equals("")) p = new ProcessBuilder(configs.get(1) + "/./ofmc", "-o", userDir + "/analysis.txt", "--numSess",configs.get(0), "--depth", configs.get(2), anbfile.getAbsolutePath()).start();
else p = new ProcessBuilder(configs.get(1) + "/./ofmc", "-o", userDir + "/analysis.txt", "--numSess",configs.get(0), anbfile.getAbsolutePath()).start();
p.waitFor();
}
read();
analysis.deleteOnExit();
} catch (Exception e) {
if (pp.syntaxError) {
try {
PrintWriter writer;
writer = new PrintWriter(errorAnB);
writer.println(content);
writer.close();
errorAnB.deleteOnExit();
errormsg = "";
String s = "";
Process p;
if (this.OS.startsWith("Windows")) {
ProcessBuilder pb = new ProcessBuilder();
pb.command("cmd.exe", "/c", "ofmc " + configs.get(0) + " \"" + errorAnB.getAbsolutePath().replaceAll("\\\\","\\\\\\\\") + "\"");
Process pro = pb.start();
BufferedReader r = new BufferedReader(new InputStreamReader(pro.getErrorStream()));
String line;
while ((line = r.readLine()) != null) {
errormsg = errormsg + line;
}
pro.waitFor();
}
else if (this.OS.startsWith("Mac")) {
if (!configs.get(2).equals("")) p = new ProcessBuilder(configs.get(1) + "/./ofmc", "--numSess",configs.get(0), "--depth", configs.get(2), errorAnB.getAbsolutePath()).start();
else p = new ProcessBuilder(configs.get(1) + "/./ofmc", "--numSess",configs.get(0), anbfile.getAbsolutePath()).start();
BufferedReader r = new BufferedReader(new InputStreamReader(p.getErrorStream()));
String line;
while ((line = r.readLine()) != null) {
errormsg = errormsg + line;
}
p.waitFor();
}
else if (this.OS.startsWith("Linux")) {
if (!configs.get(2).equals("")) p = new ProcessBuilder(configs.get(1) + "/./ofmc", "--numSess",configs.get(0), "--depth", configs.get(2), errorAnB.getAbsolutePath()).start();
else p = new ProcessBuilder(configs.get(1) + "/./ofmc", "--numSess",configs.get(0), anbfile.getAbsolutePath()).start();
BufferedReader r = new BufferedReader(new InputStreamReader(p.getErrorStream()));
String line;
while ((line = r.readLine()) != null) {
errormsg = errormsg + line;
}
p.waitFor();
}
} catch (Exception ex) {
}
}
}
}
// read output of ofmc and send to the parser
private void read() {
originalAnalysis = new ArrayList<String>();
try {
Scanner s = new Scanner(analysis);
while (s.hasNext()) originalAnalysis.add(s.nextLine());
s.close();
} catch (Exception e) {
}
String output = "";
for (String a : originalAnalysis) output = output + a + "\n";
pp.setType("a");
pp.parse(output);
}
public String geterrormsg() {
return this.errormsg;
}
public void modifyProtocol(String s) {
pp.parse(s);
}
public String getAnalysis(){
String analysis = "";
for (String line : originalAnalysis) {
analysis = analysis + line + "\n";
}
return analysis;
}
public void buildModifiedProtocol(String content) {
try {
PrintWriter writer;
writer = new PrintWriter(anbfile);
writer.println(content);
writer.close();
anbfile.deleteOnExit();
} catch (IOException ex) {
}
}
public List<AST> getSimpleAnalysis() {
if (!getAttackFound()) return new ArrayList<AST>();
return pp.getAttackTrace();
}
public boolean getAttackFound() {
return this.pp.attackFound();
}
public void setConfigs(List<String> configs) {
this.configs = configs;
}
public boolean getSyntaxError() {
return pp.syntaxError;
}
}

203
src/Model/Config.java Normal file
View File

@ -0,0 +1,203 @@
/*
* BSD License
*
* Open Source Fixedpoint Model-Checker Graphical User Interface version 2019
*
* (C) Copyright <EFBFBD>lfur J<EFBFBD>hann Edvardsson 2019
* (C) Copyright Veronica Julie Lodskov Hoffmann 2019
*
* All Rights Reserved.
*
*/
package Model;
import java.io.File;
import java.util.ArrayList;
import java.util.List;
import java.util.Optional;
import javafx.event.ActionEvent;
import javafx.event.EventHandler;
import javafx.geometry.Insets;
import javafx.scene.Node;
import javafx.scene.Scene;
import javafx.scene.control.Button;
import javafx.scene.control.ButtonBar.ButtonData;
import javafx.scene.control.ButtonType;
import javafx.scene.control.Dialog;
import javafx.scene.control.Label;
import javafx.scene.control.TextField;
import javafx.scene.layout.GridPane;
import javafx.scene.layout.HBox;
import javafx.scene.layout.StackPane;
import javafx.scene.layout.VBox;
import javafx.stage.FileChooser;
import javafx.stage.Stage;
import javafx.util.Pair;
public class Config {
private int numSess, depth;
private String location, OS;
private File file;
private boolean depthChanged;
public Config() {
this.numSess = 2;
this.depth = 0;
this.OS = System.getProperty("os.name");
this.location = System.getProperty("user.dir");
if(OS.contains("Win"))location.replaceAll("\\\\","\\\\\\\\");
this.depthChanged = false;
}
public List<String> getConfigs() {
List<String> configs = new ArrayList<String>();
String s = "";
String dep = "";
if (this.OS.contains("Win")) s = "--numSess " + Integer.toString(numSess);
else s = Integer.toString(numSess);
if (depth != 0) {
if (this.OS.contains("Win")) s = s + " --depth " + depth;
else dep = Integer.toString(depth);
}
configs.add(s);
configs.add(location);
configs.add(dep);
return configs;
}
public String getLocation() {
return this.location;
}
// The configuration window
public void sConfig() {
Dialog<Pair<String, String>> dialog = new Dialog<>();
dialog.setTitle("Configurations");
dialog.setHeaderText(null);
ButtonType buttonSave = new ButtonType("Save", ButtonData.OK_DONE);
dialog.getDialogPane().getButtonTypes().addAll(buttonSave, ButtonType.CANCEL);
GridPane gp = new GridPane();
gp.setHgap(10);
gp.setVgap(10);
gp.setPadding(new Insets(20, 150, 10, 10));
TextField numberofs = new TextField();
numberofs.setText("" + numSess);
numberofs.setPromptText("" + numSess);
TextField dep = new TextField();
String d = "" + depth;
if (!depthChanged || depth == 0) d = "Infinite";
dep.setPromptText(d);
dep.setText(d);
gp.add(new Label("Number of sessions:"), 0, 0);
gp.add(numberofs, 1, 0);
gp.add(new Label("Depth (Set to 0 for infinite):"), 0, 1);
gp.add(dep, 1, 1);
Node savebutton = dialog.getDialogPane().lookupButton(buttonSave);
savebutton.setDisable(true);
numberofs.textProperty().addListener((observable, oldValue, newValue) -> {
if(numberofs.getText().equals("") || !notNeg(numberofs.getText()) || numberofs.getText().equals("0") || dep.getText().equals("") || !notNeg(dep.getText())) savebutton.setDisable(true);
else savebutton.setDisable(!notNeg(numberofs.getText()));
});
dep.textProperty().addListener((observable, oldValue, newValue) -> {
if(numberofs.getText().equals("") || !notNeg(numberofs.getText()) || numberofs.getText().equals("0") || dep.getText().equals("") || !notNeg(dep.getText())) savebutton.setDisable(true);
else savebutton.setDisable(!notNeg(dep.getText()));
});
dialog.getDialogPane().setContent(gp);
dialog.setResultConverter(dialogButton -> {
if (dialogButton == buttonSave) {
return new Pair<>(numberofs.getText(), dep.getText());
}
return null;
});
Optional<Pair<String, String>> result = dialog.showAndWait();
if (result.isPresent()){
try {
int temp = Integer.parseInt(numberofs.getText());
numSess = temp;
temp = Integer.parseInt(dep.getText());
if (depth != temp) depthChanged = true;
depth = temp;
} catch (Exception e) {
// System.out.println("Error Message");
}
}
}
private boolean notNeg(String s) {
if (s.equals("Infinite")) return true;
try {
int temp = Integer.parseInt(s);
if (temp >= 0) return true;
} catch (Exception e) {
}
return false;
}
// If ofmc is not located in the userdir this is called
public void locateOFMC () {
Label secondLabel = new Label("Please locate ofmc");
StackPane secondaryLayout = new StackPane();
secondaryLayout.getChildren().add(secondLabel);
Scene secondScene = new Scene(secondaryLayout, 600, 400);
Stage newWindow = new Stage();
newWindow.setTitle("Locate OFMC");
newWindow.setScene(secondScene);
HBox hbox = new HBox();
VBox root = new VBox();
TextField tinput = new TextField(this.location);
hbox.getChildren().add(tinput);
Button browse = new Button("Browse");
browse.setOnAction(new EventHandler<ActionEvent>() {
@Override public void handle(ActionEvent e) {
FileChooser chooser = new FileChooser();
file = chooser.showOpenDialog(null);
tinput.setText(file.getAbsolutePath());
tinput.autosize();
}
});
hbox.getChildren().add(browse);
root.getChildren().add(hbox);
hbox = new HBox();
Button ok = new Button("OK");
ok.setOnAction(new EventHandler<ActionEvent>() {
@Override public void handle(ActionEvent e) {
location = file.getAbsolutePath().substring(0,file.getAbsolutePath().lastIndexOf(File.separator));
if(OS.contains("Win"))location = location.replaceAll("\\\\","\\\\\\\\");
newWindow.close();
}
});
hbox.getChildren().add(ok);
Button cancel = new Button("Cancel");
cancel.setOnAction(new EventHandler<ActionEvent>() {
@Override public void handle(ActionEvent e) {
newWindow.close();
}
});
hbox.getChildren().add(cancel);
root.getChildren().add(hbox);
secondScene.getWindow().sizeToScene();
secondScene.setRoot(root);
newWindow.show();
newWindow.toFront();
}
// Check if ofmc is located in userdir
public boolean locationCheck() {
File file;
if (this.OS.startsWith("Win")) file = new File(location + "\\\\ofmc.exe");
else file = new File(location + "/ofmc");
return file.exists();
}
}

View File

@ -0,0 +1,52 @@
/*
* BSD License
*
* Open Source Fixedpoint Model-Checker Graphical User Interface version 2019
*
* (C) Copyright <EFBFBD>lfur J<EFBFBD>hann Edvardsson 2019
* (C) Copyright Veronica Julie Lodskov Hoffmann 2019
*
* All Rights Reserved.
*
*/
package Model.Parser;
public class AList extends TwoVarStepProvider{
private Message fst, snd;
public AList (AST first, AST second) {
this.fst = (Message) first;
this.snd = (Message) second;
}
@Override
public String toString() {
return this.fst.toString() + "," + this.snd.toString();
}
@Override
public Message getV1() {
return fst;
}
@Override
public Message getV2() {
return snd;
}
@Override
public Integer getStepNo() {
if (fst instanceof StepProvider) return ((Variable)fst).getStepNo();
else return ((TwoVarStepProvider)fst).getStepNo();
}
@Override
public void substitude(String oldVar, Variable newVar) {
fst.substitude(oldVar, newVar);
snd.substitude(oldVar, newVar);
}
}

20
src/Model/Parser/AST.java Normal file
View File

@ -0,0 +1,20 @@
/*
* BSD License
*
* Open Source Fixedpoint Model-Checker Graphical User Interface version 2019
*
* (C) Copyright <EFBFBD>lfur J<EFBFBD>hann Edvardsson 2019
* (C) Copyright Veronica Julie Lodskov Hoffmann 2019
*
* All Rights Reserved.
*
*/
package Model.Parser;
public abstract class AST {
public abstract String toString();
}

View File

@ -0,0 +1,73 @@
/*
* BSD License
*
* Open Source Fixedpoint Model-Checker Graphical User Interface version 2019
*
* (C) Copyright <EFBFBD>lfur J<EFBFBD>hann Edvardsson 2019
* (C) Copyright Veronica Julie Lodskov Hoffmann 2019
*
* All Rights Reserved.
*
*/
package Model.Parser;
import java.util.ArrayList;
import java.util.List;
public class Action extends Actions {
private Message agents, message;
private List<Actions> actions;
private String step;
public Action (AST msg, AST ags, int i) {
this.agents = (Message) ags;
this.message = (Message) msg;
this.actions = new ArrayList<Actions>();
this.actions.add(this);
this.step = "";
}
public Action (Action act, Action a) {
this.actions = new ArrayList<Actions>();
this.actions.add(act);
this.actions.addAll(a.getList());
}
@Override
public String toString() {
return this.agents.toString() + ": " + this.step + this.message.toString();
}
@Override
public List<Actions> getList() {
return this.actions;
}
@Override
public void addStep(int i) {
this.step = "step" + i + ",";
}
@Override
public FromTo getAgents() {
return (FromTo) this.agents;
}
@Override
public Integer getStepNo() {
return ((TwoVarStepProvider)message).getStepNo();
}
@Override
public void substitude(String oldVar, Variable newVar) {
agents.substitude(oldVar, newVar);
message.substitude(oldVar, newVar);
}
@Override
public Message getMsg() {
return this.message;
}
}

View File

@ -0,0 +1,52 @@
/*
* BSD License
*
* Open Source Fixedpoint Model-Checker Graphical User Interface version 2019
*
* (C) Copyright <EFBFBD>lfur J<EFBFBD>hann Edvardsson 2019
* (C) Copyright Veronica Julie Lodskov Hoffmann 2019
*
* All Rights Reserved.
*
*/
package Model.Parser;
import java.util.ArrayList;
import java.util.List;
public class ActionKeeper extends ModifiableKeepers {
private Variable title;
private List<Actions> action;
public ActionKeeper(Variable title, Actions t) {
this.title = title;
this.action = t.getList();
modify(1);
}
@Override
public String toString() {
String m = title.toString() + ":\n";
for (Actions t : action) m = m + t.toString() + "\n";
m = m + "\n";
return m;
}
@Override
public List<AST> getList() {
List<AST> re = new ArrayList<AST>();
for(Actions a : action) re.add(a);
return re;
}
@Override
public void modify(int i) {
for(AST a : action) {
Actions mod = (Actions) a;
mod.addStep(i);
i++;
}
}
}

View File

@ -0,0 +1,30 @@
/*
* BSD License
*
* Open Source Fixedpoint Model-Checker Graphical User Interface version 2019
*
* (C) Copyright <EFBFBD>lfur J<EFBFBD>hann Edvardsson 2019
* (C) Copyright Veronica Julie Lodskov Hoffmann 2019
*
* All Rights Reserved.
*
*/
package Model.Parser;
import java.util.List;
public abstract class Actions extends AST {
public abstract List<Actions> getList();
public abstract void addStep(int i);
public abstract FromTo getAgents();
public abstract Message getMsg();
public abstract Integer getStepNo();
public abstract void substitude(String oldVar, Variable newVar);
}

View File

@ -0,0 +1,319 @@
/*
* BSD License
*
* Open Source Fixedpoint Model-Checker Graphical User Interface version 2019
*
* (C) Copyright <EFBFBD>lfur J<EFBFBD>hann Edvardsson 2019
* (C) Copyright Veronica Julie Lodskov Hoffmann 2019
*
* All Rights Reserved.
*
*/
package Model.Parser;
import org.antlr.v4.runtime.BailErrorStrategy;
import org.antlr.v4.runtime.CharStream;
import org.antlr.v4.runtime.CharStreams;
import org.antlr.v4.runtime.CommonTokenStream;
public class AnalysisParser {
public AnalysisParser () {}
public AST run(String t) throws Exception {
// Translate the input string into stream of characters
CharStream inputStream = CharStreams.fromString(t);
// Create a lexer for the CharStream
aparserLexer lex = new aparserLexer(inputStream);
// Use the lexer to generate the token stream
CommonTokenStream tokens = new CommonTokenStream(lex);
// Create a parser for the given token stream and start it
try {
// Instantiate an evaluator
Evaluator evaluator = new Evaluator();
aparserParser parser = new aparserParser(tokens);
parser.setErrorHandler(new BailErrorStrategy());
return evaluator.visit(parser.start());
} catch (Exception e){
}
return null;
}
class Evaluator extends aparserBaseVisitor<AST> {
Evaluator() {
}
@Override
public AST visitStart (aparserParser.StartContext ctx) {
Keeper keep = new Keeper();
for (int i = 0; i<ctx.begin().size(); i++) {
keep.keep(this.visit(ctx.begin(i)));
}
return keep;
}
@Override
public AST visitFunVer (aparserParser.FunVerContext ctx) {
return new TextKeeper(new Variable(ctx.t.getText()), null, visit(ctx.fun));
}
@Override
public AST visitFunIn (aparserParser.FunInContext ctx) {
return new TextKeeper(new Variable(ctx.t.getText()), null, visit(ctx.fun));
}
@Override
public AST visitFunSum (aparserParser.FunSumContext ctx) {
return new SummaryKeeper(new Variable(ctx.t.getText()), visit(ctx.fun));
}
@Override
public AST visitFunGoal (aparserParser.FunGoalContext ctx) {
return new TextKeeper(new Variable(ctx.t.getText()), null, visit(ctx.fun));
}
@Override
public AST visitFunDet (aparserParser.FunDetContext ctx) {
return new TextKeeper(new Variable(ctx.t.getText()), null, visit(ctx.fun));
}
@Override
public AST visitFunBack (aparserParser.FunBackContext ctx) {
return new TextKeeper(new Variable(ctx.t.getText()), new Variable(ctx.t2.getText()), visit(ctx.fun));
}
@Override
public AST visitFunStat (aparserParser.FunStatContext ctx) {
return new StatKeeper(new Variable(ctx.t.getText()), (Stats)visit(ctx.fun));
}
@Override
public AST visitFunTrace (aparserParser.FunTraceContext ctx) {
return new TraceKeeper(new Variable(ctx.t.getText()), (Trace) visit(ctx.fun));
}
@Override
public AST visitNameDot (aparserParser.NameDotContext ctx) {
return new Dot((Variable)visit(ctx.fun1), (Variable)visit(ctx.fun2));
}
@Override
public AST visitNameV (aparserParser.NameVContext ctx) {
return new Variable(ctx.var.getText());
}
@Override
public AST visitNameN (aparserParser.NameNContext ctx) {
return new Variable(ctx.n.getText());
}
@Override
public AST visitNameF (aparserParser.NameFContext ctx) {
return new Variable(ctx.getText());
}
@Override
public AST visitTraceMore (aparserParser.TraceMoreContext ctx) {
return new Trace((Action)visit(ctx.fun), (Trace)visit(ctx.fun2));
}
@Override
public AST visitTraceLast (aparserParser.TraceLastContext ctx) {
return new Trace((Action)visit(ctx.fun));
}
@Override
public AST visitAAct (aparserParser.AActContext ctx) {
return new Action(visit(ctx.mes), visit(ctx.fun), 1);
}
@Override
public AST visitFromTo (aparserParser.FromToContext ctx) {
return new FromTo(visit(ctx.from), visit(ctx.arrow), visit(ctx.to));
}
@Override
public AST visitRegular (aparserParser.RegularContext ctx) {
return new Variable("->");
}
@Override
public AST visitStar (aparserParser.StarContext ctx) {
return new Variable("*->");
}
@Override
public AST visitArrowstar (aparserParser.ArrowstarContext ctx) {
return new Variable("->*");
}
@Override
public AST visitStararrowstar (aparserParser.StararrowstarContext ctx) {
return new Variable("*->*");
}
@Override
public AST visitWVar (aparserParser.WVarContext ctx) {
return new Variable(ctx.v.getText());
}
@Override
public AST visitWNum (aparserParser.WNumContext ctx) {
return new Variable(ctx.n.getText());
}
@Override
public AST visitWComma (aparserParser.WCommaContext ctx) {
return new Wcomma(visit(ctx.fun1), visit(ctx.fun2));
}
@Override
public AST visitMcomma (aparserParser.McommaContext ctx) {
return new AList(visit(ctx.mes1), visit(ctx.mes2));
}
@Override
public AST visitMnocomma (aparserParser.MnocommaContext ctx) {
return visit(ctx.n);
}
@Override
public AST visitNormfunction (aparserParser.NormfunctionContext ctx) {
return new Function(new Variable(ctx.v.getText()), visit(ctx.l));
}
@Override
public AST visitNormnoenc (aparserParser.NormnoencContext ctx) {
return new NoEnc(visit(ctx.mes), visit(ctx.n));
}
@Override
public AST visitNormenc (aparserParser.NormencContext ctx) {
return new SymEnc(visit(ctx.mes), visit(ctx.n));
}
@Override
public AST visitNormvariable (aparserParser.NormvariableContext ctx) {
return new Variable(ctx.v.getText());
}
@Override
public AST visitNormnum (aparserParser.NormnumContext ctx) {
return new Variable(ctx.n.getText());
}
@Override
public AST visitNormMore (aparserParser.NormMoreContext ctx) {
return new NormMore(visit(ctx.n));
}
@Override
public AST visitNormUnder (aparserParser.NormUnderContext ctx) {
return new Variable("_");
}
@Override
public AST visitNormparenth (aparserParser.NormparenthContext ctx) {
return new Function(new Variable(""), visit(ctx.mes));
}
@Override
public AST visitLimore(aparserParser.LimoreContext ctx) {
return new AList(visit(ctx.no), visit(ctx.l));
}
@Override
public AST visitLisingle(aparserParser.LisingleContext ctx) {
return visit(ctx.no);
}
@Override
public AST visitStatBoth (aparserParser.StatBothContext ctx) {
return new Stat((Variable)visit(ctx.fun), new Variable(ctx.n.getText()), new Variable(ctx.v.getText()), true, (Stat)visit(ctx.fun2));
}
@Override
public AST visitStatStat (aparserParser.StatStatContext ctx) {
return new Stat((Variable)visit(ctx.fun), new Variable(ctx.n.getText()), new Variable(ctx.v.getText()), false, (Stat)visit(ctx.fun2));
}
@Override
public AST visitStatNeither (aparserParser.StatNeitherContext ctx) {
return new Stat((Variable)visit(ctx.fun), new Variable(ctx.n.getText()), new Variable(ctx.v.getText()), false);
}
@Override
public AST visitStatCol (aparserParser.StatColContext ctx) {
return new Stat((Variable)visit(ctx.fun), new Variable(ctx.n.getText()), new Variable(ctx.v.getText()), true);
}
@Override
public AST visitTypesT (aparserParser.TypesTContext ctx) {
return new Variable("TIME");
}
@Override
public AST visitTypesP (aparserParser.TypesPContext ctx) {
return new Variable("parseTime");
}
@Override
public AST visitTypesV (aparserParser.TypesVContext ctx) {
return new Variable("visitedNodes");
}
@Override
public AST visitTypesD (aparserParser.TypesDContext ctx) {
return new Variable("depth");
}
@Override
public AST visitFVer (aparserParser.FVerContext ctx) {
return new Variable(ctx.n.getText());
}
@Override
public AST visitTexU (aparserParser.TexUContext ctx) {
return new UnderSep(visit(ctx.fun), visit(ctx.fun2));
}
@Override
public AST visitTexA (aparserParser.TexAContext ctx) {
return new Variable(ctx.v.getText());
}
@Override
public AST visitTexN (aparserParser.TexNContext ctx) {
return new Variable(ctx.v.getText());
}
@Override
public AST visitTexF (aparserParser.TexFContext ctx) {
return new Variable(ctx.v.getText());
}
@Override
public AST visitTexMore (aparserParser.TexMoreContext ctx) {
return new Variable(ctx.v.getText());
}
@Override
public AST visitTexV (aparserParser.TexVContext ctx) {
return new Variable(ctx.v.getText());
}
}
}

View File

@ -0,0 +1,28 @@
/*
* BSD License
*
* Open Source Fixedpoint Model-Checker Graphical User Interface version 2019
*
* (C) Copyright <EFBFBD>lfur J<EFBFBD>hann Edvardsson 2019
* (C) Copyright Veronica Julie Lodskov Hoffmann 2019
*
* All Rights Reserved.
*
*/
package Model.Parser;
public class ArrowGoal extends Goals{
Message w2w,m;
public ArrowGoal (Message w2w, Message m) {
this.w2w = w2w;
this.m = m;
}
@Override
public String toString() {
return this.w2w.toString() + " : " + this.m.toString();
}
}

View File

@ -0,0 +1,31 @@
/*
* BSD License
*
* Open Source Fixedpoint Model-Checker Graphical User Interface version 2019
*
* (C) Copyright <EFBFBD>lfur J<EFBFBD>hann Edvardsson 2019
* (C) Copyright Veronica Julie Lodskov Hoffmann 2019
*
* All Rights Reserved.
*
*/
package Model.Parser;
public class Authenticates extends Goals{
private String weakly;
private Message w, w2,m;
public Authenticates (Message w, Message w2, Message m ,String weakly) {
this.weakly = weakly;
this.w = w;
this.w2 = w2;
this.m = m;
}
@Override
public String toString() {
return w.toString() + " " + weakly + " authenticates " + w2.toString() + " on " + m.toString();
}
}

View File

@ -0,0 +1,30 @@
/*
* BSD License
*
* Open Source Fixedpoint Model-Checker Graphical User Interface version 2019
*
* (C) Copyright <EFBFBD>lfur J<EFBFBD>hann Edvardsson 2019
* (C) Copyright Veronica Julie Lodskov Hoffmann 2019
*
* All Rights Reserved.
*
*/
package Model.Parser;
public class Constraints extends Extra {
private AST m1, rest;
public Constraints(AST m1, AST rest) {
this.m1 = m1;
this.rest = rest;
}
@Override
public String toString() {
if (this.rest != null) return m1.toString() + rest.toString();
return m1.toString();
}
}

29
src/Model/Parser/Dot.java Normal file
View File

@ -0,0 +1,29 @@
/*
* BSD License
*
* Open Source Fixedpoint Model-Checker Graphical User Interface version 2019
*
* (C) Copyright <EFBFBD>lfur J<EFBFBD>hann Edvardsson 2019
* (C) Copyright Veronica Julie Lodskov Hoffmann 2019
*
* All Rights Reserved.
*
*/
package Model.Parser;
public class Dot extends Extra {
private Variable v1,v2;
public Dot (Variable v1, Variable v2) {
this.v1 = v1;
this.v2 = v2;
}
@Override
public String toString() {
return this.v1.toString() + "." + v2.toString();
}
}

View File

@ -0,0 +1,17 @@
/*
* BSD License
*
* Open Source Fixedpoint Model-Checker Graphical User Interface version 2019
*
* (C) Copyright <EFBFBD>lfur J<EFBFBD>hann Edvardsson 2019
* (C) Copyright Veronica Julie Lodskov Hoffmann 2019
*
* All Rights Reserved.
*
*/
package Model.Parser;
public abstract class Extra extends Messages{
}

View File

@ -0,0 +1,47 @@
/*
* BSD License
*
* Open Source Fixedpoint Model-Checker Graphical User Interface version 2019
*
* (C) Copyright <EFBFBD>lfur J<EFBFBD>hann Edvardsson 2019
* (C) Copyright Veronica Julie Lodskov Hoffmann 2019
*
* All Rights Reserved.
*
*/
package Model.Parser;
public class FromTo extends TwoVar {
private Message agent1, agent2, arrow;
public FromTo(AST ag1, AST arr, AST ag2) {
this.agent1 = (Message) ag1;
this.arrow = (Message) arr;
this.agent2 = (Message) ag2;
}
@Override
public String toString() {
return agent1.toString() + arrow.toString() + agent2.toString();
}
@Override
public Message getV1() {
return agent1;
}
@Override
public Message getV2() {
return agent2;
}
@Override
public void substitude(String oldVar, Variable newVar) {
agent1.substitude(oldVar, newVar);
agent2.substitude(oldVar, newVar);
}
}

View File

@ -0,0 +1,45 @@
/*
* BSD License
*
* Open Source Fixedpoint Model-Checker Graphical User Interface version 2019
*
* (C) Copyright <EFBFBD>lfur J<EFBFBD>hann Edvardsson 2019
* (C) Copyright Veronica Julie Lodskov Hoffmann 2019
*
* All Rights Reserved.
*
*/
package Model.Parser;
public class Function extends TwoVar{
private Variable funName;
private Message msg;
public Function(Variable name, AST msg) {
this.funName = name;
this.msg = (Message) msg;
}
@Override
public String toString() {
return this.funName.toString() + "(" + msg.toString() + ")";
}
@Override
public Message getV1() {
return funName;
}
@Override
public Message getV2() {
return msg;
}
@Override
public void substitude(String oldVar, Variable newVar) {
msg.substitude(oldVar, newVar);
}
}

View File

@ -0,0 +1,41 @@
/*
* BSD License
*
* Open Source Fixedpoint Model-Checker Graphical User Interface version 2019
*
* (C) Copyright <EFBFBD>lfur J<EFBFBD>hann Edvardsson 2019
* (C) Copyright Veronica Julie Lodskov Hoffmann 2019
*
* All Rights Reserved.
*
*/
package Model.Parser;
import java.util.ArrayList;
import java.util.List;
public class Goal extends GoalsWithLists{
private List<Goals> goals;
public Goal (Goals g1, Goals rest) {
this.goals = new ArrayList<Goals>();
this.goals.add(g1);
this.goals.addAll(((GoalsWithLists) rest).getList());
}
public Goal (Goals goal) {
this.goals = new ArrayList<Goals>();
this.goals.add(goal);
}
@Override
public String toString() {
return "";
}
@Override
public List<Goals> getList() {
return this.goals;
}
}

View File

@ -0,0 +1,18 @@
/*
* BSD License
*
* Open Source Fixedpoint Model-Checker Graphical User Interface version 2019
*
* (C) Copyright <EFBFBD>lfur J<EFBFBD>hann Edvardsson 2019
* (C) Copyright Veronica Julie Lodskov Hoffmann 2019
*
* All Rights Reserved.
*
*/
package Model.Parser;
public abstract class Goals extends AST {
}

View File

@ -0,0 +1,41 @@
/*
* BSD License
*
* Open Source Fixedpoint Model-Checker Graphical User Interface version 2019
*
* (C) Copyright <EFBFBD>lfur J<EFBFBD>hann Edvardsson 2019
* (C) Copyright Veronica Julie Lodskov Hoffmann 2019
*
* All Rights Reserved.
*
*/
package Model.Parser;
import java.util.ArrayList;
import java.util.List;
public class GoalsKeeper extends KeepersWithLists {
private Variable title;
private List<Goals> goals;
public GoalsKeeper(Variable title, Goals t) {
this.title = title;
this.goals = ((GoalsWithLists) t).getList();
}
@Override
public String toString() {
String m = title.toString() + ":\n";
for (Goals t : goals) m = m + t.toString() + "\n";
return m;
}
@Override
public List<AST> getList() {
List<AST> re = new ArrayList<AST>();
for(Goals a : goals) re.add(a);
return re;
}
}

View File

@ -0,0 +1,21 @@
/*
* BSD License
*
* Open Source Fixedpoint Model-Checker Graphical User Interface version 2019
*
* (C) Copyright <EFBFBD>lfur J<EFBFBD>hann Edvardsson 2019
* (C) Copyright Veronica Julie Lodskov Hoffmann 2019
*
* All Rights Reserved.
*
*/
package Model.Parser;
import java.util.List;
public abstract class GoalsWithLists extends Goals{
public abstract List<Goals> getList();
}

View File

@ -0,0 +1,43 @@
/*
* BSD License
*
* Open Source Fixedpoint Model-Checker Graphical User Interface version 2019
*
* (C) Copyright <EFBFBD>lfur J<EFBFBD>hann Edvardsson 2019
* (C) Copyright Veronica Julie Lodskov Hoffmann 2019
*
* All Rights Reserved.
*
*/
package Model.Parser;
import java.util.ArrayList;
import java.util.List;
public class History extends TracingAB {
private List<Actions> history;
public History (Action action, History hist) {
this.history = new ArrayList<Actions>();
history.add(action);
history.addAll(hist.getList());
}
public History (Action action) {
this.history = new ArrayList<Actions>();
history.add(action);
}
@Override
public List<Actions> getList() {
return this.history;
}
@Override
public String toString() {
String re = "";
for (Actions h : history) re = re + h.toString() + "\n";
return re;
}
}

View File

@ -0,0 +1,41 @@
/*
* BSD License
*
* Open Source Fixedpoint Model-Checker Graphical User Interface version 2019
*
* (C) Copyright <EFBFBD>lfur J<EFBFBD>hann Edvardsson 2019
* (C) Copyright Veronica Julie Lodskov Hoffmann 2019
*
* All Rights Reserved.
*
*/
package Model.Parser;
import java.util.ArrayList;
import java.util.List;
public class HistoryKeeper extends KeepersWithLists {
private Variable title;
private List<Actions> action;
public HistoryKeeper (Variable title, History t) {
this.title = title;
this.action = t.getList();
}
@Override
public String toString() {
String m = "";
for (Actions t : action) m = m + t.toString() + "\n";
return m;
}
@Override
public List<AST> getList() {
List<AST> re = new ArrayList<AST>();
for(Actions a : action) re.add(a);
return re;
}
}

View File

@ -0,0 +1,63 @@
/*
* BSD License
*
* Open Source Fixedpoint Model-Checker Graphical User Interface version 2019
*
* (C) Copyright <EFBFBD>lfur J<EFBFBD>hann Edvardsson 2019
* (C) Copyright Veronica Julie Lodskov Hoffmann 2019
*
* All Rights Reserved.
*
*/
package Model.Parser;
import java.util.ArrayList;
import java.util.List;
public class Keeper extends KeeperOfAll{
private List<AST> msgs;
public Keeper() {
msgs = new ArrayList<AST>();
}
public void keep(AST m) {
msgs.add(m);
}
@Override
public String toString() {
String re = "";
for (AST a : msgs) re = re + a.toString();
return re;
}
@Override
public AST getType(String c) {
switch (c) {
case "Actions":
for (AST m : msgs) if (m instanceof ActionKeeper) return m;
break;
case "Knowledge":
for (AST m : msgs) if (m instanceof KnowledgeKeeper) return m;
break;
case "Trace":
for (AST m : msgs) if (m instanceof TraceKeeper) return m;
break;
case "Summary":
for (AST m : msgs) if (m instanceof SummaryKeeper) return m;
break;
case "Options":
for (AST m : msgs) if (m instanceof Options) return m;
break;
case "Types":
for (AST m : msgs) if (m instanceof TypesKeeper) return m;
break;
default:
break;
}
return null;
}
}

View File

@ -0,0 +1,21 @@
/*
* BSD License
*
* Open Source Fixedpoint Model-Checker Graphical User Interface version 2019
*
* (C) Copyright <EFBFBD>lfur J<EFBFBD>hann Edvardsson 2019
* (C) Copyright Veronica Julie Lodskov Hoffmann 2019
*
* All Rights Reserved.
*
*/
package Model.Parser;
public abstract class KeeperOfAll extends Keepers{
public abstract AST getType(String c);
public abstract void keep(AST m);
}

View File

@ -0,0 +1,18 @@
/*
* BSD License
*
* Open Source Fixedpoint Model-Checker Graphical User Interface version 2019
*
* (C) Copyright <EFBFBD>lfur J<EFBFBD>hann Edvardsson 2019
* (C) Copyright Veronica Julie Lodskov Hoffmann 2019
*
* All Rights Reserved.
*
*/
package Model.Parser;
public abstract class Keepers extends AST {
}

View File

@ -0,0 +1,20 @@
/*
* BSD License
*
* Open Source Fixedpoint Model-Checker Graphical User Interface version 2019
*
* (C) Copyright <EFBFBD>lfur J<EFBFBD>hann Edvardsson 2019
* (C) Copyright Veronica Julie Lodskov Hoffmann 2019
*
* All Rights Reserved.
*
*/
package Model.Parser;
import java.util.List;
public abstract class KeepersWithLists extends Keepers{
public abstract List<AST> getList();
}

View File

@ -0,0 +1,63 @@
/*
* BSD License
*
* Open Source Fixedpoint Model-Checker Graphical User Interface version 2019
*
* (C) Copyright <EFBFBD>lfur J<EFBFBD>hann Edvardsson 2019
* (C) Copyright Veronica Julie Lodskov Hoffmann 2019
*
* All Rights Reserved.
*
*/
package Model.Parser;
import java.util.ArrayList;
import java.util.List;
public class Knowledge extends KnowledgeAb{
private AST knows;
private Variable agent;
private List<KnowledgeAb> all;
private String steps;
public Knowledge(String agent, AST m) {
this.all = new ArrayList<KnowledgeAb>();
all.add(new Knowledge(m, agent));
}
public Knowledge (AST m, String ag) {
this.knows = m;
this.agent = new Variable(ag);
steps = "";
}
@Override
public String toString() {
return agent.toString() + ": " + knows.toString() + steps + ";";
}
public void register(KnowledgeAb a) {
this.all.add(a);
}
@Override
public void combine(List<KnowledgeAb> visit) {
all.addAll(visit);
}
@Override
public List<KnowledgeAb> getList() {
return this.all;
}
@Override
public void addSteps(int i) {
for(int a = 1; a<=i; a++) {
steps = steps + ",step" + a;
}
}
}

View File

@ -0,0 +1,25 @@
/*
* BSD License
*
* Open Source Fixedpoint Model-Checker Graphical User Interface version 2019
*
* (C) Copyright <EFBFBD>lfur J<EFBFBD>hann Edvardsson 2019
* (C) Copyright Veronica Julie Lodskov Hoffmann 2019
*
* All Rights Reserved.
*
*/
package Model.Parser;
import java.util.List;
public abstract class KnowledgeAb extends AST{
public abstract void register(KnowledgeAb a);
public abstract void combine(List<KnowledgeAb> visit);
public abstract List<KnowledgeAb> getList();
public abstract void addSteps(int i);
}

View File

@ -0,0 +1,46 @@
/*
* BSD License
*
* Open Source Fixedpoint Model-Checker Graphical User Interface version 2019
*
* (C) Copyright <EFBFBD>lfur J<EFBFBD>hann Edvardsson 2019
* (C) Copyright Veronica Julie Lodskov Hoffmann 2019
*
* All Rights Reserved.
*
*/
package Model.Parser;
import java.util.ArrayList;
import java.util.List;
public class KnowledgeKeeper extends ModifiableKeepers {
private Variable title;
private List<KnowledgeAb> knowledge;
public KnowledgeKeeper(Variable title, KnowledgeAb t) {
this.title = title;
this.knowledge = t.getList();
}
@Override
public String toString() {
String m = title.toString() + ":\n";
for (KnowledgeAb t : knowledge) m = m + t.toString() + "\n";
m = m + "\n";
return m;
}
@Override
public List<AST> getList() {
List<AST> re = new ArrayList<AST>();
for(KnowledgeAb a : knowledge) re.add(a);
return re;
}
@Override
public void modify(int i) {
for(KnowledgeAb k : knowledge) k.addSteps(i);
}
}

View File

@ -0,0 +1,19 @@
/*
* BSD License
*
* Open Source Fixedpoint Model-Checker Graphical User Interface version 2019
*
* (C) Copyright <EFBFBD>lfur J<EFBFBD>hann Edvardsson 2019
* (C) Copyright Veronica Julie Lodskov Hoffmann 2019
*
* All Rights Reserved.
*
*/
package Model.Parser;
public abstract class Message extends Messages {
public abstract void substitude(String oldVar, Variable newVar);
}

View File

@ -0,0 +1,18 @@
/*
* BSD License
*
* Open Source Fixedpoint Model-Checker Graphical User Interface version 2019
*
* (C) Copyright <EFBFBD>lfur J<EFBFBD>hann Edvardsson 2019
* (C) Copyright Veronica Julie Lodskov Hoffmann 2019
*
* All Rights Reserved.
*
*/
package Model.Parser;
public abstract class Messages extends AST {
}

View File

@ -0,0 +1,19 @@
/*
* BSD License
*
* Open Source Fixedpoint Model-Checker Graphical User Interface version 2019
*
* (C) Copyright <EFBFBD>lfur J<EFBFBD>hann Edvardsson 2019
* (C) Copyright Veronica Julie Lodskov Hoffmann 2019
*
* All Rights Reserved.
*
*/
package Model.Parser;
public abstract class ModifiableKeepers extends KeepersWithLists{
public abstract void modify(int i);
}

View File

@ -0,0 +1,27 @@
/*
* BSD License
*
* Open Source Fixedpoint Model-Checker Graphical User Interface version 2019
*
* (C) Copyright <EFBFBD>lfur J<EFBFBD>hann Edvardsson 2019
* (C) Copyright Veronica Julie Lodskov Hoffmann 2019
*
* All Rights Reserved.
*
*/
package Model.Parser;
public class Name extends Protocol{
private Variable name;
public Name (Variable n) {
this.name = n;
}
@Override
public String toString() {
return this.name.toString();
}
}

View File

@ -0,0 +1,46 @@
/*
* BSD License
*
* Open Source Fixedpoint Model-Checker Graphical User Interface version 2019
*
* (C) Copyright <EFBFBD>lfur J<EFBFBD>hann Edvardsson 2019
* (C) Copyright Veronica Julie Lodskov Hoffmann 2019
*
* All Rights Reserved.
*
*/
package Model.Parser;
public class NoEnc extends TwoVar {
private Message msg, norm;
public NoEnc (AST msg, AST norm) {
this.msg = (Message) msg;
this.norm = (Message) norm;
}
@Override
public String toString() {
return "{" + msg.toString() + "}" + norm.toString();
}
@Override
public Message getV1() {
return msg;
}
@Override
public Message getV2() {
return norm;
}
@Override
public void substitude(String oldVar, Variable newVar) {
msg.substitude(oldVar, newVar);
norm.substitude(oldVar, newVar);
}
}

View File

@ -0,0 +1,38 @@
/*
* BSD License
*
* Open Source Fixedpoint Model-Checker Graphical User Interface version 2019
*
* (C) Copyright <EFBFBD>lfur J<EFBFBD>hann Edvardsson 2019
* (C) Copyright Veronica Julie Lodskov Hoffmann 2019
*
* All Rights Reserved.
*
*/
package Model.Parser;
public class NormMore extends OneVar {
private Message norm;
public NormMore (AST norm) {
this.norm = (Message) norm;
}
@Override
public String toString() {
return "_" + this.norm.toString();
}
@Override
public AST getV1() {
return this.norm;
}
@Override
public void substitude(String oldVar, Variable newVar) {
norm.substitude(oldVar, newVar);
}
}

View File

@ -0,0 +1,41 @@
/*
* BSD License
*
* Open Source Fixedpoint Model-Checker Graphical User Interface version 2019
*
* (C) Copyright <EFBFBD>lfur J<EFBFBD>hann Edvardsson 2019
* (C) Copyright Veronica Julie Lodskov Hoffmann 2019
*
* All Rights Reserved.
*
*/
package Model.Parser;
public class NormSq extends OneVar {
private Message m;
private boolean b;
public NormSq(AST m, boolean b) {
this.m = (Message) m;
this.b = b;
}
@Override
public String toString() {
if (b) return ",[" + m.toString() + "]";
else return "[" + m.toString() + "]";
}
@Override
public Message getV1() {
return this.m;
}
@Override
public void substitude(String oldVar, Variable newVar) {
m.substitude(oldVar, newVar);
}
}

View File

@ -0,0 +1,56 @@
/*
* BSD License
*
* Open Source Fixedpoint Model-Checker Graphical User Interface version 2019
*
* (C) Copyright <EFBFBD>lfur J<EFBFBD>hann Edvardsson 2019
* (C) Copyright Veronica Julie Lodskov Hoffmann 2019
*
* All Rights Reserved.
*
*/
package Model.Parser;
public class NotEQ extends ThreeVar{
private Message m1,m2,wa;
private boolean comma;
public NotEQ(AST m1, AST m2, AST wa, boolean b) {
this.m1 = (Message) m1;
this.m2 = (Message) m2;
this.wa = (Message) wa;
this.comma = b;
}
@Override
public String toString() {
if (comma) return this.m1.toString() + "!=" + this.m2.toString() + "," + wa.toString();
else return this.m1.toString() + "!=" + this.m2.toString();
}
@Override
public Message getV1() {
return this.m1;
}
@Override
public Message getV2() {
return this.m2;
}
@Override
public Message getV3() {
return this.wa;
}
@Override
public void substitude(String oldVar, Variable newVar) {
m1.substitude(oldVar, newVar);
m2.substitude(oldVar, newVar);
if (wa!=null) wa.substitude(oldVar, newVar);
}
}

View File

@ -0,0 +1,19 @@
/*
* BSD License
*
* Open Source Fixedpoint Model-Checker Graphical User Interface version 2019
*
* (C) Copyright <EFBFBD>lfur J<EFBFBD>hann Edvardsson 2019
* (C) Copyright Veronica Julie Lodskov Hoffmann 2019
*
* All Rights Reserved.
*
*/
package Model.Parser;
public abstract class OneVar extends Message {
public abstract AST getV1();
}

View File

@ -0,0 +1,43 @@
/*
* BSD License
*
* Open Source Fixedpoint Model-Checker Graphical User Interface version 2019
*
* (C) Copyright <EFBFBD>lfur J<EFBFBD>hann Edvardsson 2019
* (C) Copyright Veronica Julie Lodskov Hoffmann 2019
*
* All Rights Reserved.
*
*/
package Model.Parser;
import java.util.List;
public class Option extends OptionsSingleABsub {
private Variable option;
private List<Actions> actions;
public Option (Variable option, List<Actions> actions) {
this.option = option;
this.actions = actions;
}
@Override
public List<Actions> getList() {
return this.actions;
}
@Override
public String toString() {
String re = "";
for (Actions a : actions) re = re + a.toString() + "\n";
return re;
}
@Override
public void substitude(String oldVar, Variable newVar) {
for(Actions a : actions) a.substitude(oldVar, newVar);
}
}

View File

@ -0,0 +1,21 @@
/*
* BSD License
*
* Open Source Fixedpoint Model-Checker Graphical User Interface version 2019
*
* (C) Copyright <EFBFBD>lfur J<EFBFBD>hann Edvardsson 2019
* (C) Copyright Veronica Julie Lodskov Hoffmann 2019
*
* All Rights Reserved.
*
*/
package Model.Parser;
import java.util.List;
public abstract class OptionSingleAB extends AST{
public abstract List<Actions> getList();
}

View File

@ -0,0 +1,48 @@
/*
* BSD License
*
* Open Source Fixedpoint Model-Checker Graphical User Interface version 2019
*
* (C) Copyright <EFBFBD>lfur J<EFBFBD>hann Edvardsson 2019
* (C) Copyright Veronica Julie Lodskov Hoffmann 2019
*
* All Rights Reserved.
*
*/
package Model.Parser;
import java.util.ArrayList;
import java.util.List;
public class Options extends OptionsABsub {
private List<Option> options;
public Options(Option option) {
this.options = new ArrayList<Option>();
this.options.add(option);
}
public Options(Option option, Options rest) {
this.options = new ArrayList<Option>();
this.options.add(option);
this.options.addAll(rest.getList());
}
@Override
public List<Option> getList() {
return options;
}
@Override
public String toString() {
String re = "";
for (Option o : options) re = re + o.toString() + "\n";
return re;
}
@Override
public void substitude(String oldVar, Variable newVar) {
for(Option a : options) a.substitude(oldVar, newVar);
}
}

View File

@ -0,0 +1,21 @@
/*
* BSD License
*
* Open Source Fixedpoint Model-Checker Graphical User Interface version 2019
*
* (C) Copyright <EFBFBD>lfur J<EFBFBD>hann Edvardsson 2019
* (C) Copyright Veronica Julie Lodskov Hoffmann 2019
*
* All Rights Reserved.
*
*/
package Model.Parser;
import java.util.List;
public abstract class OptionsAB extends AST{
public abstract List<Option> getList();
}

View File

@ -0,0 +1,19 @@
/*
* BSD License
*
* Open Source Fixedpoint Model-Checker Graphical User Interface version 2019
*
* (C) Copyright <EFBFBD>lfur J<EFBFBD>hann Edvardsson 2019
* (C) Copyright Veronica Julie Lodskov Hoffmann 2019
*
* All Rights Reserved.
*
*/
package Model.Parser;
public abstract class OptionsABsub extends OptionsAB{
public abstract void substitude(String oldVar, Variable newVar);
}

View File

@ -0,0 +1,19 @@
/*
* BSD License
*
* Open Source Fixedpoint Model-Checker Graphical User Interface version 2019
*
* (C) Copyright <EFBFBD>lfur J<EFBFBD>hann Edvardsson 2019
* (C) Copyright Veronica Julie Lodskov Hoffmann 2019
*
* All Rights Reserved.
*
*/
package Model.Parser;
public abstract class OptionsSingleABsub extends OptionSingleAB{
public abstract void substitude(String oldVar, Variable newVar);
}

View File

@ -0,0 +1,38 @@
/*
* BSD License
*
* Open Source Fixedpoint Model-Checker Graphical User Interface version 2019
*
* (C) Copyright <EFBFBD>lfur J<EFBFBD>hann Edvardsson 2019
* (C) Copyright Veronica Julie Lodskov Hoffmann 2019
*
* All Rights Reserved.
*
*/
package Model.Parser;
public class Parenth extends OneVar {
private Message m;
public Parenth (AST message) {
this.m = (Message) message;
}
@Override
public AST getV1() {
return m;
}
@Override
public void substitude(String oldVar, Variable newVar) {
m.substitude(oldVar, newVar);
}
@Override
public String toString() {
return "(" + m.toString() + ")";
}
}

View File

@ -0,0 +1,57 @@
grammar Protocol;
/*
* Parser Rules
*/
pc : line+ EOF;
line : KW COLON assignment
| assignment
| WS
;
assignment : (TYPE cs)+(SEMI line)*
| var = VAR+(line)*
| (VAR COLON cs)+(SEMI line)*
| (VAR (STAR)* ARROW (STAR)* VAR COLON cs)
| VAR ('weakly')* 'authenticates' VAR 'on' VAR (line)*
| VAR 'secret' 'between' cs
| 'where' VAR NEQ VAR
;
cs : ('{|' VAR '|}')*(VAR | VAR '(' cs ')' )+(',' ('{|' cs '|}')*(VAR | VAR '(' cs ')'))*(line)*
;
/*
* Lexer Rules
*/
KW : ([Pp][Rr][Oo][Tt][Oo][Cc][Oo][Ll]|[Tt][Yy][Pp][Ee][Ss]|[Kk][Nn][Oo][Ww][Ll][Ee][Dd][Gg][Ee]|[Aa][Cc][Tt][Ii][Oo][Nn][Ss]|[Gg][Oo][Aa][Ll][Ss])+;
TYPE : ([Aa][Gg][Ee][Nn][Tt]|[Nn][Uu][Mm][Bb][Ee][Rr]|[Ff][Uu][Nn][Cc][Tt][Ii][Oo][Nn]|[Ss][Yy][Mm][Mm][Ee][Tt][Rr][Ii][Cc][_][Kk][Ee][Yy])+;
COLON: ':';
fragment COMMA: ',';
EQ: '=';
fragment DASH: '-';
STAR: '*';
NEQ: '!=';
SEMI: ';';
HASH: '#';
ARROW: '->';
VAR : [a-zA-Z]+[0-9a-zA-Z]*;
NUM : ('0'..'9')+ ( '.' ('0'..'9')+)? ('E' ('+'|'-')? ('0'..'9')+ )? ;
COMMENT: '#' ~[\r\n]* -> skip;
WS: [ \t\r\n]+ -> skip ;

View File

@ -0,0 +1,19 @@
/*
* BSD License
*
* Open Source Fixedpoint Model-Checker Graphical User Interface version 2019
*
* (C) Copyright <EFBFBD>lfur J<EFBFBD>hann Edvardsson 2019
* (C) Copyright Veronica Julie Lodskov Hoffmann 2019
*
* All Rights Reserved.
*
*/
package Model.Parser;
public abstract class Protocol extends AST {
}

View File

@ -0,0 +1,28 @@
/*
* BSD License
*
* Open Source Fixedpoint Model-Checker Graphical User Interface version 2019
*
* (C) Copyright <EFBFBD>lfur J<EFBFBD>hann Edvardsson 2019
* (C) Copyright Veronica Julie Lodskov Hoffmann 2019
*
* All Rights Reserved.
*
*/
package Model.Parser;
public class ProtocolKeeper extends Keepers{
private Name kept;
private Variable title;
public ProtocolKeeper(Variable title, Name toKeep) {
this.title = title;
this.kept = toKeep;
}
@Override
public String toString() {
return title.toString() + ": " + kept.toString() + "\n\n";
}
}

View File

@ -0,0 +1,319 @@
/*
* BSD License
*
* Open Source Fixedpoint Model-Checker Graphical User Interface version 2019
*
* (C) Copyright <EFBFBD>lfur J<EFBFBD>hann Edvardsson 2019
* (C) Copyright Veronica Julie Lodskov Hoffmann 2019
*
* All Rights Reserved.
*
*/
package Model.Parser;
import org.antlr.v4.runtime.BailErrorStrategy;
import org.antlr.v4.runtime.CharStream;
import org.antlr.v4.runtime.CharStreams;
import org.antlr.v4.runtime.CommonTokenStream;
public class ProtocolParser {
public ProtocolParser() {}
public AST run(String t) throws Exception {
// Translate the input string into stream of characters
CharStream inputStream = CharStreams.fromString(t);
// Create a lexer for the CharStream
pparserLexer lex = new pparserLexer(inputStream);
// Use the lexer to generate the token stream
CommonTokenStream tokens = new CommonTokenStream(lex);
// Create a parser for the given token stream and start it
try {
// Instantiate an evaluator
Evaluator evaluator = new Evaluator();
pparserParser parser = new pparserParser(tokens);
parser.setErrorHandler(new BailErrorStrategy());
return evaluator.visit(parser.start());
} catch (Exception e){
System.out.println("");
}
return null;
}
class Evaluator extends pparserBaseVisitor<AST> {
Evaluator() {}
@Override
public AST visitStart (pparserParser.StartContext ctx) {
Keeper keep = new Keeper();
for (int i = 0; i<ctx.begin().size(); i++) {
keep.keep(this.visit(ctx.begin(i)));
}
return keep;
}
@Override
public AST visitFunProtocol(pparserParser.FunProtocolContext ctx) {
return new ProtocolKeeper(new Variable(ctx.title.getText()), new Name(new Variable(ctx.n.getText())));
}
@Override
public AST visitFunTypes(pparserParser.FunTypesContext ctx) {
return new TypesKeeper(new Variable(ctx.title.getText()),(Types)visit(ctx.fun));
}
@Override
public AST visitFunKnowledge(pparserParser.FunKnowledgeContext ctx) {
return new KnowledgeKeeper(new Variable(ctx.title.getText()),(KnowledgeAb)visit(ctx.fun));
}
@Override
public AST visitFunActions(pparserParser.FunActionsContext ctx) {
return new ActionKeeper(new Variable(ctx.title.getText()),(Actions)visit(ctx.fun));
}
@Override
public AST visitFunGoals(pparserParser.FunGoalsContext ctx) {
return new GoalsKeeper(new Variable(ctx.title.getText()),(Goals)visit(ctx.fun));
}
@Override
public AST visitFunBrainWhere (pparserParser.FunBrainWhereContext ctx) {
KnowledgeAb m = (KnowledgeAb) visit(ctx.b);
m.register(new Where(visit(ctx.wa)));
return m;
}
@Override
public AST visitFunBrain (pparserParser.FunBrainContext ctx) {
return visit(ctx.b);
}
@Override
public AST visitBrainWithSemi(pparserParser.BrainWithSemiContext ctx) {
Knowledge all = new Knowledge(ctx.ag.getText(), visit(ctx.knows));
all.combine(((KnowledgeAb)visit(ctx.fun)).getList());
return all;
}
@Override
public AST visitBrainOptSemi(pparserParser.BrainOptSemiContext ctx) {
return new Knowledge(ctx.ag.getText(), visit(ctx.knows));
}
@Override
public AST visitNotlastAct (pparserParser.NotlastActContext ctx) {
return new Action(new Action(visit(ctx.mes), visit(ctx.fun),1), (Action)visit(ctx.fun2));
}
@Override
public AST visitLastAct (pparserParser.LastActContext ctx) {
return new Action(visit(ctx.mes),visit(ctx.fun),1);
}
@Override
public AST visitFunFromTo (pparserParser.FunFromToContext ctx) {
return new FromTo(visit(ctx.from), visit(ctx.arrow), visit(ctx.to));
}
@Override
public AST visitRegular (pparserParser.RegularContext ctx) {
return new Variable("->");
}
@Override
public AST visitStar (pparserParser.StarContext ctx) {
return new Variable("*->");
}
@Override
public AST visitArrowstar (pparserParser.ArrowstarContext ctx) {
return new Variable("->*");
}
@Override
public AST visitStararrowstar (pparserParser.StararrowstarContext ctx) {
return new Variable("*->*");
}
@Override
public AST visitNormal (pparserParser.NormalContext ctx) {
return new Variable(ctx.v.getText());
}
@Override
public AST visitSquare (pparserParser.SquareContext ctx) {
return new VarSquare(new Variable(ctx.v.getText()));
}
@Override
public AST visitSquaremess (pparserParser.SquaremessContext ctx) {
return new VarSqMess(new Variable(ctx.v.getText()), visit(ctx.mes));
}
@Override
public AST visitWscomma (pparserParser.WscommaContext ctx) {
return new Ws(visit(ctx.w1), visit(ctx.ws1), true);
}
@Override
public AST visitWsnocomma (pparserParser.WsnocommaContext ctx) {
return new Ws(visit(ctx.w1), null, false);
}
@Override
public AST visitWaisingle (pparserParser.WaisingleContext ctx) {
return new NotEQ(visit(ctx.mes1), visit(ctx.mes2), null, false);
}
@Override
public AST visitWaimore (pparserParser.WaimoreContext ctx) {
return new NotEQ(visit(ctx.mes1), visit(ctx.mes2), visit(ctx.wa), true);
}
@Override
public AST visitMcomma (pparserParser.McommaContext ctx) {
return new AList(visit(ctx.mes1), visit(ctx.mes2));
}
@Override
public AST visitMnocomma (pparserParser.MnocommaContext ctx) {
return visit(ctx.n);
}
@Override
public AST visitNormfunction (pparserParser.NormfunctionContext ctx) {
return new Function(new Variable(ctx.v.getText()), visit(ctx.l));
}
@Override
public AST visitNormnoenc (pparserParser.NormnoencContext ctx) {
return new NoEnc(visit(ctx.mes), visit(ctx.n));
}
@Override
public AST visitNormenc (pparserParser.NormencContext ctx) {
return new SymEnc(visit(ctx.mes), visit(ctx.n));
}
@Override
public AST visitNormvariable (pparserParser.NormvariableContext ctx) {
return new Variable(ctx.v.getText());
}
@Override
public AST visitNormparenth (pparserParser.NormparenthContext ctx) {
return new Function(new Variable(""), visit(ctx.mes));
}
@Override
public AST visitLimore(pparserParser.LimoreContext ctx) {
return new AList(visit(ctx.no), visit(ctx.l));
}
@Override
public AST visitLisingle(pparserParser.LisingleContext ctx) {
return visit(ctx.no);
}
@Override
public AST visitGoalsmore (pparserParser.GoalsmoreContext ctx) {
return new Goal((Goals)visit(ctx.fun1), (Goals)visit(ctx.fun2));
}
@Override
public AST visitGoalssingle (pparserParser.GoalssingleContext ctx) {
return new Goal((Goals)visit(ctx.fun));
}
@Override
public AST visitSecretbetween (pparserParser.SecretbetweenContext ctx) {
return new Secret((Message) visit(ctx.mes), (Ws) visit(ctx.fun));
}
@Override
public AST visitWeaklyauthent (pparserParser.WeaklyauthentContext ctx) {
return new Authenticates((Message) visit(ctx.fun1), (Message)visit(ctx.fun2), (Message)visit(ctx.mes), "weakly");
}
@Override
public AST visitAuthent (pparserParser.AuthentContext ctx) {
return new Authenticates((Message) visit(ctx.fun1), (Message)visit(ctx.fun2), (Message)visit(ctx.mes), "");
}
@Override
public AST visitArrowmsg (pparserParser.ArrowmsgContext ctx) {
return new ArrowGoal((Message)visit(ctx.fun), (Message)visit(ctx.mes));
}
@Override
public AST visitTypesoptsemi(pparserParser.TypesoptsemiContext ctx) {
return new Type((Variable)visit(ctx.type), visit(ctx.cs));
}
@Override
public AST visitTypesemi(pparserParser.TypesemiContext ctx) {
return new Type(visit(ctx.type), visit(ctx.cs), (Types)visit(ctx.fun));
}
@Override
public AST visitCsepsingle(pparserParser.CsepsingleContext ctx) {
return new Variable(ctx.v.getText());
}
@Override
public AST visitCsepmore(pparserParser.CsepmoreContext ctx) {
return new AList(new Variable(ctx.v.getText()), visit(ctx.fun));
}
@Override
public AST visitAg(pparserParser.AgContext ctx) {
return new Variable(ctx.t.getText());
}
@Override
public AST visitNu(pparserParser.NuContext ctx) {
return new Variable(ctx.t.getText());
}
@Override
public AST visitSeq(pparserParser.SeqContext ctx) {
return new Variable(ctx.t.getText());
}
@Override
public AST visitPk(pparserParser.PkContext ctx) {
return new Variable(ctx.t.getText());
}
@Override
public AST visitSymk(pparserParser.SymkContext ctx) {
return new Variable(ctx.t.getText());
}
@Override
public AST visitFunc(pparserParser.FuncContext ctx) {
return new Variable(ctx.t.getText());
}
@Override
public AST visitUnt(pparserParser.UntContext ctx) {
return new Variable(ctx.t.getText());
}
}
}

View File

@ -0,0 +1,29 @@
/*
* BSD License
*
* Open Source Fixedpoint Model-Checker Graphical User Interface version 2019
*
* (C) Copyright <EFBFBD>lfur J<EFBFBD>hann Edvardsson 2019
* (C) Copyright Veronica Julie Lodskov Hoffmann 2019
*
* All Rights Reserved.
*
*/
package Model.Parser;
public class Secret extends Goals {
private Message m;
private Ws w;
public Secret (Message m, Ws w) {
this.m = m;
this.w = w;
}
@Override
public String toString() {
return m.toString() + " secret between " + w.toString();
}
}

View File

@ -0,0 +1,49 @@
/*
* BSD License
*
* Open Source Fixedpoint Model-Checker Graphical User Interface version 2019
*
* (C) Copyright <EFBFBD>lfur J<EFBFBD>hann Edvardsson 2019
* (C) Copyright Veronica Julie Lodskov Hoffmann 2019
*
* All Rights Reserved.
*
*/
package Model.Parser;
import java.util.ArrayList;
import java.util.List;
public class Stat extends Stats {
private Variable type, num, var;
private boolean colon;
private List<Stats> stats;
public Stat(Variable type, Variable num, Variable var, boolean b) {
this.type = type;
this.num = num;
this.var = var;
this.colon = b;
this.stats = new ArrayList<Stats>();
this.stats.add(this);
}
public Stat(Variable type, Variable num, Variable var, boolean b, Stat stat) {
this.stats = new ArrayList<Stats>();
this.stats.add(new Stat(type, num, var, b));
this.stats.addAll(stat.getList());
}
@Override
public String toString() {
if (colon) return this.type.toString() + ": " + this.num.toString() + " " + this.var.toString();
else return this.type.toString() + " " + this.num.toString() + " " + this.var.toString();
}
@Override
public List<Stats> getList() {
return this.stats;
}
}

View File

@ -0,0 +1,30 @@
/*
* BSD License
*
* Open Source Fixedpoint Model-Checker Graphical User Interface version 2019
*
* (C) Copyright <EFBFBD>lfur J<EFBFBD>hann Edvardsson 2019
* (C) Copyright Veronica Julie Lodskov Hoffmann 2019
*
* All Rights Reserved.
*
*/
package Model.Parser;
public class StatKeeper extends Keepers {
private AST title;
private Stats stats;
public StatKeeper (AST title, Stats stats) {
this.title = title;
this.stats = stats;
}
@Override
public String toString() {
String r = title.toString() + ":\n";
for(Stats s : stats.getList()) r = r + s.toString() + "\n";
return r;
}
}

View File

@ -0,0 +1,30 @@
/*
* BSD License
*
* Open Source Fixedpoint Model-Checker Graphical User Interface version 2019
*
* (C) Copyright <EFBFBD>lfur J<EFBFBD>hann Edvardsson 2019
* (C) Copyright Veronica Julie Lodskov Hoffmann 2019
*
* All Rights Reserved.
*
*/
package Model.Parser;
public class States extends Extra {
private AST m,rest;
public States(AST m , AST rest) {
this.m = m;
this.rest = rest;
}
@Override
public String toString() {
if(this.rest != null) return "state_" + m.toString() + "\n" + rest.toString();
return "state_" + m.toString() + "\n";
}
}

View File

@ -0,0 +1,20 @@
/*
* BSD License
*
* Open Source Fixedpoint Model-Checker Graphical User Interface version 2019
*
* (C) Copyright <EFBFBD>lfur J<EFBFBD>hann Edvardsson 2019
* (C) Copyright Veronica Julie Lodskov Hoffmann 2019
*
* All Rights Reserved.
*
*/
package Model.Parser;
import java.util.List;
public abstract class Stats extends AST {
public abstract List<Stats> getList();
}

View File

@ -0,0 +1,19 @@
/*
* BSD License
*
* Open Source Fixedpoint Model-Checker Graphical User Interface version 2019
*
* (C) Copyright <EFBFBD>lfur J<EFBFBD>hann Edvardsson 2019
* (C) Copyright Veronica Julie Lodskov Hoffmann 2019
*
* All Rights Reserved.
*
*/
package Model.Parser;
public abstract class StepProvider extends OneVar{
public abstract Integer getStepNo();
}

View File

@ -0,0 +1,39 @@
/*
* BSD License
*
* Open Source Fixedpoint Model-Checker Graphical User Interface version 2019
*
* (C) Copyright <EFBFBD>lfur J<EFBFBD>hann Edvardsson 2019
* (C) Copyright Veronica Julie Lodskov Hoffmann 2019
*
* All Rights Reserved.
*
*/
package Model.Parser;
import java.util.ArrayList;
import java.util.List;
public class SummaryKeeper extends KeepersWithLists {
private AST t, fun;
public SummaryKeeper(AST t, AST fun) {
this.t = t;
this.fun = fun;
}
@Override
public String toString() {
return this.t.toString() + ":\n" + fun.toString() + "\n";
}
@Override
public List<AST> getList() {
List<AST> list = new ArrayList<AST>();
list.add(fun);
return list;
}
}

View File

@ -0,0 +1,45 @@
/*
* BSD License
*
* Open Source Fixedpoint Model-Checker Graphical User Interface version 2019
*
* (C) Copyright <EFBFBD>lfur J<EFBFBD>hann Edvardsson 2019
* (C) Copyright Veronica Julie Lodskov Hoffmann 2019
*
* All Rights Reserved.
*
*/
package Model.Parser;
public class SymEnc extends TwoVar{
private Message msg, norm;
public SymEnc (AST msg, AST norm) {
this.msg = (Message) msg;
this.norm = (Message) norm;
}
@Override
public String toString() {
return "{|" + msg.toString() + "|}" + norm.toString();
}
@Override
public Message getV1() {
return msg;
}
@Override
public Message getV2() {
return norm;
}
@Override
public void substitude(String oldVar, Variable newVar) {
msg.substitude(oldVar, newVar);
norm.substitude(oldVar, newVar);
}
}

View File

@ -0,0 +1,31 @@
/*
* BSD License
*
* Open Source Fixedpoint Model-Checker Graphical User Interface version 2019
*
* (C) Copyright <EFBFBD>lfur J<EFBFBD>hann Edvardsson 2019
* (C) Copyright Veronica Julie Lodskov Hoffmann 2019
*
* All Rights Reserved.
*
*/
package Model.Parser;
public class TextKeeper extends Keepers {
private AST t, fun, t2;
public TextKeeper(AST t, AST t2, AST fun) {
this.t = t;
this.fun = fun;
this.t2 = t2;
}
@Override
public String toString() {
if(t.toString().equals("where")) return fun.toString() + "\n";
if(t2 != null) return this.t.toString() + ":\n" + t2.toString() + " "+ fun.toString() + "\n";
return this.t.toString() + ":\n" + fun.toString() + "\n";
}
}

View File

@ -0,0 +1,22 @@
/*
* BSD License
*
* Open Source Fixedpoint Model-Checker Graphical User Interface version 2019
*
* (C) Copyright <EFBFBD>lfur J<EFBFBD>hann Edvardsson 2019
* (C) Copyright Veronica Julie Lodskov Hoffmann 2019
*
* All Rights Reserved.
*
*/
package Model.Parser;
public abstract class ThreeVar extends Message{
public abstract Message getV1();
public abstract Message getV2();
public abstract Message getV3();
}

View File

@ -0,0 +1,45 @@
/*
* BSD License
*
* Open Source Fixedpoint Model-Checker Graphical User Interface version 2019
*
* (C) Copyright <EFBFBD>lfur J<EFBFBD>hann Edvardsson 2019
* (C) Copyright Veronica Julie Lodskov Hoffmann 2019
*
* All Rights Reserved.
*
*/
package Model.Parser;
import java.util.ArrayList;
import java.util.List;
public class Trace extends TracingAB {
private List<Actions> trace;
public Trace (Action a, Trace rest) {
this.trace = new ArrayList<Actions>();
this.trace.add(a);
this.trace.addAll(rest.getList());
}
public Trace (Action a) {
this.trace = new ArrayList<Actions>();
this.trace.add(a);
}
@Override
public List<Actions> getList() {
return this.trace;
}
@Override
public String toString() {
String re = "";
for(Actions t : trace) {
re = re + t.toString() + "\n";
}
return re;
}
}

View File

@ -0,0 +1,39 @@
/*
* BSD License
*
* Open Source Fixedpoint Model-Checker Graphical User Interface version 2019
*
* (C) Copyright <EFBFBD>lfur J<EFBFBD>hann Edvardsson 2019
* (C) Copyright Veronica Julie Lodskov Hoffmann 2019
*
* All Rights Reserved.
*
*/
package Model.Parser;
import java.util.ArrayList;
import java.util.List;
public class TraceKeeper extends KeepersWithLists {
private Trace trace;
private Variable title;
public TraceKeeper(Variable title, Trace trace) {
this.title = title;
this.trace = trace;
}
@Override
public String toString() {
return this.title.toString() + ":\n" + this.trace.toString();
}
@Override
public List<AST> getList() {
List<AST> re = new ArrayList<AST>();
for(Actions a : this.trace.getList()) re.add(a);
return re;
}
}

View File

@ -0,0 +1,419 @@
/*
* BSD License
*
* Open Source Fixedpoint Model-Checker Graphical User Interface version 2019
*
* (C) Copyright <EFBFBD>lfur J<EFBFBD>hann Edvardsson 2019
* (C) Copyright Veronica Julie Lodskov Hoffmann 2019
*
* All Rights Reserved.
*
*/
package Model.Parser;
import java.util.ArrayList;
import java.util.List;
import org.antlr.v4.runtime.BailErrorStrategy;
import org.antlr.v4.runtime.CharStream;
import org.antlr.v4.runtime.CharStreams;
import org.antlr.v4.runtime.CommonTokenStream;
public class TraceParser {
public AST run(String input) throws Exception {
// Translate the input string into stream of characters
CharStream inputStream = CharStreams.fromString(input);
// Create a lexer for the CharStream
tparserLexer lex = new tparserLexer(inputStream);
// Use the lexer to generate the token stream
CommonTokenStream tokens = new CommonTokenStream(lex);
// Create a parser for the given token stream and start it
try {
// Instantiate an evaluator
Evaluator evaluator = new Evaluator();
tparserParser parser = new tparserParser(tokens);
parser.setErrorHandler(new BailErrorStrategy());
return evaluator.visit(parser.start());
} catch (Exception e){
}
return null;
}
class Evaluator extends tparserBaseVisitor<AST> {
Evaluator() {
}
@Override
public AST visitStart (tparserParser.StartContext ctx) {
Keeper keep = new Keeper();
for (int i = 0; i<ctx.begin().size(); i++) {
keep.keep(this.visit(ctx.begin(i)));
}
return keep;
}
@Override
public AST visitFunVer (tparserParser.FunVerContext ctx) {
return new TextKeeper(new Variable(ctx.t.getText()), null, visit(ctx.fun));
}
@Override
public AST visitFunSum (tparserParser.FunSumContext ctx) {
return new TextKeeper(new Variable(ctx.t.getText()), null, visit(ctx.sum));
}
@Override
public AST visitFunVer2 (tparserParser.FunVer2Context ctx) {
return new TextKeeper(new Variable(ctx.t.getText()), new Variable(ctx.t2.getText()), visit(ctx.fun));
}
@Override
public AST visitFunCom (tparserParser.FunComContext ctx) {
return new TextKeeper(new Variable(ctx.t.getText() + ": state"), null, visit(ctx.fun));
}
@Override
public AST visitFunPost (tparserParser.FunPostContext ctx) {
return new TextKeeper(new Variable(ctx.t.getText()), null, visit(ctx.fun));
}
@Override
public AST visitFunIk (tparserParser.FunIkContext ctx) {
return new TextKeeper(new Variable(ctx.t.getText()), null, visit(ctx.fun));
}
@Override
public AST visitFunCon (tparserParser.FunConContext ctx) {
return new TextKeeper(new Variable(ctx.t.getText()), null, visit(ctx.fun));
}
@Override
public AST visitFunWhere (tparserParser.FunWhereContext ctx) {
return new TextKeeper(new Variable(ctx.t.getText()), null, visit(ctx.fun));
}
@Override
public AST visitFunHistory (tparserParser.FunHistoryContext ctx) {
return new HistoryKeeper(new Variable(""), (History)visit(ctx.fun));
}
@Override
public AST visitFunOp (tparserParser.FunOpContext ctx) {
return visit(ctx.fun);
}
@Override
public AST visitOpMore (tparserParser.OpMoreContext ctx) {
List<Actions> acts = new ArrayList<Actions>();
for (int i = 0; i<ctx.act().size(); i++) acts.add((Actions) visit(ctx.act(i)));
return new Options((Option)new Option(new Variable(ctx.n.getText()), acts), (Options) visit(ctx.fun2));
}
@Override
public AST visitOpLast (tparserParser.OpLastContext ctx) {
List<Actions> acts = new ArrayList<Actions>();
for (int i = 0; i<ctx.act().size(); i++) acts.add((Actions) visit(ctx.act(i)));
return new Options(new Option(new Variable(ctx.n.getText()), acts));
}
@Override
public AST visitHistMore (tparserParser.HistMoreContext ctx) {
return new History((Action)visit(ctx.fun), (History)visit(ctx.fun2));
}
@Override
public AST visitHistLast (tparserParser.HistLastContext ctx) {
return new History((Action)visit(ctx.fun));
}
@Override
public AST visitWheMore (tparserParser.WheMoreContext ctx) {
List<Variable> list = new ArrayList<Variable>();
for(int i=0; i<ctx.wheSym().size(); i++) list.add((Variable) visit(ctx.wheSym(i)));
return new WheColl(new WhePar(list), (Variable)visit(ctx.fun2), (WheColl)visit(ctx.fun3));
}
@Override
public AST visitWhePar (tparserParser.WheParContext ctx) {
List<Variable> list = new ArrayList<Variable>();
for(int i=0; i<ctx.wheSym().size(); i++) list.add((Variable) visit(ctx.wheSym(i)));
return new WheColl(new WhePar(list));
}
@Override
public AST visitWheLast (tparserParser.WheLastContext ctx) {
return new WheColl((Variable)visit(ctx.fun));
}
@Override
public AST visitSymT (tparserParser.SymTContext ctx) {
return new Variable("True");
}
@Override
public AST visitSymF (tparserParser.SymFContext ctx) {
return new Variable("False");
}
@Override
public AST visitSymV (tparserParser.SymVContext ctx) {
return new Variable(ctx.v.getText());
}
@Override
public AST visitSymS (tparserParser.SymSContext ctx) {
return new Variable(ctx.v.getText());
}
@Override
public AST visitSymE (tparserParser.SymEContext ctx) {
return new Variable(ctx.v.getText());
}
@Override
public AST visitSymA (tparserParser.SymAContext ctx) {
return new Variable(" and ");
}
@Override
public AST visitSymO (tparserParser.SymOContext ctx) {
return new Variable(" or ");
}
@Override
public AST visitConMore (tparserParser.ConMoreContext ctx) {
return new Constraints(visit(ctx.mes), visit(ctx.fun));
}
@Override
public AST visitConLast (tparserParser.ConLastContext ctx) {
return new Constraints(visit(ctx.mes), null);
}
@Override
public AST visitIkMore (tparserParser.IkMoreContext ctx) {
return new Constraints(visit(ctx.mes), visit(ctx.fun));
}
@Override
public AST visitIkLast (tparserParser.IkLastContext ctx) {
return new Constraints(visit(ctx.mes), null);
}
@Override
public AST visitPostM (tparserParser.PostMContext ctx) {
if (ctx.mes == null ) return new Variable("");
return new Constraints(visit(ctx.mes), null);
}
@Override
public AST visitComMore (tparserParser.ComMoreContext ctx) {
return new States(visit(ctx.mes), visit(ctx.fun));
}
@Override
public AST visitComLast (tparserParser.ComLastContext ctx) {
return new States(visit(ctx.mes), null);
}
@Override
public AST visitNameDot (tparserParser.NameDotContext ctx) {
return new Dot((Variable)visit(ctx.fun1), (Variable)visit(ctx.fun2));
}
@Override
public AST visitNameV (tparserParser.NameVContext ctx) {
return new Variable(ctx.v.getText());
}
@Override
public AST visitNameN (tparserParser.NameNContext ctx) {
return new Variable(ctx.n.getText());
}
@Override
public AST visitNameF (tparserParser.NameFContext ctx) {
return new Variable(ctx.v.getText());
}
@Override
public AST visitAAct (tparserParser.AActContext ctx) {
return new Action(visit(ctx.mes), visit(ctx.fun), 1);
}
@Override
public AST visitFromTo (tparserParser.FromToContext ctx) {
return new FromTo(visit(ctx.from), visit(ctx.arrow), visit(ctx.to));
}
@Override
public AST visitRegular (tparserParser.RegularContext ctx) {
return new Variable("->");
}
@Override
public AST visitStar (tparserParser.StarContext ctx) {
return new Variable("*->");
}
@Override
public AST visitArrowstar (tparserParser.ArrowstarContext ctx) {
return new Variable("->*");
}
@Override
public AST visitStararrowstar (tparserParser.StararrowstarContext ctx) {
return new Variable("*->*");
}
@Override
public AST visitWVar (tparserParser.WVarContext ctx) {
return new Variable(ctx.v.getText());
}
@Override
public AST visitWNum (tparserParser.WNumContext ctx) {
return new Variable(ctx.n.getText());
}
@Override
public AST visitWComma (tparserParser.WCommaContext ctx) {
return new Wcomma(visit(ctx.fun1), visit(ctx.fun2));
}
@Override
public AST visitMcomma (tparserParser.McommaContext ctx) {
return new AList(visit(ctx.mes1), visit(ctx.mes2));
}
@Override
public AST visitMnocomma (tparserParser.MnocommaContext ctx) {
return visit(ctx.n);
}
@Override
public AST visitNormfunction (tparserParser.NormfunctionContext ctx) {
return new Function(new Variable(ctx.v.getText()), visit(ctx.l));
}
@Override
public AST visitNormnoenc (tparserParser.NormnoencContext ctx) {
return new NoEnc(visit(ctx.mes), visit(ctx.n));
}
@Override
public AST visitNormenc (tparserParser.NormencContext ctx) {
return new SymEnc(visit(ctx.mes), visit(ctx.n));
}
@Override
public AST visitNormvariable (tparserParser.NormvariableContext ctx) {
return new Variable(ctx.getText());
}
@Override
public AST visitNormnum (tparserParser.NormnumContext ctx) {
return new Variable(ctx.getText());
}
@Override
public AST visitNormMore (tparserParser.NormMoreContext ctx) {
return new NormMore(visit(ctx.n));
}
@Override
public AST visitNormUnder (tparserParser.NormUnderContext ctx) {
return new Variable("_");
}
@Override
public AST visitNormparenth (tparserParser.NormparenthContext ctx) {
return new Parenth(visit(ctx.mes));
}
@Override
public AST visitNormcmes (tparserParser.NormcmesContext ctx) {
return new NormSq(visit(ctx.mes), true);
}
@Override
public AST visitNormmes (tparserParser.NormmesContext ctx) {
return new NormSq(visit(ctx.mes), false);
}
@Override
public AST visitNormcsq (tparserParser.NormcsqContext ctx) {
return new NormSq(new Variable(""), true);
}
@Override
public AST visitNormsq (tparserParser.NormsqContext ctx) {
return new NormSq(new Variable(""), false);
}
@Override
public AST visitNormempty (tparserParser.NormemptyContext ctx) {
return new Variable("{}");
}
@Override
public AST visitLimore(tparserParser.LimoreContext ctx) {
return new AList(visit(ctx.no), visit(ctx.l));
}
@Override
public AST visitLisingle(tparserParser.LisingleContext ctx) {
return visit(ctx.no);
}
@Override
public AST visitFVer (tparserParser.FVerContext ctx) {
return new Variable(ctx.n.getText());
}
@Override
public AST visitTexU (tparserParser.TexUContext ctx) {
return new UnderSep((Variable)visit(ctx.fun), (Variable)visit(ctx.fun2));
}
@Override
public AST visitTexA (tparserParser.TexAContext ctx) {
return new Variable(ctx.v.getText());
}
@Override
public AST visitTexN (tparserParser.TexNContext ctx) {
return new Variable(ctx.v.getText());
}
@Override
public AST visitTexF (tparserParser.TexFContext ctx) {
return new Variable(ctx.v.getText());
}
@Override
public AST visitTexMore (tparserParser.TexMoreContext ctx) {
return new Variable(ctx.v.getText());
}
@Override
public AST visitTexV (tparserParser.TexVContext ctx) {
return new Variable(ctx.v.getText());
}
}
}

View File

@ -0,0 +1,21 @@
/*
* BSD License
*
* Open Source Fixedpoint Model-Checker Graphical User Interface version 2019
*
* (C) Copyright <EFBFBD>lfur J<EFBFBD>hann Edvardsson 2019
* (C) Copyright Veronica Julie Lodskov Hoffmann 2019
*
* All Rights Reserved.
*
*/
package Model.Parser;
import java.util.List;
public abstract class TracingAB extends AST{
public abstract List<Actions> getList();
}

View File

@ -0,0 +1,19 @@
/*
* BSD License
*
* Open Source Fixedpoint Model-Checker Graphical User Interface version 2019
*
* (C) Copyright <EFBFBD>lfur J<EFBFBD>hann Edvardsson 2019
* (C) Copyright Veronica Julie Lodskov Hoffmann 2019
*
* All Rights Reserved.
*
*/
package Model.Parser;
public abstract class TracingABsub extends TracingAB {
public abstract void substitude(String oldVar, Variable newVar);
}

View File

@ -0,0 +1,21 @@
/*
* BSD License
*
* Open Source Fixedpoint Model-Checker Graphical User Interface version 2019
*
* (C) Copyright <EFBFBD>lfur J<EFBFBD>hann Edvardsson 2019
* (C) Copyright Veronica Julie Lodskov Hoffmann 2019
*
* All Rights Reserved.
*
*/
package Model.Parser;
public abstract class TwoVar extends Message{
public abstract Message getV1();
public abstract Message getV2();
}

View File

@ -0,0 +1,18 @@
/*
* BSD License
*
* Open Source Fixedpoint Model-Checker Graphical User Interface version 2019
*
* (C) Copyright <EFBFBD>lfur J<EFBFBD>hann Edvardsson 2019
* (C) Copyright Veronica Julie Lodskov Hoffmann 2019
*
* All Rights Reserved.
*
*/
package Model.Parser;
public abstract class TwoVarStepProvider extends TwoVar{
public abstract Integer getStepNo();
}

View File

@ -0,0 +1,45 @@
/*
* BSD License
*
* Open Source Fixedpoint Model-Checker Graphical User Interface version 2019
*
* (C) Copyright <EFBFBD>lfur J<EFBFBD>hann Edvardsson 2019
* (C) Copyright Veronica Julie Lodskov Hoffmann 2019
*
* All Rights Reserved.
*
*/
package Model.Parser;
import java.util.ArrayList;
import java.util.List;
public class Type extends Types{
private Variable type;
private Message cs;
private List<Types> types;
public Type(AST type, AST cs) {
this.type = (Variable) type;
this.cs = (Message) cs;
this.types = new ArrayList<Types>();
this.types.add(this);
}
public Type(AST type, AST cs,Types t) {
this.types = new ArrayList<Types>();
this.types.add(new Type(type,cs));
this.types.addAll(t.getList());
}
@Override
public String toString() {
return this.type.toString() + " " + this.cs.toString() + ";";
}
@Override
public List<Types> getList() {
return this.types;
}
}

View File

@ -0,0 +1,20 @@
/*
* BSD License
*
* Open Source Fixedpoint Model-Checker Graphical User Interface version 2019
*
* (C) Copyright <EFBFBD>lfur J<EFBFBD>hann Edvardsson 2019
* (C) Copyright Veronica Julie Lodskov Hoffmann 2019
*
* All Rights Reserved.
*
*/
package Model.Parser;
import java.util.List;
public abstract class Types extends AST {
public abstract List<Types> getList();
}

View File

@ -0,0 +1,41 @@
/*
* BSD License
*
* Open Source Fixedpoint Model-Checker Graphical User Interface version 2019
*
* (C) Copyright <EFBFBD>lfur J<EFBFBD>hann Edvardsson 2019
* (C) Copyright Veronica Julie Lodskov Hoffmann 2019
*
* All Rights Reserved.
*
*/
package Model.Parser;
import java.util.ArrayList;
import java.util.List;
public class TypesKeeper extends KeepersWithLists {
private Variable title;
private List<Types> types;
public TypesKeeper(Variable title, Types t) {
this.title = title;
this.types = t.getList();
}
@Override
public String toString() {
String m = title.toString() + ":\n";
for (Types t : types) m = m + t.toString() + "\n";
m = m + "\n";
return m;
}
@Override
public List<AST> getList() {
List<AST> re = new ArrayList<AST>();
for(Types a : types) re.add(a);
return re;
}
}

View File

@ -0,0 +1,45 @@
/*
* BSD License
*
* Open Source Fixedpoint Model-Checker Graphical User Interface version 2019
*
* (C) Copyright <EFBFBD>lfur J<EFBFBD>hann Edvardsson 2019
* (C) Copyright Veronica Julie Lodskov Hoffmann 2019
*
* All Rights Reserved.
*
*/
package Model.Parser;
public class UnderSep extends TwoVar {
private Message v1,v2;
public UnderSep (AST v1, AST v2) {
this.v1 = (Message) v1;
this.v2 = (Message) v2;
}
@Override
public String toString() {
return this.v1.toString() + "_" + this.v2.toString();
}
@Override
public Message getV1() {
return v1;
}
@Override
public Message getV2() {
return v2;
}
@Override
public void substitude(String oldVar, Variable newVar) {
v1.substitude(oldVar, newVar);
v2.substitude(oldVar, newVar);
}
}

View File

@ -0,0 +1,48 @@
/*
* BSD License
*
* Open Source Fixedpoint Model-Checker Graphical User Interface version 2019
*
* (C) Copyright <EFBFBD>lfur J<EFBFBD>hann Edvardsson 2019
* (C) Copyright Veronica Julie Lodskov Hoffmann 2019
*
* All Rights Reserved.
*
*/
package Model.Parser;
public class VarSqMess extends TwoVar {
private Variable var;
private Message message;
public VarSqMess(Variable text, AST msg) {
this.var = text;
this.message = (Message) msg;
}
@Override
public String toString() {
return "[" + var.toString() + ": " + this.message.toString() + "]";
}
@Override
public Message getV1() {
return var;
}
@Override
public Message getV2() {
return message;
}
@Override
public void substitude(String oldVar, Variable newVar) {
this.var.substitude(oldVar, newVar);
this.message.substitude(oldVar, newVar);
}
}

View File

@ -0,0 +1,39 @@
/*
* BSD License
*
* Open Source Fixedpoint Model-Checker Graphical User Interface version 2019
*
* (C) Copyright <EFBFBD>lfur J<EFBFBD>hann Edvardsson 2019
* (C) Copyright Veronica Julie Lodskov Hoffmann 2019
*
* All Rights Reserved.
*
*/
package Model.Parser;
public class VarSquare extends OneVar{
private Variable var;
public VarSquare(Variable text) {
this.var = text;
}
@Override
public String toString() {
return "[" + this.var.toString() + "]";
}
@Override
public Message getV1() {
return var;
}
@Override
public void substitude(String oldVar, Variable newVar) {
this.var.substitude(oldVar, newVar);
}
}

View File

@ -0,0 +1,46 @@
/*
* BSD License
*
* Open Source Fixedpoint Model-Checker Graphical User Interface version 2019
*
* (C) Copyright <EFBFBD>lfur J<EFBFBD>hann Edvardsson 2019
* (C) Copyright Veronica Julie Lodskov Hoffmann 2019
*
* All Rights Reserved.
*
*/
package Model.Parser;
public class Variable extends StepProvider {
private String var;
public Variable (String text) {
this.var = text;
}
@Override
public String toString() {
return this.var;
}
@Override
public Variable getV1() {
return this;
}
@Override
public Integer getStepNo() {
String i = var.replaceAll("step", "");
int re = Integer.parseInt(i);
return re;
}
@Override
public void substitude(String oldVar, Variable newVar) {
if (this.var.equals(oldVar)) this.var = newVar.toString();
}
}

View File

@ -0,0 +1,44 @@
/*
* BSD License
*
* Open Source Fixedpoint Model-Checker Graphical User Interface version 2019
*
* (C) Copyright <EFBFBD>lfur J<EFBFBD>hann Edvardsson 2019
* (C) Copyright Veronica Julie Lodskov Hoffmann 2019
*
* All Rights Reserved.
*
*/
package Model.Parser;
public class Wcomma extends TwoVar {
private Variable w1,w2;
public Wcomma(AST w1, AST w2) {
this.w1 = (Variable) w1;
this.w2 = (Variable) w2;
}
@Override
public String toString() {
return "(" + w1.toString() + "," + w2.toString() + ")";
}
@Override
public Message getV1() {
return this.w1;
}
@Override
public Message getV2() {
return this.w2;
}
@Override
public void substitude(String oldVar, Variable newVar) {
w1.substitude(oldVar, newVar);
}
}

View File

@ -0,0 +1,50 @@
/*
* BSD License
*
* Open Source Fixedpoint Model-Checker Graphical User Interface version 2019
*
* (C) Copyright <EFBFBD>lfur J<EFBFBD>hann Edvardsson 2019
* (C) Copyright Veronica Julie Lodskov Hoffmann 2019
*
* All Rights Reserved.
*
*/
package Model.Parser;
import java.util.ArrayList;
import java.util.List;
public class WheColl extends WheSym {
private List<AST> whe;
public WheColl(WhePar w, Variable a, WheColl rest) {
this.whe = new ArrayList<AST>();
this.whe.add(w);
this.whe.add(a);
this.whe.addAll(rest.getList());
}
public WheColl(WhePar w) {
this.whe = new ArrayList<AST>();
this.whe.add(w);
}
public WheColl(Variable v) {
this.whe = new ArrayList<AST>();
this.whe.add(v);
}
@Override
public List<AST> getList() {
return whe;
}
@Override
public String toString() {
String re = "where ";
for (AST w : whe) re = re + w.toString();
return re;
}
}

View File

@ -0,0 +1,38 @@
/*
* BSD License
*
* Open Source Fixedpoint Model-Checker Graphical User Interface version 2019
*
* (C) Copyright <EFBFBD>lfur J<EFBFBD>hann Edvardsson 2019
* (C) Copyright Veronica Julie Lodskov Hoffmann 2019
*
* All Rights Reserved.
*
*/
package Model.Parser;
import java.util.ArrayList;
import java.util.List;
public class WhePar extends WheSym{
private List<Variable> sym;
public WhePar(List<Variable> sym) {
this.sym = sym;
}
@Override
public List<AST> getList() {
List<AST> re = new ArrayList<AST>();
for(Variable v : sym) re.add(v);
return re;
}
@Override
public String toString() {
String re = "";
for (Variable w : sym) re = re + w.toString();
return "(" + re + ")";
}
}

View File

@ -0,0 +1,19 @@
/*
* BSD License
*
* Open Source Fixedpoint Model-Checker Graphical User Interface version 2019
*
* (C) Copyright <EFBFBD>lfur J<EFBFBD>hann Edvardsson 2019
* (C) Copyright Veronica Julie Lodskov Hoffmann 2019
*
* All Rights Reserved.
*
*/
package Model.Parser;
import java.util.List;
public abstract class WheSym extends AST {
public abstract List<AST> getList();
}

View File

@ -0,0 +1,51 @@
/*
* BSD License
*
* Open Source Fixedpoint Model-Checker Graphical User Interface version 2019
*
* (C) Copyright <EFBFBD>lfur J<EFBFBD>hann Edvardsson 2019
* (C) Copyright Veronica Julie Lodskov Hoffmann 2019
*
* All Rights Reserved.
*
*/
package Model.Parser;
import java.util.ArrayList;
import java.util.List;
public class Where extends KnowledgeAb{
private AST where;
private List<KnowledgeAb> all;
public Where (AST w) {
this.where = w;
this.all = new ArrayList<KnowledgeAb>();
all.add(this);
}
@Override
public String toString() {
return "where " + where.toString();
}
@Override
public void register(KnowledgeAb a) {
}
@Override
public void combine(List<KnowledgeAb> visit) {
this.all.addAll(visit);
}
@Override
public List<KnowledgeAb> getList() {
return this.all;
}
@Override
public void addSteps(int i) {
}
}

49
src/Model/Parser/Ws.java Normal file
View File

@ -0,0 +1,49 @@
/*
* BSD License
*
* Open Source Fixedpoint Model-Checker Graphical User Interface version 2019
*
* (C) Copyright <EFBFBD>lfur J<EFBFBD>hann Edvardsson 2019
* (C) Copyright Veronica Julie Lodskov Hoffmann 2019
*
* All Rights Reserved.
*
*/
package Model.Parser;
public class Ws extends TwoVar{
private Message w, ws;
private boolean comma;
public Ws(AST w, AST ws, boolean b) {
this.w = (Message) w;
this.ws = (Message) ws;
this.comma = b;
}
@Override
public String toString() {
if (comma) return w.toString() + "," + ws.toString();
else return w.toString();
}
@Override
public Message getV1() {
return w;
}
@Override
public Message getV2() {
return ws;
}
@Override
public void substitude(String oldVar, Variable newVar) {
w.substitude(oldVar, newVar);
ws.substitude(oldVar, newVar);
}
}

View File

@ -0,0 +1,383 @@
/*
* BSD License
*
* Open Source Fixedpoint Model-Checker Graphical User Interface version 2019
*
* (C) Copyright <EFBFBD>lfur J<EFBFBD>hann Edvardsson 2019
* (C) Copyright Veronica Julie Lodskov Hoffmann 2019
*
* All Rights Reserved.
*
*/
package Model.Parser;
// Generated from aparser.g4 by ANTLR 4.7.1
import org.antlr.v4.runtime.tree.AbstractParseTreeVisitor;
/**
* This class provides an empty implementation of {@link aparserVisitor},
* which can be extended to create a visitor which only needs to handle a subset
* of the available methods.
*
* @param <T> The return type of the visit operation. Use {@link Void} for
* operations with no return type.
*/
public class aparserBaseVisitor<T> extends AbstractParseTreeVisitor<T> implements aparserVisitor<T> {
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitStart(aparserParser.StartContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitFunVer(aparserParser.FunVerContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitFunIn(aparserParser.FunInContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitFunSum(aparserParser.FunSumContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitFunGoal(aparserParser.FunGoalContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitFunDet(aparserParser.FunDetContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitFunBack(aparserParser.FunBackContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitFunStat(aparserParser.FunStatContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitFunTrace(aparserParser.FunTraceContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitNameV(aparserParser.NameVContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitNameF(aparserParser.NameFContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitNameN(aparserParser.NameNContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitNameDot(aparserParser.NameDotContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitTraceMore(aparserParser.TraceMoreContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitTraceLast(aparserParser.TraceLastContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitAAct(aparserParser.AActContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitFromTo(aparserParser.FromToContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitRegular(aparserParser.RegularContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitStar(aparserParser.StarContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitArrowstar(aparserParser.ArrowstarContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitStararrowstar(aparserParser.StararrowstarContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitWVar(aparserParser.WVarContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitWNum(aparserParser.WNumContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitWComma(aparserParser.WCommaContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitMnocomma(aparserParser.MnocommaContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitMcomma(aparserParser.McommaContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitNormfunction(aparserParser.NormfunctionContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitNormnoenc(aparserParser.NormnoencContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitNormenc(aparserParser.NormencContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitNormvariable(aparserParser.NormvariableContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitNormnum(aparserParser.NormnumContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitNormMore(aparserParser.NormMoreContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitNormUnder(aparserParser.NormUnderContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitNormparenth(aparserParser.NormparenthContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitLimore(aparserParser.LimoreContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitLisingle(aparserParser.LisingleContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitStatBoth(aparserParser.StatBothContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitStatStat(aparserParser.StatStatContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitStatNeither(aparserParser.StatNeitherContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitStatCol(aparserParser.StatColContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitTypesT(aparserParser.TypesTContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitTypesP(aparserParser.TypesPContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitTypesV(aparserParser.TypesVContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitTypesD(aparserParser.TypesDContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitFVer(aparserParser.FVerContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitTexMore(aparserParser.TexMoreContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitTexN(aparserParser.TexNContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitTexU(aparserParser.TexUContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitTexF(aparserParser.TexFContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitTexV(aparserParser.TexVContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitTexA(aparserParser.TexAContext ctx) { return visitChildren(ctx); }
}

View File

@ -0,0 +1,236 @@
/*
* BSD License
*
* Open Source Fixedpoint Model-Checker Graphical User Interface version 2019
*
* (C) Copyright <EFBFBD>lfur J<EFBFBD>hann Edvardsson 2019
* (C) Copyright Veronica Julie Lodskov Hoffmann 2019
*
* All Rights Reserved.
*
*/
package Model.Parser;
// Generated from aparser.g4 by ANTLR 4.7.1
import org.antlr.v4.runtime.Lexer;
import org.antlr.v4.runtime.CharStream;
import org.antlr.v4.runtime.*;
import org.antlr.v4.runtime.atn.*;
import org.antlr.v4.runtime.dfa.DFA;
@SuppressWarnings({"all", "warnings", "unchecked", "unused", "cast"})
public class aparserLexer extends Lexer {
static { RuntimeMetaData.checkVersion("4.7.1", RuntimeMetaData.VERSION); }
protected static final DFA[] _decisionToDFA;
protected static final PredictionContextCache _sharedContextCache =
new PredictionContextCache();
public static final int
T__0=1, T__1=2, T__2=3, T__3=4, T__4=5, T__5=6, T__6=7, T__7=8, T__8=9,
T__9=10, T__10=11, T__11=12, T__12=13, T__13=14, T__14=15, T__15=16, T__16=17,
T__17=18, T__18=19, T__19=20, T__20=21, T__21=22, T__22=23, T__23=24,
T__24=25, T__25=26, T__26=27, COLON=28, EQ=29, STAR=30, NEQ=31, SEMI=32,
HASH=33, ARROW=34, VAR=35, NUM=36, COMMENT=37, WS=38;
public static String[] channelNames = {
"DEFAULT_TOKEN_CHANNEL", "HIDDEN"
};
public static String[] modeNames = {
"DEFAULT_MODE"
};
public static final String[] ruleNames = {
"T__0", "T__1", "T__2", "T__3", "T__4", "T__5", "T__6", "T__7", "T__8",
"T__9", "T__10", "T__11", "T__12", "T__13", "T__14", "T__15", "T__16",
"T__17", "T__18", "T__19", "T__20", "T__21", "T__22", "T__23", "T__24",
"T__25", "T__26", "COLON", "COMMA", "EQ", "DASH", "STAR", "NEQ", "SEMI",
"HASH", "ARROW", "VAR", "NUM", "COMMENT", "WS"
};
private static final String[] _LITERAL_NAMES = {
null, "'Open-Source Fixedpoint Model-Checker version'", "'INPUT'", "'SUMMARY'",
"'GOAL'", "'DETAILS'", "'BACKEND'", "'STATISTICS'", "'ATTACK TRACE'",
"'.'", "'_'", "'-'", "'\\'", "'/'", "'('", "','", "')'", "'{'", "'}'",
"'{|'", "'|}'", "'TIME'", "'parseTime'", "'visitedNodes'", "'depth'",
"'ATTACK'", "'NO'", "'FOUND'", "':'", "'='", "'*'", "'!='", "';'", "'#'",
"'->'"
};
private static final String[] _SYMBOLIC_NAMES = {
null, null, null, null, null, null, null, null, null, null, null, null,
null, null, null, null, null, null, null, null, null, null, null, null,
null, null, null, null, "COLON", "EQ", "STAR", "NEQ", "SEMI", "HASH",
"ARROW", "VAR", "NUM", "COMMENT", "WS"
};
public static final Vocabulary VOCABULARY = new VocabularyImpl(_LITERAL_NAMES, _SYMBOLIC_NAMES);
/**
* @deprecated Use {@link #VOCABULARY} instead.
*/
@Deprecated
public static final String[] tokenNames;
static {
tokenNames = new String[_SYMBOLIC_NAMES.length];
for (int i = 0; i < tokenNames.length; i++) {
tokenNames[i] = VOCABULARY.getLiteralName(i);
if (tokenNames[i] == null) {
tokenNames[i] = VOCABULARY.getSymbolicName(i);
}
if (tokenNames[i] == null) {
tokenNames[i] = "<INVALID>";
}
}
}
@Override
@Deprecated
public String[] getTokenNames() {
return tokenNames;
}
@Override
public Vocabulary getVocabulary() {
return VOCABULARY;
}
public aparserLexer(CharStream input) {
super(input);
_interp = new LexerATNSimulator(this,_ATN,_decisionToDFA,_sharedContextCache);
}
@Override
public String getGrammarFileName() { return "aparser.g4"; }
@Override
public String[] getRuleNames() { return ruleNames; }
@Override
public String getSerializedATN() { return _serializedATN; }
@Override
public String[] getChannelNames() { return channelNames; }
@Override
public String[] getModeNames() { return modeNames; }
@Override
public ATN getATN() { return _ATN; }
public static final String _serializedATN =
"\3\u608b\ua72a\u8133\ub9ed\u417c\u3be7\u7786\u5964\2(\u014e\b\1\4\2\t"+
"\2\4\3\t\3\4\4\t\4\4\5\t\5\4\6\t\6\4\7\t\7\4\b\t\b\4\t\t\t\4\n\t\n\4\13"+
"\t\13\4\f\t\f\4\r\t\r\4\16\t\16\4\17\t\17\4\20\t\20\4\21\t\21\4\22\t\22"+
"\4\23\t\23\4\24\t\24\4\25\t\25\4\26\t\26\4\27\t\27\4\30\t\30\4\31\t\31"+
"\4\32\t\32\4\33\t\33\4\34\t\34\4\35\t\35\4\36\t\36\4\37\t\37\4 \t \4!"+
"\t!\4\"\t\"\4#\t#\4$\t$\4%\t%\4&\t&\4\'\t\'\4(\t(\4)\t)\3\2\3\2\3\2\3"+
"\2\3\2\3\2\3\2\3\2\3\2\3\2\3\2\3\2\3\2\3\2\3\2\3\2\3\2\3\2\3\2\3\2\3\2"+
"\3\2\3\2\3\2\3\2\3\2\3\2\3\2\3\2\3\2\3\2\3\2\3\2\3\2\3\2\3\2\3\2\3\2\3"+
"\2\3\2\3\2\3\2\3\2\3\2\3\2\3\3\3\3\3\3\3\3\3\3\3\3\3\4\3\4\3\4\3\4\3\4"+
"\3\4\3\4\3\4\3\5\3\5\3\5\3\5\3\5\3\6\3\6\3\6\3\6\3\6\3\6\3\6\3\6\3\7\3"+
"\7\3\7\3\7\3\7\3\7\3\7\3\7\3\b\3\b\3\b\3\b\3\b\3\b\3\b\3\b\3\b\3\b\3\b"+
"\3\t\3\t\3\t\3\t\3\t\3\t\3\t\3\t\3\t\3\t\3\t\3\t\3\t\3\n\3\n\3\13\3\13"+
"\3\f\3\f\3\r\3\r\3\16\3\16\3\17\3\17\3\20\3\20\3\21\3\21\3\22\3\22\3\23"+
"\3\23\3\24\3\24\3\24\3\25\3\25\3\25\3\26\3\26\3\26\3\26\3\26\3\27\3\27"+
"\3\27\3\27\3\27\3\27\3\27\3\27\3\27\3\27\3\30\3\30\3\30\3\30\3\30\3\30"+
"\3\30\3\30\3\30\3\30\3\30\3\30\3\30\3\31\3\31\3\31\3\31\3\31\3\31\3\32"+
"\3\32\3\32\3\32\3\32\3\32\3\32\3\33\3\33\3\33\3\34\3\34\3\34\3\34\3\34"+
"\3\34\3\35\3\35\3\36\3\36\3\37\3\37\3 \3 \3!\3!\3\"\3\"\3\"\3#\3#\3$\3"+
"$\3%\3%\3%\3&\6&\u011d\n&\r&\16&\u011e\3&\7&\u0122\n&\f&\16&\u0125\13"+
"&\3\'\6\'\u0128\n\'\r\'\16\'\u0129\3\'\3\'\6\'\u012e\n\'\r\'\16\'\u012f"+
"\5\'\u0132\n\'\3\'\3\'\5\'\u0136\n\'\3\'\6\'\u0139\n\'\r\'\16\'\u013a"+
"\5\'\u013d\n\'\3(\3(\7(\u0141\n(\f(\16(\u0144\13(\3(\3(\3)\6)\u0149\n"+
")\r)\16)\u014a\3)\3)\2\2*\3\3\5\4\7\5\t\6\13\7\r\b\17\t\21\n\23\13\25"+
"\f\27\r\31\16\33\17\35\20\37\21!\22#\23%\24\'\25)\26+\27-\30/\31\61\32"+
"\63\33\65\34\67\359\36;\2=\37?\2A C!E\"G#I$K%M&O\'Q(\3\2\7\4\2C\\c|\5"+
"\2\62;C\\c|\4\2--//\4\2\f\f\17\17\5\2\13\f\17\17\"\"\2\u0155\2\3\3\2\2"+
"\2\2\5\3\2\2\2\2\7\3\2\2\2\2\t\3\2\2\2\2\13\3\2\2\2\2\r\3\2\2\2\2\17\3"+
"\2\2\2\2\21\3\2\2\2\2\23\3\2\2\2\2\25\3\2\2\2\2\27\3\2\2\2\2\31\3\2\2"+
"\2\2\33\3\2\2\2\2\35\3\2\2\2\2\37\3\2\2\2\2!\3\2\2\2\2#\3\2\2\2\2%\3\2"+
"\2\2\2\'\3\2\2\2\2)\3\2\2\2\2+\3\2\2\2\2-\3\2\2\2\2/\3\2\2\2\2\61\3\2"+
"\2\2\2\63\3\2\2\2\2\65\3\2\2\2\2\67\3\2\2\2\29\3\2\2\2\2=\3\2\2\2\2A\3"+
"\2\2\2\2C\3\2\2\2\2E\3\2\2\2\2G\3\2\2\2\2I\3\2\2\2\2K\3\2\2\2\2M\3\2\2"+
"\2\2O\3\2\2\2\2Q\3\2\2\2\3S\3\2\2\2\5\u0080\3\2\2\2\7\u0086\3\2\2\2\t"+
"\u008e\3\2\2\2\13\u0093\3\2\2\2\r\u009b\3\2\2\2\17\u00a3\3\2\2\2\21\u00ae"+
"\3\2\2\2\23\u00bb\3\2\2\2\25\u00bd\3\2\2\2\27\u00bf\3\2\2\2\31\u00c1\3"+
"\2\2\2\33\u00c3\3\2\2\2\35\u00c5\3\2\2\2\37\u00c7\3\2\2\2!\u00c9\3\2\2"+
"\2#\u00cb\3\2\2\2%\u00cd\3\2\2\2\'\u00cf\3\2\2\2)\u00d2\3\2\2\2+\u00d5"+
"\3\2\2\2-\u00da\3\2\2\2/\u00e4\3\2\2\2\61\u00f1\3\2\2\2\63\u00f7\3\2\2"+
"\2\65\u00fe\3\2\2\2\67\u0101\3\2\2\29\u0107\3\2\2\2;\u0109\3\2\2\2=\u010b"+
"\3\2\2\2?\u010d\3\2\2\2A\u010f\3\2\2\2C\u0111\3\2\2\2E\u0114\3\2\2\2G"+
"\u0116\3\2\2\2I\u0118\3\2\2\2K\u011c\3\2\2\2M\u0127\3\2\2\2O\u013e\3\2"+
"\2\2Q\u0148\3\2\2\2ST\7Q\2\2TU\7r\2\2UV\7g\2\2VW\7p\2\2WX\7/\2\2XY\7U"+
"\2\2YZ\7q\2\2Z[\7w\2\2[\\\7t\2\2\\]\7e\2\2]^\7g\2\2^_\7\"\2\2_`\7H\2\2"+
"`a\7k\2\2ab\7z\2\2bc\7g\2\2cd\7f\2\2de\7r\2\2ef\7q\2\2fg\7k\2\2gh\7p\2"+
"\2hi\7v\2\2ij\7\"\2\2jk\7O\2\2kl\7q\2\2lm\7f\2\2mn\7g\2\2no\7n\2\2op\7"+
"/\2\2pq\7E\2\2qr\7j\2\2rs\7g\2\2st\7e\2\2tu\7m\2\2uv\7g\2\2vw\7t\2\2w"+
"x\7\"\2\2xy\7x\2\2yz\7g\2\2z{\7t\2\2{|\7u\2\2|}\7k\2\2}~\7q\2\2~\177\7"+
"p\2\2\177\4\3\2\2\2\u0080\u0081\7K\2\2\u0081\u0082\7P\2\2\u0082\u0083"+
"\7R\2\2\u0083\u0084\7W\2\2\u0084\u0085\7V\2\2\u0085\6\3\2\2\2\u0086\u0087"+
"\7U\2\2\u0087\u0088\7W\2\2\u0088\u0089\7O\2\2\u0089\u008a\7O\2\2\u008a"+
"\u008b\7C\2\2\u008b\u008c\7T\2\2\u008c\u008d\7[\2\2\u008d\b\3\2\2\2\u008e"+
"\u008f\7I\2\2\u008f\u0090\7Q\2\2\u0090\u0091\7C\2\2\u0091\u0092\7N\2\2"+
"\u0092\n\3\2\2\2\u0093\u0094\7F\2\2\u0094\u0095\7G\2\2\u0095\u0096\7V"+
"\2\2\u0096\u0097\7C\2\2\u0097\u0098\7K\2\2\u0098\u0099\7N\2\2\u0099\u009a"+
"\7U\2\2\u009a\f\3\2\2\2\u009b\u009c\7D\2\2\u009c\u009d\7C\2\2\u009d\u009e"+
"\7E\2\2\u009e\u009f\7M\2\2\u009f\u00a0\7G\2\2\u00a0\u00a1\7P\2\2\u00a1"+
"\u00a2\7F\2\2\u00a2\16\3\2\2\2\u00a3\u00a4\7U\2\2\u00a4\u00a5\7V\2\2\u00a5"+
"\u00a6\7C\2\2\u00a6\u00a7\7V\2\2\u00a7\u00a8\7K\2\2\u00a8\u00a9\7U\2\2"+
"\u00a9\u00aa\7V\2\2\u00aa\u00ab\7K\2\2\u00ab\u00ac\7E\2\2\u00ac\u00ad"+
"\7U\2\2\u00ad\20\3\2\2\2\u00ae\u00af\7C\2\2\u00af\u00b0\7V\2\2\u00b0\u00b1"+
"\7V\2\2\u00b1\u00b2\7C\2\2\u00b2\u00b3\7E\2\2\u00b3\u00b4\7M\2\2\u00b4"+
"\u00b5\7\"\2\2\u00b5\u00b6\7V\2\2\u00b6\u00b7\7T\2\2\u00b7\u00b8\7C\2"+
"\2\u00b8\u00b9\7E\2\2\u00b9\u00ba\7G\2\2\u00ba\22\3\2\2\2\u00bb\u00bc"+
"\7\60\2\2\u00bc\24\3\2\2\2\u00bd\u00be\7a\2\2\u00be\26\3\2\2\2\u00bf\u00c0"+
"\7/\2\2\u00c0\30\3\2\2\2\u00c1\u00c2\7^\2\2\u00c2\32\3\2\2\2\u00c3\u00c4"+
"\7\61\2\2\u00c4\34\3\2\2\2\u00c5\u00c6\7*\2\2\u00c6\36\3\2\2\2\u00c7\u00c8"+
"\7.\2\2\u00c8 \3\2\2\2\u00c9\u00ca\7+\2\2\u00ca\"\3\2\2\2\u00cb\u00cc"+
"\7}\2\2\u00cc$\3\2\2\2\u00cd\u00ce\7\177\2\2\u00ce&\3\2\2\2\u00cf\u00d0"+
"\7}\2\2\u00d0\u00d1\7~\2\2\u00d1(\3\2\2\2\u00d2\u00d3\7~\2\2\u00d3\u00d4"+
"\7\177\2\2\u00d4*\3\2\2\2\u00d5\u00d6\7V\2\2\u00d6\u00d7\7K\2\2\u00d7"+
"\u00d8\7O\2\2\u00d8\u00d9\7G\2\2\u00d9,\3\2\2\2\u00da\u00db\7r\2\2\u00db"+
"\u00dc\7c\2\2\u00dc\u00dd\7t\2\2\u00dd\u00de\7u\2\2\u00de\u00df\7g\2\2"+
"\u00df\u00e0\7V\2\2\u00e0\u00e1\7k\2\2\u00e1\u00e2\7o\2\2\u00e2\u00e3"+
"\7g\2\2\u00e3.\3\2\2\2\u00e4\u00e5\7x\2\2\u00e5\u00e6\7k\2\2\u00e6\u00e7"+
"\7u\2\2\u00e7\u00e8\7k\2\2\u00e8\u00e9\7v\2\2\u00e9\u00ea\7g\2\2\u00ea"+
"\u00eb\7f\2\2\u00eb\u00ec\7P\2\2\u00ec\u00ed\7q\2\2\u00ed\u00ee\7f\2\2"+
"\u00ee\u00ef\7g\2\2\u00ef\u00f0\7u\2\2\u00f0\60\3\2\2\2\u00f1\u00f2\7"+
"f\2\2\u00f2\u00f3\7g\2\2\u00f3\u00f4\7r\2\2\u00f4\u00f5\7v\2\2\u00f5\u00f6"+
"\7j\2\2\u00f6\62\3\2\2\2\u00f7\u00f8\7C\2\2\u00f8\u00f9\7V\2\2\u00f9\u00fa"+
"\7V\2\2\u00fa\u00fb\7C\2\2\u00fb\u00fc\7E\2\2\u00fc\u00fd\7M\2\2\u00fd"+
"\64\3\2\2\2\u00fe\u00ff\7P\2\2\u00ff\u0100\7Q\2\2\u0100\66\3\2\2\2\u0101"+
"\u0102\7H\2\2\u0102\u0103\7Q\2\2\u0103\u0104\7W\2\2\u0104\u0105\7P\2\2"+
"\u0105\u0106\7F\2\2\u01068\3\2\2\2\u0107\u0108\7<\2\2\u0108:\3\2\2\2\u0109"+
"\u010a\7.\2\2\u010a<\3\2\2\2\u010b\u010c\7?\2\2\u010c>\3\2\2\2\u010d\u010e"+
"\7/\2\2\u010e@\3\2\2\2\u010f\u0110\7,\2\2\u0110B\3\2\2\2\u0111\u0112\7"+
"#\2\2\u0112\u0113\7?\2\2\u0113D\3\2\2\2\u0114\u0115\7=\2\2\u0115F\3\2"+
"\2\2\u0116\u0117\7%\2\2\u0117H\3\2\2\2\u0118\u0119\7/\2\2\u0119\u011a"+
"\7@\2\2\u011aJ\3\2\2\2\u011b\u011d\t\2\2\2\u011c\u011b\3\2\2\2\u011d\u011e"+
"\3\2\2\2\u011e\u011c\3\2\2\2\u011e\u011f\3\2\2\2\u011f\u0123\3\2\2\2\u0120"+
"\u0122\t\3\2\2\u0121\u0120\3\2\2\2\u0122\u0125\3\2\2\2\u0123\u0121\3\2"+
"\2\2\u0123\u0124\3\2\2\2\u0124L\3\2\2\2\u0125\u0123\3\2\2\2\u0126\u0128"+
"\4\62;\2\u0127\u0126\3\2\2\2\u0128\u0129\3\2\2\2\u0129\u0127\3\2\2\2\u0129"+
"\u012a\3\2\2\2\u012a\u0131\3\2\2\2\u012b\u012d\7\60\2\2\u012c\u012e\4"+
"\62;\2\u012d\u012c\3\2\2\2\u012e\u012f\3\2\2\2\u012f\u012d\3\2\2\2\u012f"+
"\u0130\3\2\2\2\u0130\u0132\3\2\2\2\u0131\u012b\3\2\2\2\u0131\u0132\3\2"+
"\2\2\u0132\u013c\3\2\2\2\u0133\u0135\7G\2\2\u0134\u0136\t\4\2\2\u0135"+
"\u0134\3\2\2\2\u0135\u0136\3\2\2\2\u0136\u0138\3\2\2\2\u0137\u0139\4\62"+
";\2\u0138\u0137\3\2\2\2\u0139\u013a\3\2\2\2\u013a\u0138\3\2\2\2\u013a"+
"\u013b\3\2\2\2\u013b\u013d\3\2\2\2\u013c\u0133\3\2\2\2\u013c\u013d\3\2"+
"\2\2\u013dN\3\2\2\2\u013e\u0142\7\'\2\2\u013f\u0141\n\5\2\2\u0140\u013f"+
"\3\2\2\2\u0141\u0144\3\2\2\2\u0142\u0140\3\2\2\2\u0142\u0143\3\2\2\2\u0143"+
"\u0145\3\2\2\2\u0144\u0142\3\2\2\2\u0145\u0146\b(\2\2\u0146P\3\2\2\2\u0147"+
"\u0149\t\6\2\2\u0148\u0147\3\2\2\2\u0149\u014a\3\2\2\2\u014a\u0148\3\2"+
"\2\2\u014a\u014b\3\2\2\2\u014b\u014c\3\2\2\2\u014c\u014d\b)\2\2\u014d"+
"R\3\2\2\2\r\2\u011e\u0123\u0129\u012f\u0131\u0135\u013a\u013c\u0142\u014a"+
"\3\b\2\2";
public static final ATN _ATN =
new ATNDeserializer().deserialize(_serializedATN.toCharArray());
static {
_decisionToDFA = new DFA[_ATN.getNumberOfDecisions()];
for (int i = 0; i < _ATN.getNumberOfDecisions(); i++) {
_decisionToDFA[i] = new DFA(_ATN.getDecisionState(i), i);
}
}
}

File diff suppressed because it is too large Load Diff

View File

@ -0,0 +1,381 @@
/*
* BSD License
*
* Open Source Fixedpoint Model-Checker Graphical User Interface version 2019
*
* (C) Copyright <EFBFBD>lfur J<EFBFBD>hann Edvardsson 2019
* (C) Copyright Veronica Julie Lodskov Hoffmann 2019
*
* All Rights Reserved.
*
*/
package Model.Parser;
// Generated from aparser.g4 by ANTLR 4.7.1
import org.antlr.v4.runtime.tree.ParseTreeVisitor;
/**
* This interface defines a complete generic visitor for a parse tree produced
* by {@link aparserParser}.
*
* @param <T> The return type of the visit operation. Use {@link Void} for
* operations with no return type.
*/
public interface aparserVisitor<T> extends ParseTreeVisitor<T> {
/**
* Visit a parse tree produced by {@link aparserParser#start}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitStart(aparserParser.StartContext ctx);
/**
* Visit a parse tree produced by the {@code funVer}
* labeled alternative in {@link aparserParser#begin}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitFunVer(aparserParser.FunVerContext ctx);
/**
* Visit a parse tree produced by the {@code funIn}
* labeled alternative in {@link aparserParser#begin}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitFunIn(aparserParser.FunInContext ctx);
/**
* Visit a parse tree produced by the {@code funSum}
* labeled alternative in {@link aparserParser#begin}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitFunSum(aparserParser.FunSumContext ctx);
/**
* Visit a parse tree produced by the {@code funGoal}
* labeled alternative in {@link aparserParser#begin}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitFunGoal(aparserParser.FunGoalContext ctx);
/**
* Visit a parse tree produced by the {@code funDet}
* labeled alternative in {@link aparserParser#begin}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitFunDet(aparserParser.FunDetContext ctx);
/**
* Visit a parse tree produced by the {@code funBack}
* labeled alternative in {@link aparserParser#begin}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitFunBack(aparserParser.FunBackContext ctx);
/**
* Visit a parse tree produced by the {@code funStat}
* labeled alternative in {@link aparserParser#begin}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitFunStat(aparserParser.FunStatContext ctx);
/**
* Visit a parse tree produced by the {@code funTrace}
* labeled alternative in {@link aparserParser#begin}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitFunTrace(aparserParser.FunTraceContext ctx);
/**
* Visit a parse tree produced by the {@code nameV}
* labeled alternative in {@link aparserParser#name}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitNameV(aparserParser.NameVContext ctx);
/**
* Visit a parse tree produced by the {@code nameF}
* labeled alternative in {@link aparserParser#name}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitNameF(aparserParser.NameFContext ctx);
/**
* Visit a parse tree produced by the {@code nameN}
* labeled alternative in {@link aparserParser#name}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitNameN(aparserParser.NameNContext ctx);
/**
* Visit a parse tree produced by the {@code nameDot}
* labeled alternative in {@link aparserParser#name}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitNameDot(aparserParser.NameDotContext ctx);
/**
* Visit a parse tree produced by the {@code traceMore}
* labeled alternative in {@link aparserParser#trace}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitTraceMore(aparserParser.TraceMoreContext ctx);
/**
* Visit a parse tree produced by the {@code traceLast}
* labeled alternative in {@link aparserParser#trace}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitTraceLast(aparserParser.TraceLastContext ctx);
/**
* Visit a parse tree produced by the {@code aAct}
* labeled alternative in {@link aparserParser#act}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitAAct(aparserParser.AActContext ctx);
/**
* Visit a parse tree produced by the {@code fromTo}
* labeled alternative in {@link aparserParser#w2w}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitFromTo(aparserParser.FromToContext ctx);
/**
* Visit a parse tree produced by the {@code regular}
* labeled alternative in {@link aparserParser#c}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitRegular(aparserParser.RegularContext ctx);
/**
* Visit a parse tree produced by the {@code star}
* labeled alternative in {@link aparserParser#c}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitStar(aparserParser.StarContext ctx);
/**
* Visit a parse tree produced by the {@code arrowstar}
* labeled alternative in {@link aparserParser#c}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitArrowstar(aparserParser.ArrowstarContext ctx);
/**
* Visit a parse tree produced by the {@code stararrowstar}
* labeled alternative in {@link aparserParser#c}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitStararrowstar(aparserParser.StararrowstarContext ctx);
/**
* Visit a parse tree produced by the {@code wVar}
* labeled alternative in {@link aparserParser#w}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitWVar(aparserParser.WVarContext ctx);
/**
* Visit a parse tree produced by the {@code wNum}
* labeled alternative in {@link aparserParser#w}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitWNum(aparserParser.WNumContext ctx);
/**
* Visit a parse tree produced by the {@code wComma}
* labeled alternative in {@link aparserParser#w}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitWComma(aparserParser.WCommaContext ctx);
/**
* Visit a parse tree produced by the {@code mnocomma}
* labeled alternative in {@link aparserParser#m}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitMnocomma(aparserParser.MnocommaContext ctx);
/**
* Visit a parse tree produced by the {@code mcomma}
* labeled alternative in {@link aparserParser#m}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitMcomma(aparserParser.McommaContext ctx);
/**
* Visit a parse tree produced by the {@code normfunction}
* labeled alternative in {@link aparserParser#norm}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitNormfunction(aparserParser.NormfunctionContext ctx);
/**
* Visit a parse tree produced by the {@code normnoenc}
* labeled alternative in {@link aparserParser#norm}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitNormnoenc(aparserParser.NormnoencContext ctx);
/**
* Visit a parse tree produced by the {@code normenc}
* labeled alternative in {@link aparserParser#norm}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitNormenc(aparserParser.NormencContext ctx);
/**
* Visit a parse tree produced by the {@code normvariable}
* labeled alternative in {@link aparserParser#norm}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitNormvariable(aparserParser.NormvariableContext ctx);
/**
* Visit a parse tree produced by the {@code normnum}
* labeled alternative in {@link aparserParser#norm}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitNormnum(aparserParser.NormnumContext ctx);
/**
* Visit a parse tree produced by the {@code normMore}
* labeled alternative in {@link aparserParser#norm}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitNormMore(aparserParser.NormMoreContext ctx);
/**
* Visit a parse tree produced by the {@code normUnder}
* labeled alternative in {@link aparserParser#norm}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitNormUnder(aparserParser.NormUnderContext ctx);
/**
* Visit a parse tree produced by the {@code normparenth}
* labeled alternative in {@link aparserParser#norm}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitNormparenth(aparserParser.NormparenthContext ctx);
/**
* Visit a parse tree produced by the {@code limore}
* labeled alternative in {@link aparserParser#li}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitLimore(aparserParser.LimoreContext ctx);
/**
* Visit a parse tree produced by the {@code lisingle}
* labeled alternative in {@link aparserParser#li}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitLisingle(aparserParser.LisingleContext ctx);
/**
* Visit a parse tree produced by the {@code statBoth}
* labeled alternative in {@link aparserParser#stat}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitStatBoth(aparserParser.StatBothContext ctx);
/**
* Visit a parse tree produced by the {@code statStat}
* labeled alternative in {@link aparserParser#stat}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitStatStat(aparserParser.StatStatContext ctx);
/**
* Visit a parse tree produced by the {@code statNeither}
* labeled alternative in {@link aparserParser#stat}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitStatNeither(aparserParser.StatNeitherContext ctx);
/**
* Visit a parse tree produced by the {@code statCol}
* labeled alternative in {@link aparserParser#stat}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitStatCol(aparserParser.StatColContext ctx);
/**
* Visit a parse tree produced by the {@code typesT}
* labeled alternative in {@link aparserParser#types}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitTypesT(aparserParser.TypesTContext ctx);
/**
* Visit a parse tree produced by the {@code typesP}
* labeled alternative in {@link aparserParser#types}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitTypesP(aparserParser.TypesPContext ctx);
/**
* Visit a parse tree produced by the {@code typesV}
* labeled alternative in {@link aparserParser#types}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitTypesV(aparserParser.TypesVContext ctx);
/**
* Visit a parse tree produced by the {@code typesD}
* labeled alternative in {@link aparserParser#types}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitTypesD(aparserParser.TypesDContext ctx);
/**
* Visit a parse tree produced by the {@code fVer}
* labeled alternative in {@link aparserParser#ver}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitFVer(aparserParser.FVerContext ctx);
/**
* Visit a parse tree produced by the {@code texMore}
* labeled alternative in {@link aparserParser#tex}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitTexMore(aparserParser.TexMoreContext ctx);
/**
* Visit a parse tree produced by the {@code texN}
* labeled alternative in {@link aparserParser#tex}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitTexN(aparserParser.TexNContext ctx);
/**
* Visit a parse tree produced by the {@code texU}
* labeled alternative in {@link aparserParser#tex}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitTexU(aparserParser.TexUContext ctx);
/**
* Visit a parse tree produced by the {@code texF}
* labeled alternative in {@link aparserParser#tex}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitTexF(aparserParser.TexFContext ctx);
/**
* Visit a parse tree produced by the {@code texV}
* labeled alternative in {@link aparserParser#tex}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitTexV(aparserParser.TexVContext ctx);
/**
* Visit a parse tree produced by the {@code texA}
* labeled alternative in {@link aparserParser#tex}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitTexA(aparserParser.TexAContext ctx);
}

View File

@ -0,0 +1,364 @@
package Model.Parser;
// Generated from pparser.g4 by ANTLR 4.7.1
import org.antlr.v4.runtime.tree.AbstractParseTreeVisitor;
/**
* This class provides an empty implementation of {@link pparserVisitor},
* which can be extended to create a visitor which only needs to handle a subset
* of the available methods.
*
* @param <T> The return type of the visit operation. Use {@link Void} for
* operations with no return type.
*/
public class pparserBaseVisitor<T> extends AbstractParseTreeVisitor<T> implements pparserVisitor<T> {
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitStart(pparserParser.StartContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitFunProtocol(pparserParser.FunProtocolContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitFunTypes(pparserParser.FunTypesContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitFunKnowledge(pparserParser.FunKnowledgeContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitFunActions(pparserParser.FunActionsContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitFunGoals(pparserParser.FunGoalsContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitFunBrainWhere(pparserParser.FunBrainWhereContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitFunBrain(pparserParser.FunBrainContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitBrainWithSemi(pparserParser.BrainWithSemiContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitBrainOptSemi(pparserParser.BrainOptSemiContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitNotlastAct(pparserParser.NotlastActContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitLastAct(pparserParser.LastActContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitFunFromTo(pparserParser.FunFromToContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitRegular(pparserParser.RegularContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitStar(pparserParser.StarContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitArrowstar(pparserParser.ArrowstarContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitStararrowstar(pparserParser.StararrowstarContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitNormal(pparserParser.NormalContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitSquare(pparserParser.SquareContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitSquaremess(pparserParser.SquaremessContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitWscomma(pparserParser.WscommaContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitWsnocomma(pparserParser.WsnocommaContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitWaisingle(pparserParser.WaisingleContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitWaimore(pparserParser.WaimoreContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitMnocomma(pparserParser.MnocommaContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitMcomma(pparserParser.McommaContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitNormfunction(pparserParser.NormfunctionContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitNormnoenc(pparserParser.NormnoencContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitNormenc(pparserParser.NormencContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitNormvariable(pparserParser.NormvariableContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitNormparenth(pparserParser.NormparenthContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitLimore(pparserParser.LimoreContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitLisingle(pparserParser.LisingleContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitGoalsmore(pparserParser.GoalsmoreContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitGoalssingle(pparserParser.GoalssingleContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitSecretbetween(pparserParser.SecretbetweenContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitWeaklyauthent(pparserParser.WeaklyauthentContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitAuthent(pparserParser.AuthentContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitArrowmsg(pparserParser.ArrowmsgContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitTypesoptsemi(pparserParser.TypesoptsemiContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitTypesemi(pparserParser.TypesemiContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitCsepsingle(pparserParser.CsepsingleContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitCsepmore(pparserParser.CsepmoreContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitAg(pparserParser.AgContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitNu(pparserParser.NuContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitSeq(pparserParser.SeqContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitPk(pparserParser.PkContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitSymk(pparserParser.SymkContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitFunc(pparserParser.FuncContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitUnt(pparserParser.UntContext ctx) { return visitChildren(ctx); }
}

View File

@ -0,0 +1,230 @@
package Model.Parser;
// Generated from pparser.g4 by ANTLR 4.7.1
import org.antlr.v4.runtime.Lexer;
import org.antlr.v4.runtime.CharStream;
import org.antlr.v4.runtime.Token;
import org.antlr.v4.runtime.TokenStream;
import org.antlr.v4.runtime.*;
import org.antlr.v4.runtime.atn.*;
import org.antlr.v4.runtime.dfa.DFA;
import org.antlr.v4.runtime.misc.*;
@SuppressWarnings({"all", "warnings", "unchecked", "unused", "cast"})
public class pparserLexer extends Lexer {
static { RuntimeMetaData.checkVersion("4.7.1", RuntimeMetaData.VERSION); }
protected static final DFA[] _decisionToDFA;
protected static final PredictionContextCache _sharedContextCache =
new PredictionContextCache();
public static final int
T__0=1, T__1=2, T__2=3, T__3=4, T__4=5, T__5=6, T__6=7, T__7=8, T__8=9,
T__9=10, T__10=11, T__11=12, T__12=13, T__13=14, T__14=15, T__15=16, T__16=17,
T__17=18, T__18=19, T__19=20, T__20=21, T__21=22, T__22=23, T__23=24,
T__24=25, T__25=26, COLON=27, EQ=28, STAR=29, NEQ=30, SEMI=31, HASH=32,
ARROW=33, VAR=34, NAME=35, NUM=36, COMMENT=37, WS=38;
public static String[] channelNames = {
"DEFAULT_TOKEN_CHANNEL", "HIDDEN"
};
public static String[] modeNames = {
"DEFAULT_MODE"
};
public static final String[] ruleNames = {
"T__0", "T__1", "T__2", "T__3", "T__4", "T__5", "T__6", "T__7", "T__8",
"T__9", "T__10", "T__11", "T__12", "T__13", "T__14", "T__15", "T__16",
"T__17", "T__18", "T__19", "T__20", "T__21", "T__22", "T__23", "T__24",
"T__25", "COLON", "COMMA", "EQ", "DASH", "STAR", "NEQ", "SEMI", "HASH",
"ARROW", "VAR", "NAME", "NUM", "COMMENT", "WS"
};
private static final String[] _LITERAL_NAMES = {
null, "'Protocol'", "'Types'", "'Knowledge'", "'Actions'", "'Goals'",
"'where'", "'['", "']'", "','", "'('", "')'", "'{'", "'}'", "'{|'", "'|}'",
"'secret between'", "'weakly authenticates'", "'on'", "'authenticates'",
"'Agent'", "'Number'", "'SeqNumber'", "'PublicKey'", "'Symmetric_key'",
"'Function'", "'Untyped'", "':'", "'='", "'*'", "'!='", "';'", "'#'",
"'->'"
};
private static final String[] _SYMBOLIC_NAMES = {
null, null, null, null, null, null, null, null, null, null, null, null,
null, null, null, null, null, null, null, null, null, null, null, null,
null, null, null, "COLON", "EQ", "STAR", "NEQ", "SEMI", "HASH", "ARROW",
"VAR", "NAME", "NUM", "COMMENT", "WS"
};
public static final Vocabulary VOCABULARY = new VocabularyImpl(_LITERAL_NAMES, _SYMBOLIC_NAMES);
/**
* @deprecated Use {@link #VOCABULARY} instead.
*/
@Deprecated
public static final String[] tokenNames;
static {
tokenNames = new String[_SYMBOLIC_NAMES.length];
for (int i = 0; i < tokenNames.length; i++) {
tokenNames[i] = VOCABULARY.getLiteralName(i);
if (tokenNames[i] == null) {
tokenNames[i] = VOCABULARY.getSymbolicName(i);
}
if (tokenNames[i] == null) {
tokenNames[i] = "<INVALID>";
}
}
}
@Override
@Deprecated
public String[] getTokenNames() {
return tokenNames;
}
@Override
public Vocabulary getVocabulary() {
return VOCABULARY;
}
public pparserLexer(CharStream input) {
super(input);
_interp = new LexerATNSimulator(this,_ATN,_decisionToDFA,_sharedContextCache);
}
@Override
public String getGrammarFileName() { return "pparser.g4"; }
@Override
public String[] getRuleNames() { return ruleNames; }
@Override
public String getSerializedATN() { return _serializedATN; }
@Override
public String[] getChannelNames() { return channelNames; }
@Override
public String[] getModeNames() { return modeNames; }
@Override
public ATN getATN() { return _ATN; }
public static final String _serializedATN =
"\3\u608b\ua72a\u8133\ub9ed\u417c\u3be7\u7786\u5964\2(\u0155\b\1\4\2\t"+
"\2\4\3\t\3\4\4\t\4\4\5\t\5\4\6\t\6\4\7\t\7\4\b\t\b\4\t\t\t\4\n\t\n\4\13"+
"\t\13\4\f\t\f\4\r\t\r\4\16\t\16\4\17\t\17\4\20\t\20\4\21\t\21\4\22\t\22"+
"\4\23\t\23\4\24\t\24\4\25\t\25\4\26\t\26\4\27\t\27\4\30\t\30\4\31\t\31"+
"\4\32\t\32\4\33\t\33\4\34\t\34\4\35\t\35\4\36\t\36\4\37\t\37\4 \t \4!"+
"\t!\4\"\t\"\4#\t#\4$\t$\4%\t%\4&\t&\4\'\t\'\4(\t(\4)\t)\3\2\3\2\3\2\3"+
"\2\3\2\3\2\3\2\3\2\3\2\3\3\3\3\3\3\3\3\3\3\3\3\3\4\3\4\3\4\3\4\3\4\3\4"+
"\3\4\3\4\3\4\3\4\3\5\3\5\3\5\3\5\3\5\3\5\3\5\3\5\3\6\3\6\3\6\3\6\3\6\3"+
"\6\3\7\3\7\3\7\3\7\3\7\3\7\3\b\3\b\3\t\3\t\3\n\3\n\3\13\3\13\3\f\3\f\3"+
"\r\3\r\3\16\3\16\3\17\3\17\3\17\3\20\3\20\3\20\3\21\3\21\3\21\3\21\3\21"+
"\3\21\3\21\3\21\3\21\3\21\3\21\3\21\3\21\3\21\3\21\3\22\3\22\3\22\3\22"+
"\3\22\3\22\3\22\3\22\3\22\3\22\3\22\3\22\3\22\3\22\3\22\3\22\3\22\3\22"+
"\3\22\3\22\3\22\3\23\3\23\3\23\3\24\3\24\3\24\3\24\3\24\3\24\3\24\3\24"+
"\3\24\3\24\3\24\3\24\3\24\3\24\3\25\3\25\3\25\3\25\3\25\3\25\3\26\3\26"+
"\3\26\3\26\3\26\3\26\3\26\3\27\3\27\3\27\3\27\3\27\3\27\3\27\3\27\3\27"+
"\3\27\3\30\3\30\3\30\3\30\3\30\3\30\3\30\3\30\3\30\3\30\3\31\3\31\3\31"+
"\3\31\3\31\3\31\3\31\3\31\3\31\3\31\3\31\3\31\3\31\3\31\3\32\3\32\3\32"+
"\3\32\3\32\3\32\3\32\3\32\3\32\3\33\3\33\3\33\3\33\3\33\3\33\3\33\3\33"+
"\3\34\3\34\3\35\3\35\3\36\3\36\3\37\3\37\3 \3 \3!\3!\3!\3\"\3\"\3#\3#"+
"\3$\3$\3$\3%\6%\u011f\n%\r%\16%\u0120\3%\7%\u0124\n%\f%\16%\u0127\13%"+
"\3&\6&\u012a\n&\r&\16&\u012b\3\'\6\'\u012f\n\'\r\'\16\'\u0130\3\'\3\'"+
"\6\'\u0135\n\'\r\'\16\'\u0136\5\'\u0139\n\'\3\'\3\'\5\'\u013d\n\'\3\'"+
"\6\'\u0140\n\'\r\'\16\'\u0141\5\'\u0144\n\'\3(\3(\7(\u0148\n(\f(\16(\u014b"+
"\13(\3(\3(\3)\6)\u0150\n)\r)\16)\u0151\3)\3)\2\2*\3\3\5\4\7\5\t\6\13\7"+
"\r\b\17\t\21\n\23\13\25\f\27\r\31\16\33\17\35\20\37\21!\22#\23%\24\'\25"+
")\26+\27-\30/\31\61\32\63\33\65\34\67\359\2;\36=\2?\37A C!E\"G#I$K%M&"+
"O\'Q(\3\2\7\4\2C\\c|\6\2\62;C\\aac|\4\2--//\4\2\f\f\17\17\5\2\13\f\17"+
"\17\"\"\2\u015d\2\3\3\2\2\2\2\5\3\2\2\2\2\7\3\2\2\2\2\t\3\2\2\2\2\13\3"+
"\2\2\2\2\r\3\2\2\2\2\17\3\2\2\2\2\21\3\2\2\2\2\23\3\2\2\2\2\25\3\2\2\2"+
"\2\27\3\2\2\2\2\31\3\2\2\2\2\33\3\2\2\2\2\35\3\2\2\2\2\37\3\2\2\2\2!\3"+
"\2\2\2\2#\3\2\2\2\2%\3\2\2\2\2\'\3\2\2\2\2)\3\2\2\2\2+\3\2\2\2\2-\3\2"+
"\2\2\2/\3\2\2\2\2\61\3\2\2\2\2\63\3\2\2\2\2\65\3\2\2\2\2\67\3\2\2\2\2"+
";\3\2\2\2\2?\3\2\2\2\2A\3\2\2\2\2C\3\2\2\2\2E\3\2\2\2\2G\3\2\2\2\2I\3"+
"\2\2\2\2K\3\2\2\2\2M\3\2\2\2\2O\3\2\2\2\2Q\3\2\2\2\3S\3\2\2\2\5\\\3\2"+
"\2\2\7b\3\2\2\2\tl\3\2\2\2\13t\3\2\2\2\rz\3\2\2\2\17\u0080\3\2\2\2\21"+
"\u0082\3\2\2\2\23\u0084\3\2\2\2\25\u0086\3\2\2\2\27\u0088\3\2\2\2\31\u008a"+
"\3\2\2\2\33\u008c\3\2\2\2\35\u008e\3\2\2\2\37\u0091\3\2\2\2!\u0094\3\2"+
"\2\2#\u00a3\3\2\2\2%\u00b8\3\2\2\2\'\u00bb\3\2\2\2)\u00c9\3\2\2\2+\u00cf"+
"\3\2\2\2-\u00d6\3\2\2\2/\u00e0\3\2\2\2\61\u00ea\3\2\2\2\63\u00f8\3\2\2"+
"\2\65\u0101\3\2\2\2\67\u0109\3\2\2\29\u010b\3\2\2\2;\u010d\3\2\2\2=\u010f"+
"\3\2\2\2?\u0111\3\2\2\2A\u0113\3\2\2\2C\u0116\3\2\2\2E\u0118\3\2\2\2G"+
"\u011a\3\2\2\2I\u011e\3\2\2\2K\u0129\3\2\2\2M\u012e\3\2\2\2O\u0145\3\2"+
"\2\2Q\u014f\3\2\2\2ST\7R\2\2TU\7t\2\2UV\7q\2\2VW\7v\2\2WX\7q\2\2XY\7e"+
"\2\2YZ\7q\2\2Z[\7n\2\2[\4\3\2\2\2\\]\7V\2\2]^\7{\2\2^_\7r\2\2_`\7g\2\2"+
"`a\7u\2\2a\6\3\2\2\2bc\7M\2\2cd\7p\2\2de\7q\2\2ef\7y\2\2fg\7n\2\2gh\7"+
"g\2\2hi\7f\2\2ij\7i\2\2jk\7g\2\2k\b\3\2\2\2lm\7C\2\2mn\7e\2\2no\7v\2\2"+
"op\7k\2\2pq\7q\2\2qr\7p\2\2rs\7u\2\2s\n\3\2\2\2tu\7I\2\2uv\7q\2\2vw\7"+
"c\2\2wx\7n\2\2xy\7u\2\2y\f\3\2\2\2z{\7y\2\2{|\7j\2\2|}\7g\2\2}~\7t\2\2"+
"~\177\7g\2\2\177\16\3\2\2\2\u0080\u0081\7]\2\2\u0081\20\3\2\2\2\u0082"+
"\u0083\7_\2\2\u0083\22\3\2\2\2\u0084\u0085\7.\2\2\u0085\24\3\2\2\2\u0086"+
"\u0087\7*\2\2\u0087\26\3\2\2\2\u0088\u0089\7+\2\2\u0089\30\3\2\2\2\u008a"+
"\u008b\7}\2\2\u008b\32\3\2\2\2\u008c\u008d\7\177\2\2\u008d\34\3\2\2\2"+
"\u008e\u008f\7}\2\2\u008f\u0090\7~\2\2\u0090\36\3\2\2\2\u0091\u0092\7"+
"~\2\2\u0092\u0093\7\177\2\2\u0093 \3\2\2\2\u0094\u0095\7u\2\2\u0095\u0096"+
"\7g\2\2\u0096\u0097\7e\2\2\u0097\u0098\7t\2\2\u0098\u0099\7g\2\2\u0099"+
"\u009a\7v\2\2\u009a\u009b\7\"\2\2\u009b\u009c\7d\2\2\u009c\u009d\7g\2"+
"\2\u009d\u009e\7v\2\2\u009e\u009f\7y\2\2\u009f\u00a0\7g\2\2\u00a0\u00a1"+
"\7g\2\2\u00a1\u00a2\7p\2\2\u00a2\"\3\2\2\2\u00a3\u00a4\7y\2\2\u00a4\u00a5"+
"\7g\2\2\u00a5\u00a6\7c\2\2\u00a6\u00a7\7m\2\2\u00a7\u00a8\7n\2\2\u00a8"+
"\u00a9\7{\2\2\u00a9\u00aa\7\"\2\2\u00aa\u00ab\7c\2\2\u00ab\u00ac\7w\2"+
"\2\u00ac\u00ad\7v\2\2\u00ad\u00ae\7j\2\2\u00ae\u00af\7g\2\2\u00af\u00b0"+
"\7p\2\2\u00b0\u00b1\7v\2\2\u00b1\u00b2\7k\2\2\u00b2\u00b3\7e\2\2\u00b3"+
"\u00b4\7c\2\2\u00b4\u00b5\7v\2\2\u00b5\u00b6\7g\2\2\u00b6\u00b7\7u\2\2"+
"\u00b7$\3\2\2\2\u00b8\u00b9\7q\2\2\u00b9\u00ba\7p\2\2\u00ba&\3\2\2\2\u00bb"+
"\u00bc\7c\2\2\u00bc\u00bd\7w\2\2\u00bd\u00be\7v\2\2\u00be\u00bf\7j\2\2"+
"\u00bf\u00c0\7g\2\2\u00c0\u00c1\7p\2\2\u00c1\u00c2\7v\2\2\u00c2\u00c3"+
"\7k\2\2\u00c3\u00c4\7e\2\2\u00c4\u00c5\7c\2\2\u00c5\u00c6\7v\2\2\u00c6"+
"\u00c7\7g\2\2\u00c7\u00c8\7u\2\2\u00c8(\3\2\2\2\u00c9\u00ca\7C\2\2\u00ca"+
"\u00cb\7i\2\2\u00cb\u00cc\7g\2\2\u00cc\u00cd\7p\2\2\u00cd\u00ce\7v\2\2"+
"\u00ce*\3\2\2\2\u00cf\u00d0\7P\2\2\u00d0\u00d1\7w\2\2\u00d1\u00d2\7o\2"+
"\2\u00d2\u00d3\7d\2\2\u00d3\u00d4\7g\2\2\u00d4\u00d5\7t\2\2\u00d5,\3\2"+
"\2\2\u00d6\u00d7\7U\2\2\u00d7\u00d8\7g\2\2\u00d8\u00d9\7s\2\2\u00d9\u00da"+
"\7P\2\2\u00da\u00db\7w\2\2\u00db\u00dc\7o\2\2\u00dc\u00dd\7d\2\2\u00dd"+
"\u00de\7g\2\2\u00de\u00df\7t\2\2\u00df.\3\2\2\2\u00e0\u00e1\7R\2\2\u00e1"+
"\u00e2\7w\2\2\u00e2\u00e3\7d\2\2\u00e3\u00e4\7n\2\2\u00e4\u00e5\7k\2\2"+
"\u00e5\u00e6\7e\2\2\u00e6\u00e7\7M\2\2\u00e7\u00e8\7g\2\2\u00e8\u00e9"+
"\7{\2\2\u00e9\60\3\2\2\2\u00ea\u00eb\7U\2\2\u00eb\u00ec\7{\2\2\u00ec\u00ed"+
"\7o\2\2\u00ed\u00ee\7o\2\2\u00ee\u00ef\7g\2\2\u00ef\u00f0\7v\2\2\u00f0"+
"\u00f1\7t\2\2\u00f1\u00f2\7k\2\2\u00f2\u00f3\7e\2\2\u00f3\u00f4\7a\2\2"+
"\u00f4\u00f5\7m\2\2\u00f5\u00f6\7g\2\2\u00f6\u00f7\7{\2\2\u00f7\62\3\2"+
"\2\2\u00f8\u00f9\7H\2\2\u00f9\u00fa\7w\2\2\u00fa\u00fb\7p\2\2\u00fb\u00fc"+
"\7e\2\2\u00fc\u00fd\7v\2\2\u00fd\u00fe\7k\2\2\u00fe\u00ff\7q\2\2\u00ff"+
"\u0100\7p\2\2\u0100\64\3\2\2\2\u0101\u0102\7W\2\2\u0102\u0103\7p\2\2\u0103"+
"\u0104\7v\2\2\u0104\u0105\7{\2\2\u0105\u0106\7r\2\2\u0106\u0107\7g\2\2"+
"\u0107\u0108\7f\2\2\u0108\66\3\2\2\2\u0109\u010a\7<\2\2\u010a8\3\2\2\2"+
"\u010b\u010c\7.\2\2\u010c:\3\2\2\2\u010d\u010e\7?\2\2\u010e<\3\2\2\2\u010f"+
"\u0110\7/\2\2\u0110>\3\2\2\2\u0111\u0112\7,\2\2\u0112@\3\2\2\2\u0113\u0114"+
"\7#\2\2\u0114\u0115\7?\2\2\u0115B\3\2\2\2\u0116\u0117\7=\2\2\u0117D\3"+
"\2\2\2\u0118\u0119\7%\2\2\u0119F\3\2\2\2\u011a\u011b\7/\2\2\u011b\u011c"+
"\7@\2\2\u011cH\3\2\2\2\u011d\u011f\t\2\2\2\u011e\u011d\3\2\2\2\u011f\u0120"+
"\3\2\2\2\u0120\u011e\3\2\2\2\u0120\u0121\3\2\2\2\u0121\u0125\3\2\2\2\u0122"+
"\u0124\t\3\2\2\u0123\u0122\3\2\2\2\u0124\u0127\3\2\2\2\u0125\u0123\3\2"+
"\2\2\u0125\u0126\3\2\2\2\u0126J\3\2\2\2\u0127\u0125\3\2\2\2\u0128\u012a"+
"\t\3\2\2\u0129\u0128\3\2\2\2\u012a\u012b\3\2\2\2\u012b\u0129\3\2\2\2\u012b"+
"\u012c\3\2\2\2\u012cL\3\2\2\2\u012d\u012f\4\62;\2\u012e\u012d\3\2\2\2"+
"\u012f\u0130\3\2\2\2\u0130\u012e\3\2\2\2\u0130\u0131\3\2\2\2\u0131\u0138"+
"\3\2\2\2\u0132\u0134\7\60\2\2\u0133\u0135\4\62;\2\u0134\u0133\3\2\2\2"+
"\u0135\u0136\3\2\2\2\u0136\u0134\3\2\2\2\u0136\u0137\3\2\2\2\u0137\u0139"+
"\3\2\2\2\u0138\u0132\3\2\2\2\u0138\u0139\3\2\2\2\u0139\u0143\3\2\2\2\u013a"+
"\u013c\7G\2\2\u013b\u013d\t\4\2\2\u013c\u013b\3\2\2\2\u013c\u013d\3\2"+
"\2\2\u013d\u013f\3\2\2\2\u013e\u0140\4\62;\2\u013f\u013e\3\2\2\2\u0140"+
"\u0141\3\2\2\2\u0141\u013f\3\2\2\2\u0141\u0142\3\2\2\2\u0142\u0144\3\2"+
"\2\2\u0143\u013a\3\2\2\2\u0143\u0144\3\2\2\2\u0144N\3\2\2\2\u0145\u0149"+
"\7%\2\2\u0146\u0148\n\5\2\2\u0147\u0146\3\2\2\2\u0148\u014b\3\2\2\2\u0149"+
"\u0147\3\2\2\2\u0149\u014a\3\2\2\2\u014a\u014c\3\2\2\2\u014b\u0149\3\2"+
"\2\2\u014c\u014d\b(\2\2\u014dP\3\2\2\2\u014e\u0150\t\6\2\2\u014f\u014e"+
"\3\2\2\2\u0150\u0151\3\2\2\2\u0151\u014f\3\2\2\2\u0151\u0152\3\2\2\2\u0152"+
"\u0153\3\2\2\2\u0153\u0154\b)\2\2\u0154R\3\2\2\2\20\2\u0120\u0123\u0125"+
"\u0129\u012b\u0130\u0136\u0138\u013c\u0141\u0143\u0149\u0151\3\b\2\2";
public static final ATN _ATN =
new ATNDeserializer().deserialize(_serializedATN.toCharArray());
static {
_decisionToDFA = new DFA[_ATN.getNumberOfDecisions()];
for (int i = 0; i < _ATN.getNumberOfDecisions(); i++) {
_decisionToDFA[i] = new DFA(_ATN.getDecisionState(i), i);
}
}
}

File diff suppressed because it is too large Load Diff

View File

@ -0,0 +1,362 @@
package Model.Parser;
// Generated from pparser.g4 by ANTLR 4.7.1
import org.antlr.v4.runtime.tree.ParseTreeVisitor;
/**
* This interface defines a complete generic visitor for a parse tree produced
* by {@link pparserParser}.
*
* @param <T> The return type of the visit operation. Use {@link Void} for
* operations with no return type.
*/
public interface pparserVisitor<T> extends ParseTreeVisitor<T> {
/**
* Visit a parse tree produced by {@link pparserParser#start}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitStart(pparserParser.StartContext ctx);
/**
* Visit a parse tree produced by the {@code funProtocol}
* labeled alternative in {@link pparserParser#begin}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitFunProtocol(pparserParser.FunProtocolContext ctx);
/**
* Visit a parse tree produced by the {@code funTypes}
* labeled alternative in {@link pparserParser#begin}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitFunTypes(pparserParser.FunTypesContext ctx);
/**
* Visit a parse tree produced by the {@code funKnowledge}
* labeled alternative in {@link pparserParser#begin}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitFunKnowledge(pparserParser.FunKnowledgeContext ctx);
/**
* Visit a parse tree produced by the {@code funActions}
* labeled alternative in {@link pparserParser#begin}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitFunActions(pparserParser.FunActionsContext ctx);
/**
* Visit a parse tree produced by the {@code funGoals}
* labeled alternative in {@link pparserParser#begin}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitFunGoals(pparserParser.FunGoalsContext ctx);
/**
* Visit a parse tree produced by the {@code funBrainWhere}
* labeled alternative in {@link pparserParser#iknow}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitFunBrainWhere(pparserParser.FunBrainWhereContext ctx);
/**
* Visit a parse tree produced by the {@code funBrain}
* labeled alternative in {@link pparserParser#iknow}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitFunBrain(pparserParser.FunBrainContext ctx);
/**
* Visit a parse tree produced by the {@code brainWithSemi}
* labeled alternative in {@link pparserParser#brain}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitBrainWithSemi(pparserParser.BrainWithSemiContext ctx);
/**
* Visit a parse tree produced by the {@code brainOptSemi}
* labeled alternative in {@link pparserParser#brain}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitBrainOptSemi(pparserParser.BrainOptSemiContext ctx);
/**
* Visit a parse tree produced by the {@code notlastAct}
* labeled alternative in {@link pparserParser#act}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitNotlastAct(pparserParser.NotlastActContext ctx);
/**
* Visit a parse tree produced by the {@code lastAct}
* labeled alternative in {@link pparserParser#act}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitLastAct(pparserParser.LastActContext ctx);
/**
* Visit a parse tree produced by the {@code funFromTo}
* labeled alternative in {@link pparserParser#w2w}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitFunFromTo(pparserParser.FunFromToContext ctx);
/**
* Visit a parse tree produced by the {@code regular}
* labeled alternative in {@link pparserParser#c}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitRegular(pparserParser.RegularContext ctx);
/**
* Visit a parse tree produced by the {@code star}
* labeled alternative in {@link pparserParser#c}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitStar(pparserParser.StarContext ctx);
/**
* Visit a parse tree produced by the {@code arrowstar}
* labeled alternative in {@link pparserParser#c}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitArrowstar(pparserParser.ArrowstarContext ctx);
/**
* Visit a parse tree produced by the {@code stararrowstar}
* labeled alternative in {@link pparserParser#c}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitStararrowstar(pparserParser.StararrowstarContext ctx);
/**
* Visit a parse tree produced by the {@code normal}
* labeled alternative in {@link pparserParser#w}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitNormal(pparserParser.NormalContext ctx);
/**
* Visit a parse tree produced by the {@code square}
* labeled alternative in {@link pparserParser#w}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitSquare(pparserParser.SquareContext ctx);
/**
* Visit a parse tree produced by the {@code squaremess}
* labeled alternative in {@link pparserParser#w}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitSquaremess(pparserParser.SquaremessContext ctx);
/**
* Visit a parse tree produced by the {@code wscomma}
* labeled alternative in {@link pparserParser#ws}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitWscomma(pparserParser.WscommaContext ctx);
/**
* Visit a parse tree produced by the {@code wsnocomma}
* labeled alternative in {@link pparserParser#ws}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitWsnocomma(pparserParser.WsnocommaContext ctx);
/**
* Visit a parse tree produced by the {@code waisingle}
* labeled alternative in {@link pparserParser#wai}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitWaisingle(pparserParser.WaisingleContext ctx);
/**
* Visit a parse tree produced by the {@code waimore}
* labeled alternative in {@link pparserParser#wai}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitWaimore(pparserParser.WaimoreContext ctx);
/**
* Visit a parse tree produced by the {@code mnocomma}
* labeled alternative in {@link pparserParser#m}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitMnocomma(pparserParser.MnocommaContext ctx);
/**
* Visit a parse tree produced by the {@code mcomma}
* labeled alternative in {@link pparserParser#m}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitMcomma(pparserParser.McommaContext ctx);
/**
* Visit a parse tree produced by the {@code normfunction}
* labeled alternative in {@link pparserParser#norm}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitNormfunction(pparserParser.NormfunctionContext ctx);
/**
* Visit a parse tree produced by the {@code normnoenc}
* labeled alternative in {@link pparserParser#norm}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitNormnoenc(pparserParser.NormnoencContext ctx);
/**
* Visit a parse tree produced by the {@code normenc}
* labeled alternative in {@link pparserParser#norm}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitNormenc(pparserParser.NormencContext ctx);
/**
* Visit a parse tree produced by the {@code normvariable}
* labeled alternative in {@link pparserParser#norm}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitNormvariable(pparserParser.NormvariableContext ctx);
/**
* Visit a parse tree produced by the {@code normparenth}
* labeled alternative in {@link pparserParser#norm}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitNormparenth(pparserParser.NormparenthContext ctx);
/**
* Visit a parse tree produced by the {@code limore}
* labeled alternative in {@link pparserParser#li}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitLimore(pparserParser.LimoreContext ctx);
/**
* Visit a parse tree produced by the {@code lisingle}
* labeled alternative in {@link pparserParser#li}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitLisingle(pparserParser.LisingleContext ctx);
/**
* Visit a parse tree produced by the {@code goalsmore}
* labeled alternative in {@link pparserParser#goals}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitGoalsmore(pparserParser.GoalsmoreContext ctx);
/**
* Visit a parse tree produced by the {@code goalssingle}
* labeled alternative in {@link pparserParser#goals}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitGoalssingle(pparserParser.GoalssingleContext ctx);
/**
* Visit a parse tree produced by the {@code secretbetween}
* labeled alternative in {@link pparserParser#g}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitSecretbetween(pparserParser.SecretbetweenContext ctx);
/**
* Visit a parse tree produced by the {@code weaklyauthent}
* labeled alternative in {@link pparserParser#g}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitWeaklyauthent(pparserParser.WeaklyauthentContext ctx);
/**
* Visit a parse tree produced by the {@code authent}
* labeled alternative in {@link pparserParser#g}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitAuthent(pparserParser.AuthentContext ctx);
/**
* Visit a parse tree produced by the {@code arrowmsg}
* labeled alternative in {@link pparserParser#g}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitArrowmsg(pparserParser.ArrowmsgContext ctx);
/**
* Visit a parse tree produced by the {@code typesoptsemi}
* labeled alternative in {@link pparserParser#whattype}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitTypesoptsemi(pparserParser.TypesoptsemiContext ctx);
/**
* Visit a parse tree produced by the {@code typesemi}
* labeled alternative in {@link pparserParser#whattype}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitTypesemi(pparserParser.TypesemiContext ctx);
/**
* Visit a parse tree produced by the {@code csepsingle}
* labeled alternative in {@link pparserParser#csep}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitCsepsingle(pparserParser.CsepsingleContext ctx);
/**
* Visit a parse tree produced by the {@code csepmore}
* labeled alternative in {@link pparserParser#csep}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitCsepmore(pparserParser.CsepmoreContext ctx);
/**
* Visit a parse tree produced by the {@code ag}
* labeled alternative in {@link pparserParser#types}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitAg(pparserParser.AgContext ctx);
/**
* Visit a parse tree produced by the {@code nu}
* labeled alternative in {@link pparserParser#types}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitNu(pparserParser.NuContext ctx);
/**
* Visit a parse tree produced by the {@code seq}
* labeled alternative in {@link pparserParser#types}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitSeq(pparserParser.SeqContext ctx);
/**
* Visit a parse tree produced by the {@code pk}
* labeled alternative in {@link pparserParser#types}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitPk(pparserParser.PkContext ctx);
/**
* Visit a parse tree produced by the {@code symk}
* labeled alternative in {@link pparserParser#types}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitSymk(pparserParser.SymkContext ctx);
/**
* Visit a parse tree produced by the {@code func}
* labeled alternative in {@link pparserParser#types}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitFunc(pparserParser.FuncContext ctx);
/**
* Visit a parse tree produced by the {@code unt}
* labeled alternative in {@link pparserParser#types}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitUnt(pparserParser.UntContext ctx);
}

Some files were not shown because too many files have changed in this diff Show More