Bewerter von struktureller Induktion

Automatische Bewertung von struktureller Induktion auf abstrakten Datentypen

Kompilieren des Programms

Das Programm kann mit .NET oder mit Mono kompiliert werden.

Komplilieren mit .NET

.NET kann auf jedem Betriebssystem installiert werden. Die kompilierte ausführbare Datei funktioniert Plattformunabhängig, solange die entsprechende .NET-Version installiert ist.

1. Installieren Sie .NET Version 6.0 oder höher.
2. Navigieren Sie mit der Konsole in den Ordner der .csproj-Datei
3. Rufen Sie dotnet build auf. Der Kompiler findet automatisch die .csproj-Datei und kompiliert das Projekt entsprechend dieser Konfiguration.

Kompilieren mit Mono

Wenn Sie das Projekt mit Mono kompilieren möchten, gibt es eine Diskussion auf Stackoverflow, die Ihnen dabei behilflich sein kann. Aus der Diskussion geht heraus, dass die Werkzeuge MonoDevelop oder auch xbuild verwendet werden können, um Visual Studio Projekte mit Mono zu kompilieren.

Zwei Programmeinstiegsmöglichkeiten

Es gibt zwei Programmeinstiegsmöglichkeiten für das Programm:

1. ProgramForHuman ist die Version des Programms, dessen Benutzerschnittstelle für die menschliche Verwendung optimiert ist. Wenn Sie diese Version kompilieren möchten, ersetzen Sie vor dem Kompilieren in der .csproj-Datei alle Vorkommen von "Yapex" durch "Human".

2. ProgramForYapex ist die Version des Programms, die eine optimale Schnittstelle für Yapex implementiert.

Verwendung des Programms

Bevor Sie das Programm verwenden, stellen Sie sicher für welche Version Sie das Programm kompiliert haben.

Version für Yapex

Alle Eingaben werden über die Argumente des Programms getätigt. Die Eingaben können in beliebiger Reihenfolge getätigt werden.

• ADT: Pfad zur Datei mit Endung .adt .
• Aufgabenstellung: Pfad zur Datei mit Endung .task .
• Beweis: Pfad zur Datei mit Endung .proof .
• Konfiguration: Pfad zur Datei mit Endung .config . Diese Eingabe ist optional. Ohne Eingabe der Konfigurationsdatei wird die Standardkonfiguration verwendet.
• Nur Syntax- und Namensanalyse: Option: "-checkSyntaxOnly" (Wenn Sie einen Syntax-check ohne Namensanalyse wünschen, installieren Sie ANTLR 4 und rufen Sie ANTLR auf, wie in Test_Parsers.bat)

Verhalten des Programms

• Wenn ein Pfad zu einer Datei nicht korrekt ist, wird das Programm mit einer entsprechenden Ausnahme unterbrochen.
• Wenn ADT / Task nicht erstellt werden können, hält das Programm mit ExitCode 0. Fehlermeldung wird in Konsole ausgegeben.
• Wenn Proof nicht erstellt werden kann, hält das Programm mit ExitCode 1. Fehlermeldung wird in Konsole ausgegeben.
• Bei Bewertung mit 0 Punkten hält das Programm mit ExitCode 1, sonst ExitCode 0.
• Mit der Option "-checkSyntaxOnly" wird nur versucht das Modell zu erstellen. Die eigentliche Überprüfung und Bewertung wird ausgelassen.
• Die Ausgabe der Bewertung und Überprüfung erfolgt auf die Konsole.

Version für Mensch

Es gibt meherere Möglichkeiten das Programm zu verwenden

1. Keine Argumente. Das Programm fragt interaktiv nach den Pfaden zu ADT / Task / Proof und führt anschließend eine Überprüfung und Bewertung durch.
2. Argument debug. Es wird eine interaktive Shell geöffnet. Mit ? können die Eingabemöglichkeiten angefragt werden.
3. Es werden drei Pfade über die Argumente angegeben: 1. ADT 2. Task 3. Proof. Das Programm führt eine Überprüfung und Bewertung durch.

• Konfiguration erfolgt über die Datei .config, die auch im selben Ordner liegen muss wie die ausführbare Datei.
• Die Ausgabe des Programms ist in der Datei Automatische_Bewertung.txt, die in den selben Ordner generiert wird.
• Tritt ein Fehler bei der Erstellung des Modells auf, so wird der Fehler ausgegeben und ein erneuter Eingabeversuch wird gestartet.

Beispiele

• Die Beispiele in ANTRL-Grammatiken sind teilweise für ältere Versionen der Grammatik konzepiert und können inkompatibel zur aktuellen Version der Grammatik sein.
• Alle Beispiele in den Tests funktionieren immer mit dem neuesten Stand der Grammatik und funktionieren auch mit der Yapex-Version.