Initial import

.gitignore

@@ -0,0 +1,2 @@
+/Debug/
+/Release/

.project

@@ -0,0 +1,27 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<projectDescription>
+	<name>MCheck</name>
+	<comment></comment>
+	<projects>
+	</projects>
+	<buildSpec>
+		<buildCommand>
+			<name>org.eclipse.cdt.managedbuilder.core.genmakebuilder</name>
+			<triggers>clean,full,incremental,</triggers>
+			<arguments>
+			</arguments>
+		</buildCommand>
+		<buildCommand>
+			<name>org.eclipse.cdt.managedbuilder.core.ScannerConfigBuilder</name>
+			<triggers>full,incremental,</triggers>
+			<arguments>
+			</arguments>
+		</buildCommand>
+	</buildSpec>
+	<natures>
+		<nature>org.eclipse.cdt.core.cnature</nature>
+		<nature>org.eclipse.cdt.core.ccnature</nature>
+		<nature>org.eclipse.cdt.managedbuilder.core.managedBuildNature</nature>
+		<nature>org.eclipse.cdt.managedbuilder.core.ScannerConfigNature</nature>
+	</natures>
+</projectDescription>

.settings/language.settings.xml

@@ -0,0 +1,25 @@
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<project>
+	<configuration id="cdt.managedbuild.config.gnu.exe.debug.866248684" name="Debug">
+		<extension point="org.eclipse.cdt.core.LanguageSettingsProvider">
+			<provider copy-of="extension" id="org.eclipse.cdt.ui.UserLanguageSettingsProvider"/>
+			<provider-reference id="org.eclipse.cdt.core.ReferencedProjectsLanguageSettingsProvider" ref="shared-provider"/>
+			<provider-reference id="org.eclipse.cdt.managedbuilder.core.MBSLanguageSettingsProvider" ref="shared-provider"/>
+			<provider class="org.eclipse.cdt.managedbuilder.language.settings.providers.GCCBuiltinSpecsDetector" console="false" env-hash="137140326719343593" id="org.eclipse.cdt.managedbuilder.core.GCCBuiltinSpecsDetector" keep-relative-paths="false" name="CDT GCC Built-in Compiler Settings" parameter="${COMMAND} ${FLAGS} -E -P -v -dD &quot;${INPUTS}&quot;" prefer-non-shared="true">
+				<language-scope id="org.eclipse.cdt.core.gcc"/>
+				<language-scope id="org.eclipse.cdt.core.g++"/>
+			</provider>
+		</extension>
+	</configuration>
+	<configuration id="cdt.managedbuild.config.gnu.exe.release.1384844544" name="Release">
+		<extension point="org.eclipse.cdt.core.LanguageSettingsProvider">
+			<provider copy-of="extension" id="org.eclipse.cdt.ui.UserLanguageSettingsProvider"/>
+			<provider-reference id="org.eclipse.cdt.core.ReferencedProjectsLanguageSettingsProvider" ref="shared-provider"/>
+			<provider-reference id="org.eclipse.cdt.managedbuilder.core.MBSLanguageSettingsProvider" ref="shared-provider"/>
+			<provider class="org.eclipse.cdt.managedbuilder.language.settings.providers.GCCBuiltinSpecsDetector" console="false" env-hash="137140326719343593" id="org.eclipse.cdt.managedbuilder.core.GCCBuiltinSpecsDetector" keep-relative-paths="false" name="CDT GCC Built-in Compiler Settings" parameter="${COMMAND} ${FLAGS} -E -P -v -dD &quot;${INPUTS}&quot;" prefer-non-shared="true">
+				<language-scope id="org.eclipse.cdt.core.gcc"/>
+				<language-scope id="org.eclipse.cdt.core.g++"/>
+			</provider>
+		</extension>
+	</configuration>
+</project>

LICENSE

@@ -0,0 +1,19 @@
+Copyright (c) 2016, Niklas Gürtler
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without modification, are permitted provided that the
+following conditions are met:
+
+1. Redistributions of source code must retain the above copyright notice, this list of conditions and the following
+   disclaimer.
+
+2. Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the
+   following disclaimer in the documentation and/or other materials provided with the distribution.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES,
+INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
+DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
+SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY,
+WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

README.md

@@ -0,0 +1,68 @@
+# MCheck - Simple implementation of a model checking algorithm using CTL formulae
+This is a simple C++ based application that parses CTL formulae, descriptions of transition systems, and checks whether the systems satisfy the formulae. Both the formulae and the transision systems are parsed using the [Boost.Spirit](http://boost-spirit.com) Parser library. It is written in Standard C++ and runs on both Windows and Linux.
+## Syntax
+The syntax for transistion system descriptions is a simple subset of the language used by the [Graphviz dot](http://www.graphviz.org/) graph plotting application, which allows to easily plot the system. An example transition system is:
+```
+digraph G {
+	S0 -> S1
+	S1 -> S2
+	S2 -> S0
+	
+	S0 [label = "S0: r", shape="box"]
+	S1 [label = "r,y"]
+	S2 [label = "S2: g"]
+}
+```
+The lines 2-4 define some states and transitions. The lines 6-8 define additional attributes for the states. The label is used by graphviz for displaying, and used by MCheck to define the atomic propositions. The part up to and including the colon is optional and ignored by MCheck. The remainder should be a comma-seperated list of propositions, each being a C-like identifier. Nodes whose shape is defined as "box" are assumed as initial states.
+Transistion systems descriptions are saved in ordinary text files and passed to MCheck.
+
+CTL Formulae look like this:
+```
+∀ ⬜ (y → (∀ X g))
+∃ ⬜ ∃(r U (∀X y))
+```
+Unicode UTF-8 characters are used for the operators. The following syntax elements are defined (Φ,Ψ are placeholders for sub-formulae):
+
+Form | Description
+-----|------------
+true/false | Boolean literals
+¬Φ | Negation
+Φ∧Ψ | Logical And
+Φ∨Ψ | Logical Or
+Φ→Ψ | Logical implication
+∃XΦ | Exists next
+∃(Φ U Ψ) | Exists until
+∃⬜Φ | Exists always
+∀XΦ|For all next
+∀(Φ U Ψ) | For all until
+∀⬜Φ | For all always
+
+Formulae are input via simple text files, one formula per line. The text files must be encoded as UTF-8, without a byte order mark. Therefore, Windows notepad can not be used.
+
+## Usage
+MCheck is a console application, run it as:
+```shell
+MCheck TransitionSystem.txt Formulae.txt
+```
+Where TransitionSystem.txt contains a description of a transition system, and Formulae.txt one or more CTL formulae. Since the Windows Console does not support UTF-8 output, output can be redirected to a file which can then be displayed by a text editor to view the unicode characters:
+```shell
+MCheck TransitionSystem.txt Formulae.txt > Result.txt
+```
+
+An example output is
+```
+∀ ⬜ (y → (∀ X g))
+Is satisfied
+Sat (∀ ⬜ (y → (∀ X g))) = {S0, S1, S2}
+	Sat (y → (∀ X g)) = {S0, S1, S2}
+		Sat (y) = {S1}
+		Sat (∀ X g) = {S1}
+			Sat (g) = {S2}
+```
+Each computed formulae are printed, followed by the computation result, and its syntax tree. Each sub-formula is annotated with the set of states satisfying it.
+
+## Download
+The [Releases](https://github.com/Erlkoenig90/MCheck/releases) page provides binaries for Windows and Linux. You can also download the source and compile it using eclipse and GCC or MSVC.
+
+## License
+This is an open source project licensed under the terms of the BSD license. See the [LICENSE file](LICENSE) for details.

src/ctl/ast.cc

@@ -0,0 +1,86 @@
+/*
+ * Copyright (c) 2016, Niklas Gürtler
+ * All rights reserved.
+ * 
+ * Redistribution and use in source and binary forms, with or without modification, are permitted provided that the
+ * following conditions are met:
+ * 
+ * 1. Redistributions of source code must retain the above copyright notice, this list of conditions and the following
+ *    disclaimer.
+ * 
+ * 2. Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the
+ *    following disclaimer in the documentation and/or other materials provided with the distribution.
+ * 
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES,
+ * INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
+ * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+ * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
+ * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY,
+ * WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ */
+
+#include "ast.hh"
+
+namespace CTL {
+std::ostream& operator<< (std::ostream& os, const E_Literal& l) {
+	os << "E_Literal {" << std::boolalpha << l.value << "}";
+    return os;
+}
+
+std::ostream& operator<< (std::ostream& os, const E_Label& l) {
+	os << "E_Label {\"" << l.name << "\"}";
+    return os;
+}
+
+std::ostream& operator<< (std::ostream& os, const E_Negation& l) {
+	os << "E_Negation {" << l.exp << "}";
+    return os;
+}
+
+std::ostream& operator<< (std::ostream& os, const E_And& a) {
+	os << "E_And {" << a.lhs << ", " << a.rhs << "}";
+    return os;
+}
+
+std::ostream& operator<< (std::ostream& os, const E_Or& a) {
+	os << "E_Or {" << a.lhs << ", " << a.rhs << "}";
+    return os;
+}
+
+std::ostream& operator<< (std::ostream& os, const E_Implication& a) {
+	os << "E_Implication {" << a.lhs << ", " << a.rhs << "}";
+    return os;
+}
+
+std::ostream& operator<< (std::ostream& os, const E_ExistNext& a) {
+	os << "E_ExistNext {" << a.exp << "}";
+    return os;
+}
+
+std::ostream& operator<< (std::ostream& os, const E_ExistUntil& a) {
+	os << "E_ExistUntil {" << a.lhs << ", " << a.rhs << "}";
+    return os;
+}
+
+std::ostream& operator<< (std::ostream& os, const E_ExistAlways& a) {
+	os << "E_ExistAlways {" << a.exp << "}";
+    return os;
+}
+
+std::ostream& operator<< (std::ostream& os, const E_AllNext& a) {
+	os << "E_AllNext {" << a.exp << "}";
+    return os;
+}
+
+std::ostream& operator<< (std::ostream& os, const E_AllUntil& a) {
+	os << "E_AllUntil {" << a.lhs << ", " << a.rhs << "}";
+    return os;
+}
+
+std::ostream& operator<< (std::ostream& os, const E_AllAlways& a) {
+	os << "E_AllAlways {" << a.exp << "}";
+    return os;
+}
+
+}