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](https://dotnet.microsoft.com/en-us/download/dotnet) Version 3.1 oder höher.
2. Navigieren Sie mit der Konsole in den Ordner der [.csproj](BaumtransformationBewerter/BaumtransformationBewerter.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](https://stackoverflow.com/questions/8264323/how-to-compile-a-visual-studio-c-sharp-project-with-mono),
die Ihnen dabei behilflich sein kann. Aus der Diskussion geht heraus, dass die
Werkzeuge [MonoDevelop](https://www.monodevelop.com/) oder auch
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](BaumtransformationBewerter/ProgramForHuman.cs) 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](BaumtransformationBewerter/ProgramForYapex.cs) 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](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](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](BaumtransformationBewerter/bin/Debug/netcoreapp3.1/Tests) funktionieren immer mit dem neuesten Stand der Grammatik und funktionieren auch mit der Yapex-Version.
