Starting cmake conversion

.gitignore

@@ -13,7 +13,7 @@ TAGS
 *.sum
 *.plist
 *.dSYM
-config.h.in
+# config.h.in Removed for cmake compilation
 .libs/
 .metadata/
 .project
@@ -67,3 +67,20 @@ testsuite/wine.exp
 /examples/*.lps
 /examples/abp.pbes
 nbproject
+
+#Build files
+build/*
+
+# Cmake files
+CMakeLists.txt.user
+CMakeCache.txt
+CMakeFiles
+CMakeScripts
+Testing
+Makefile
+cmake_install.cmake
+install_manifest.txt
+compile_commands.json
+CTestTestfile.cmake
+_deps
+

CMakeLists.txt

@@ -0,0 +1,149 @@
+cmake_minimum_required(VERSION 3.21)
+
+
+
+project(ltsmin 
+    VERSION 3.0.3
+    DESCRIPTION "TODO"
+    HOMEPAGE_URL "https://github.com/utwente-fmt/ltsmin"
+    LANGUAGES C CXX
+)
+
+Set(CMAKE_CXX_STANDARD 11)
+Set(CMAKE_CXX_STANDARD_REQUIRED True)
+set(PACKAGE_STRING "${CMAKE_PROJECT_NAME} ${CMAKE_PROJECT_VERSION}")
+set(PACKAGE_BUGREPORT "[email protected]")
+include(CTest)
+set(CMAKE_MODULE_PATH cmake_modules/)
+
+# update submodules:
+find_package(Git QUIET)
+if(GIT_FOUND AND EXISTS "${PROJECT_SOURCE_DIR}/.git")
+# Update submodules as needed
+    option(GIT_SUBMODULE "Check submodules during build" ON)
+    if(GIT_SUBMODULE)
+        message(STATUS "Submodule update")
+        execute_process(COMMAND ${GIT_EXECUTABLE} submodule update --init --recursive
+                        WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR}
+                        RESULT_VARIABLE GIT_SUBMOD_RESULT)
+        if(NOT GIT_SUBMOD_RESULT EQUAL "0")
+            message(FATAL_ERROR "git submodule update --init --recursive failed with ${GIT_SUBMOD_RESULT}, please checkout submodules")
+        endif()
+    endif()
+endif()
+
+if(NOT EXISTS "${PROJECT_SOURCE_DIR}/ltl2ba/CMakeLists.txt" OR 
+   NOT EXISTS "${PROJECT_SOURCE_DIR}/scoop/Makefile.am" OR
+   NOT EXISTS "${PROJECT_SOURCE_DIR}/spins/spins.sh")
+    message(FATAL_ERROR "The submodules were not downloaded! GIT_SUBMODULE was turned off or failed. Please update submodules and try again.")
+endif()
+
+
+
+
+
+
+###### CONFIGURATION ######
+
+#check OS https://gitlab.kitware.com/cmake/community/-/wikis/doc/tutorials/How-To-Write-Platform-Checks
+    if (WIN32)
+        set(_WIN32 ON)
+    elseif (UNIX)
+        set(__linux__ ON)
+    elseif (${CMAKE_SYSTEM_NAME} MATCHES "Darwin")
+        set(_APPLE_ ON)
+    else ()
+        message(FATAL_ERROR "OS not accounted for in this program")
+    endif()
+
+
+
+configure_file(${PROJECT_SOURCE_DIR}/config.h.in ${PROJECT_SOURCE_DIR}/ltl2ba/config.h)
+
+####### cmake configuration output ######
+#This will output which modules are active when executing the cmake command 
+message("cmake configuration:")
+message("====================")
+###ASCIIDOC
+    #TODO check if this actually finds asciidoc
+    find_program(ASCIIDOC asciidoc)
+    string(COMPARE NOTEQUAL ${ASCIIDOC} "ASCIIDOC-NOTFOUND" have_asciidoc)
+    if(${have_asciidoc})
+        message("ASCIIDOC = ON")
+    else()
+        message("ASCIIDOC = NOT FOUND. Asciidoc is needed for building documentation.")
+    endif()
+###BIGNUM
+    #TODO: implement some kind of check here
+    option(with_bignum "variable to disable bignum" ON)
+    message("BIGNUM = ${with_bignum}")
+###BUDDY
+###CADP
+###CC
+###CXX
+###LIBDDD
+###MCRL
+###MCRL2
+###MPICC
+###MPICXX
+###OPAAL
+###PBES
+###SCOOP
+###SPINS
+###SPOT
+
+
+    option(without-spot "variable to disable spot" ON) #TODO when find_package(SPOT) works. Then change option default value to OFF
+    message(${without-spot})
+    if(${without-spot})
+        set(have_spot OFF)
+    else()
+        #TODO: Implement a FindSPOT.cmake in CMAKE_MODULE_PATH.
+        message("TODO: Implement a FindSPOT.cmake in CMAKE_MODULE_PATH.")
+        find_package(SPOT)
+        #TODO: have_spot should depend if the package was found or not
+        set(have_spot ON)
+    endif()
+
+    if(${have_spot})
+        message("SPOT = ON. (override with -Dwithout-spot)")
+    else()
+        message("SPOT = OFF. Spot not found, or disabled")
+    endif()
+###XMLTO
+###BOOST
+###VIENNACL
+###PNML
+###PROB
+###SDD
+###SYLVAN
+
+    option(without-sylvan "variable to disable sylvan" OFF)
+    if(${without-sylvan})
+        set(SYLVAN_FOUND OFF)
+    else()
+        find_package(LACE)
+        find_package(SYLVAN)
+        #set( ON)
+    endif()
+
+    if(${SYLVAN_FOUND})
+        set(HAVE_SYLVAN ON)
+        message("SYLVAN = ON. (override with -Dwithout-sylvan=1)")
+    else()
+        message("SYLVAN = OFF. SYLVAN not found, or disabled")
+    endif()
+message("====================")
+
+
+#TODO add options for examples, tests and documentation
+
+
+##### MAKE PROJECT
+#TODO get sylvan(?) via FetchContent? or make it a submodule
+add_subdirectory(src)
+add_subdirectory(lib)
+add_subdirectory(lemon)
+add_subdirectory(ltl2ba)
+
+

Conversion-to-cmake.txt

@@ -0,0 +1,66 @@
+TODO make hint about:
+    vector_set.c:(.text+0x1199): undefined reference to `bn_init'
+    ./src/bignum/bignum.h:35:extern void         bn_init_copy (bn_int_t *a, bn_int_t *b);
+
+GENERAL NOTES:
+- TODO: Check if flex installation in install script (install.sh) is good enough. Maybe a make error? If no error when running make, delete this note.
+- root/lib should not be necessary with cmake, as it is used to increase portability between systems. Cmake should be able to do that itself. https://cmake.org/pipermail/cmake/2018-January/066885.html
+    - Files that might be needed from root/lib: verify.h
+- TODO: find a way to get CACHE_LINE_SIZE, CACHE_LINE & LTSMIN_PATHNAME_MAX and specify it in src/hre/config.h.in
+    -TODO in src/hre/config.h.in figure out a way "__assume(cond)" should be define with cmakedefine
+    - TODO in src/hre/config.h.in what to do with /* Enable GNU extensions on systems that have them.  */
+NEW DEPENDENCIES?
+    - LTDL was given with automake in src/m4/ltdl.m4. cmake can't use this. an other dependency is needed. As standard i think linux comes with an ltdl library
+- CMAKE TUTORIAL: to configure the project you can define cmake variables in the command line. Example: "cmake .. -DWITH_SPINS=1" defines the WITH_SPINS variable to be 1.
+    - It saves the definition in a cache. That means if you in the future do not want WITH_SPINS defined, then you need to delete the build folder
+- CMAKE find_package(X): the mcr project has multiple findX files in the cmake folder (https://github.com/alaarman/mcf)
+----------------root-----------------
+
+
+---------------src/hre----------------
+    TODO: FILE:git_version.h is generated. Figure our how
+    config.h.in need to use #cmakedefine in order for cmake to create the config.h dynamically. You need to SET(__linux__ ON) at some point in order for __linux__ to be defined.
+    TODO: FILE:config.h.in Right now __linux__ is hard coded: make a way to dynamically check and set operating system version. I don't know where it is done in the automake version
+    TODO: FILE:config.h.in check if  _GNU_SOURCE is defined correctly 
+
+
+---------------src/ce---------------- OPTIONAL
+    TODO: this is not done. is an optional modules that only is create if HAVE_CE is ON.
+
+---------------src/ltmin-libs----------------
+    .lemon and .l files are used for generation of .c and .h files with lemon and flex
+    TODO: It looks like on the old automake code that generating lex files is optional. Look into this.
+
+
+---------------lemon---------------------
+    Lemon is used to generate files from .lemon files (eg. src/ltsmin-libs/ltsmin-grammar.lemon)
+    It uses lempar.c to generate these files, BUT not a compiled version of lempar.c. Therefore lempar.c is copied into the binary directory. I'm unsure if this is the best approach
+
+---------------ltl2ba--------------------
+    NOTE: root/ltl2ba/config.h file is created with the root/config.h.in. This file is currently empty. Unsure if it's needed.
+        SUGGESTION: this config.h should maybe be the same as root/src/hre/config.h
+
+---------------src/pins-lib: --------------------
+
+---------------src/pins2lts-sym---------------------
+    TODO MISSING IMPLEMENTATION: lpo2lts-sym
+    TODO MISSING IMPLEMENTATION: lps2lts-sym
+    TODO MISSING IMPLEMENTATION: mapa2lts-sym
+    TODO MISSING IMPLEMENTATION: pbe2lts-sym
+    TODO MISSING IMPLEMENTATION: prom2lts-sym
+    TODO MISSING IMPLEMENTATION: prob2lts-sym
+
+---------------src/vset-lib---------------------
+    Note: a lot of optional content. I've tried to copy the options from the automake script
+
+---------------src/util-lib---------------------
+    TODO: Unsure if util-lib should link to hre
+---------------src/dm---------------------
+    TODO: In the Makefile.am there is specified a debug and nonddebug library. MAYBE CHANGE SO CMAKE HAS DEBUG AND NON-DEBUG
+----------------src/bignum
+    TODO: implement variablity in #if defined(HAVE_GMP_H) and #elif defined(HAVE_TOMMATH_H)
+---------------src/---------------------
+
+
+
+

install_on_ubuntu.sh

@@ -0,0 +1,47 @@
+#!/bin/bash
+
+# Update
+sudo apt update -y
+sudo apt upgrade -y
+
+# Required dependencies when installing from github:
+sudo apt install git -y
+sudo apt install make -y
+sudo apt install automake -y
+sudo apt install libtool -y
+sudo apt install flex -y
+sudo apt install bison -y
+sudo apt install pkgconf -y
+sudo apt install cmake -y
+
+# Required dependencies
+sudo apt install libpopt-dev -y
+sudo apt install zlib1g-dev -y
+sudo apt install openjdk-11-jdk -y
+sudo apt install ant -y
+
+########################### install sylvan & sylvan dependencies #############################
+#TODO: make sylvan a submodule
+sudo apt install libgmp-dev -y
+sudo apt install libhwloc-dev -y
+git clone https://github.com/Codermann63/sylvan.git
+cd sylvan
+mkdir build
+cd build
+cmake ..
+make
+sudo make install
+cd ../..
+
+########################## PNML dependencies ##############################
+sudo apt install xml2 -y
+sudo apt install libxml2-dev -y
+
+################################# install LTSMIN from github #################################
+git clone https://github.com/utwente-fmt/ltsmin.git
+cd ltsmin
+git submodule update --init
+./ltsminreconf
+./configure
+make
+sudo make install

lemon/CMakeLists.txt

@@ -0,0 +1,8 @@
+cmake_minimum_required(VERSION 3.12)
+
+
+add_executable(lemon lemon.c)
+
+#lemon needs lempar.c to generate .lemons files. lempar.c is a templatefile and should not be compiled, just copied to the binaries
+file(COPY ${CMAKE_CURRENT_SOURCE_DIR}/lempar.c
+     DESTINATION ${CMAKE_CURRENT_BINARY_DIR})

lib/CMakeLists.txt

@@ -0,0 +1,17 @@
+
+add_library(general-lib STATIC write.c)
+
+target_sources(general-lib
+    PUBLIC
+    verify.h)
+
+
+find_library(MATH_LIBRARY m REQUIRED)
+if(MATH_LIBRARY)
+    target_link_libraries(general-lib PUBLIC ${MATH_LIBRARY})
+endif()
+
+
+target_include_directories(general-lib PUBLIC ${CMAKE_CURRENT_SOURCE_DIR}
+                            ${CMAKE_SOURCE_DIR}/src/hre)
+add_dependencies(general-lib hre)

src/CMakeLists.txt

@@ -0,0 +1,44 @@
+# LIB DEPENDENCIES (transitive depends on relations)
+#
+# vset-lib  ---->  bignum-lib
+#    |
+#    |
+#    v
+#   HRE   <------>   HRE-IO
+#    ^
+#    |
+#    v
+# util-lib
+#    ^
+#    |
+#    |
+# ltsmin-lib  <--->  lts-io  <----  lts-lib 
+#    ^   ^
+#    |    \
+#    |     \
+#    |      \
+#    |      mc-lib
+#    |            \
+#    |             v
+# pins-lib  ---->  dm-lib
+#    
+#
+
+Option(have_ce "variable to check if CE is enabled" OFF) # TODO change when actual variability management has been made
+if (have_ce)
+    add_subdirectory(ce)
+endif()
+add_subdirectory(hre)
+add_subdirectory(pins-lib)
+add_subdirectory(ltsmin-lib)
+add_subdirectory(pins2lts-sym)
+add_subdirectory(vset-lib)
+add_subdirectory(util-lib)
+add_subdirectory(lts-io)
+add_subdirectory(dm)
+add_subdirectory(mc-lib)
+add_subdirectory(spg-lib)
+add_subdirectory(bignum)
+add_subdirectory(hre-io)
+add_subdirectory(andl-lib)
+add_subdirectory(tests)