Merge pull request #44 from sillydan1/feat/detcheck

Version v1.1.0 - detcheck and cpp parsers

.github/workflows/cmake.yml

@@ -21,7 +21,7 @@ jobs:
     - name: checkout repository
       uses: actions/checkout@v2
     - name: install dependencies
-      run: sudo apt-get install -y flex bison make m4 cmake
+      run: sudo apt-get install -y flex bison make m4 cmake libfl-dev libbison-dev
     - name: create build environment
       run: cmake -E make_directory ${{ github.workspace }}/build
     - name: configure

launch.json → .vscode/launch.json

@@ -1,17 +1,26 @@
 {
     "version": "0.2.0",
     "configurations": [
+        {
+            "name": "launch unit tests",
+            "type": "codelldb",
+            "request": "launch",
+            "cwd": "${workspaceFolder}/Debug",
+            "program": "${workspaceFolder}/Debug/aaltitoad_tests",
+            "args": [
+            ]
+        },
         {
             "name": "Launch Verifier",
             "type": "codelldb",
             "request": "launch",
             "program": "${workspaceFolder}/Debug/verifier",
+            "cwd": "${workspaceFolder}/Debug",
             "args": [ 
                 "-f", "../test/verification/fischer-suite/fischer-2/",
                 "-q", "../test/verification/fischer-suite/fischer-2/Queries.json",
                 "-i", ".*\\.ignore.*"
-            ],
-            "cwd": "${workspaceFolder}/Debug"
+            ]
         }
     ]
 }

CMakeLists.txt

@@ -14,25 +14,28 @@
 #   You should have received a copy of the GNU General Public License
 #   along with this program.  If not, see <https://www.gnu.org/licenses/>.
 cmake_minimum_required(VERSION 3.16) # 3.16+ because of target_precompiled_header
-project(aaltitoad VERSION 1.0.0)
+project(aaltitoad VERSION 1.1.0)
 set(THREADS_PREFER_PTHREAD_FLAG ON)
 set(CMAKE_CXX_STANDARD 20)
 set(CXX_STANDARD_REQUIRED ON)
 set(SPDLOG_BUILD_SHARED)
 set(CONFIG_IN_FILE src/config.h.in)
 set(CONFIG_OUT_FILE config.h)
 include(cmake/CPM.cmake)
-include(cmake/VER.cmake) # TODO: make a yalibs release of this cmake file
+include(cmake/VER.cmake) # TODO: yalibs candidate 
 set(CMAKE_ARCHIVE_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/lib)
 set(CMAKE_LIBRARY_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/lib)
 set(CMAKE_RUNTIME_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR})
 set(CMAKE_MACOSX_RPATH 1)
 list(APPEND CMAKE_INSTALL_RPATH ${CMAKE_INSTALL_PREFIX}/lib)
 
+find_package(BISON REQUIRED)
+find_package(FLEX REQUIRED)
+
 add_compile_definitions(DEFAULT_EXPRESSION_VALUE="true")
-CPMAddPackage(NAME expr VERSION 2.2.0 GITHUB_REPOSITORY sillydan1/expr OPTIONS "ENABLE_Z3 ON")
+CPMAddPackage(NAME expr VERSION 3.0.0 GITHUB_REPOSITORY sillydan1/expr OPTIONS "ENABLE_Z3 ON")
 CPMAddPackage("gh:sillydan1/[email protected]")
-CPMAddPackage("gh:sillydan1/ctl-expr@1.1.2")
+CPMAddPackage("gh:sillydan1/ctl-expr@2.0.0")
 
 CPMAddPackage("gh:yalibs/[email protected]")
 CPMAddPackage("gh:yalibs/[email protected]")
@@ -44,14 +47,17 @@ CPMAddPackage("gh:yalibs/[email protected]")
 CPMAddPackage("gh:yalibs/[email protected]")
 CPMAddPackage("gh:yalibs/[email protected]")
 
-CPMAddPackage("gh:gabime/spdlog@1.8.2")
-CPMAddPackage("gh:nlohmann/json@3.10.5")
-CPMAddPackage("gh:neargye/[email protected].1")
+CPMAddPackage("gh:gabime/spdlog@1.11.0")
+CPMAddPackage("gh:nlohmann/json@3.11.2")
+CPMAddPackage("gh:neargye/[email protected].2")
 
-CPMAddPackage("gh:cpm-cmake/[email protected].5")
+CPMAddPackage("gh:cpm-cmake/[email protected].6")
 cpm_licenses_create_disclaimer_target(write_licenses "${CMAKE_BINARY_DIR}/third_party.txt" "${CPM_PACKAGES}")
 
-set(${PROJECT_NAME}_SOURCES
+add_library(${PROJECT_NAME} SHARED 
+        src/expr-wrappers/interpreter.cpp
+        src/expr-wrappers/parameterized-expr-evaluator.cpp
+        src/expr-wrappers/parameterized-ast-factory.cpp
         src/ntta/builder/ntta_builder.cpp
         src/ntta/tta.cpp
         src/ntta/interesting_tocker.cpp
@@ -61,14 +67,11 @@ set(${PROJECT_NAME}_SOURCES
         src/util/warnings.cpp
         src/util/random.cpp
         src/util/string_extensions.cpp)
-
-# TODO: split the project up - each folder should have their own CMakeLists file
-add_library(${PROJECT_NAME} SHARED ${${PROJECT_NAME}_SOURCES})
 if(${CODE_COVERAGE})
     target_link_options(${PROJECT_NAME} PUBLIC --coverage)
     target_compile_options(${PROJECT_NAME} PUBLIC --coverage)
 endif()
-target_link_libraries(${PROJECT_NAME} expr dl pthread ctl)
+target_link_libraries(${PROJECT_NAME} PUBLIC expr_lang dl pthread ctl_lang)
 target_include_directories(${PROJECT_NAME} PUBLIC
         ${CMAKE_BINARY_DIR}
         ${CMAKE_CURRENT_BINARY_DIR}
@@ -96,15 +99,19 @@ target_include_directories(${PROJECT_NAME} PUBLIC
         ${yapermutation_SOURCE_DIR}/include
         ${yasetwrappers_SOURCE_DIR}/include
         src
+        # strictly not required, but it helps my clangd lsp setup and it doesn't hurt
+        ${FLEX_INCLUDE_DIRS}
+        ${BISON_INCLUDE_DIRS}
 )
 
 add_compile_definitions(ENABLE_Z3)
 add_subdirectory(src/cli/simulator)
 add_subdirectory(src/cli/verifier)
+add_subdirectory(src/cli/detcheck)
 add_subdirectory(src/parser)
 add_subdirectory(test)
 
-install(TARGETS ${PROJECT_NAME} expr ctl)
+install(TARGETS ${PROJECT_NAME} expr_lang ctl_lang verifier simulator detcheck)
 install(FILES src/man/tta.7 DESTINATION man/man7)
 if(CMAKE_SYSTEM_NAME STREQUAL "Linux")
     install(FILES ${CMAKE_BINARY_DIR}/libz3.so DESTINATION lib)
@@ -115,10 +122,9 @@ elseif(CMAKE_SYSTEM_NAME STREQUAL "Darwin")
 else()
     message(WARNING "unknown system ${CMAKE_SYSTEM_NAME}")
 endif()
-
-# TODO: determine required header files for plugins and add them to the install target
-#       install(DIRECTORY src/ntta src/plugin_system src/util DESTINATION include FILES_MATCHING PATTERN "*.h")
+install(DIRECTORY src/ntta src/plugin_system src/util src/verification src/parser DESTINATION include FILES_MATCHING PATTERN "*.h")
 
 if(NOT WIN32)
     target_precompile_headers(${PROJECT_NAME} PUBLIC src/aaltitoadpch.h)
 endif()
+

cmake/CPM.cmake

@@ -1,4 +1,4 @@
-set(CPM_DOWNLOAD_VERSION 0.36.0)
+set(CPM_DOWNLOAD_VERSION 0.38.0)
 
 if(CPM_SOURCE_CACHE)
   # Expand relative path. This is important if the provided path contains a tilde (~)

src/cli/cli_common.h

@@ -26,14 +26,14 @@
 
 int print_required_args() {
     std::cout << "Required arguments:\n";
-    std::cout << " --input\n";
+    std::cout << " --input / -f\n";
     return 1;
 }
 
 int print_help(const std::string& program_name, const std::vector<option_t>& options) {
     std::cout << get_license() << std::endl;
     std::cout << PROJECT_NAME << " v" << PROJECT_VER << std::endl;
-    std::cout << "USAGE: " << program_name << " -i /path/to/tta/dir [OPTIONS] \n" << std::endl;
+    std::cout << "USAGE: " << program_name << " -f /path/to/tta/dir [OPTIONS] \n" << std::endl;
     std::cout << "OPTIONS: " << std::endl;
     print_argument_help(options);
     return 0;

src/cli/detcheck/CMakeLists.txt

@@ -0,0 +1,25 @@
+# aaltitoad - a verification engine for tick tock automata models
+#   Copyright (C) 2023 Asger Gitz-Johansen
+#
+#    This program is free software: you can redistribute it and/or modify
+#    it under the terms of the GNU General Public License as published by
+#    the Free Software Foundation, either version 3 of the License, or
+#    (at your option) any later version.
+#
+#    This program is distributed in the hope that it will be useful,
+#    but WITHOUT ANY WARRANTY; without even the implied warranty of
+#    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+#    GNU General Public License for more details.
+#
+#    You should have received a copy of the GNU General Public License
+#    along with this program.  If not, see <https://www.gnu.org/licenses/>.
+#
+project(detcheck VERSION 1.0.0)
+find_package(argvparse REQUIRED)
+add_executable(${PROJECT_NAME} main.cpp)
+target_link_libraries(${PROJECT_NAME} aaltitoad argvparse)
+if(TARGET default_plugins)
+    add_dependencies(${PROJECT_NAME} default_plugins)
+endif()
+install(TARGETS ${PROJECT_NAME})
+

src/cli/detcheck/cli_options.h

@@ -0,0 +1,55 @@
+/**
+ * aaltitoad - a verification engine for tick tock automata models
+   Copyright (C) 2023 Asger Gitz-Johansen
+
+    This program is free software: you can redistribute it and/or modify
+    it under the terms of the GNU General Public License as published by
+    the Free Software Foundation, either version 3 of the License, or
+    (at your option) any later version.
+
+    This program is distributed in the hope that it will be useful,
+    but WITHOUT ANY WARRANTY; without even the implied warranty of
+    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+    GNU General Public License for more details.
+
+    You should have received a copy of the GNU General Public License
+    along with this program.  If not, see <https://www.gnu.org/licenses/>.
+ */
+#ifndef AALTITOAD_CLI_OPTIONS_H
+#define AALTITOAD_CLI_OPTIONS_H
+
+std::vector<option_t> get_options() {
+    return {
+            {"input",         'f', argument_requirement::REQUIRE_ARG,  "(Required) input folder containing diagram files to parse and simulate"},
+            {"version",       'V', argument_requirement::NO_ARG,       "Print version and exit"},
+            {"verbosity",     'v', argument_requirement::REQUIRE_ARG,  "Set verbosity level (6 for max verbosity)"},
+            {"ignore",        'i', argument_requirement::REQUIRE_ARG,  "Specify a file to ignore (-i file1 -i file2 for multiple files)"},
+            {"parser",        'p', argument_requirement::REQUIRE_ARG,  "Specify the parser to use"},
+            {"plugin-dir",    'P', argument_requirement::REQUIRE_ARG,  "Specify directories to look for parser plugins"},
+            {"instance",      'n', argument_requirement::REQUIRE_ARG,  "Specify tta instances to check"},
+            {"instance-file", 'N', argument_requirement::REQUIRE_ARG,  "Specify a json-encoded file containing tta instances to check"},
+            {"list-instances",'L', argument_requirement::NO_ARG,       "List available instances and exit"},
+
+            {"known",         'k', argument_requirement::REQUIRE_ARG,  "Specify known symbol declarations"},
+            {"known-file",    'K', argument_requirement::REQUIRE_ARG,  "Specify a json-encoded file containing known symbol declarations"},
+            {"condition",     'c', argument_requirement::REQUIRE_ARG,  "Specify a condition. This will be added to all bool checks"},
+            {"condition-file",'C', argument_requirement::REQUIRE_ARG,  "Specify a json-encoded file containing extra conditions"},
+    };
+}
+
+bool is_required(const std::string& s) {
+    if(s == "input")
+        return true;
+    return false;
+}
+
+bool is_required_provided(std::map<std::string, argument_t>& provided_args, const std::vector<option_t>& options) {
+    if(provided_args["version"])
+        return true;
+    for(auto& opt : options) {
+        if(is_required(opt.long_option) && !provided_args[opt.long_option])
+            return false;
+    }
+    return true;
+}
+#endif //AALTITOAD_CLI_OPTIONS_H