From 3a75778e64abd2bfa76c094196fc29719c01a6d4 Mon Sep 17 00:00:00 2001 From: klicker Date: Wed, 15 Nov 2023 09:19:58 +0100 Subject: [PATCH 01/40] added timeline to conversion --- README.md | 1 + 1 file changed, 1 insertion(+) diff --git a/README.md b/README.md index cf2522c1..d1bf2bd8 100644 --- a/README.md +++ b/README.md @@ -1,3 +1,4 @@ +conversion status: LTSmin [![Build Status](https://travis-ci.org/utwente-fmt/ltsmin.svg?branch=master)](https://travis-ci.org/utwente-fmt/ltsmin) [![FMT](http://fmt.cs.utwente.nl/images/fmt-logo.png)](http://fmt.cs.utwente.nl/) [![UT](https://www.symbitron.eu/wp-content/uploads/2013/10/UT_Logo_2400_Black_EN1-300x58.png)](https://www.utwente.nl/) === From ad3f258d0f67941a40608110d5535e3a0c24059f Mon Sep 17 00:00:00 2001 From: Codermann63 Date: Wed, 15 Nov 2023 10:11:30 +0100 Subject: [PATCH 02/40] added conversion list --- README.md | 57 +++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 57 insertions(+) diff --git a/README.md b/README.md index d1bf2bd8..b4987682 100644 --- a/README.md +++ b/README.md @@ -1,4 +1,61 @@ conversion status: +πŸ’€ = not done +(βœ“) = done but not integrationtestd +βœ“ = done +? = not sure it needs conversion + +πŸ’€ ROOT configure.ac & makefile.am + +Ltsmin/... +? Autotools +? Contrib +πŸ’€ Doc +(βœ“) Examples [OK – laptop/cmake/ltsmin] +(βœ“) Lemon [OK – laptop/cmake/ltsmin] +πŸ₯Ί Lib [AUTOGEN] +βœ“ Ltl2ba [OK – github] +? M4 +πŸ’€ Scoop [Convert the github] +? Spins [Java project] +X Src/.. +---andl-lib +---bignum +---ce +---dm +---etf-convert +---gcf-tool +---hre +---hre-io +---hre-mpi +---ldd2bdd +---lts-io +---lts-lib +---ltsmin-compare +---ltsmin-convert +---ltsmin-lib +---ltsmin-printtrace +---ltsmin-reduce +---ltsmin-reduce-dist +---mc-lib +---pins2lts-dist +---pins2lts-mc +---pins2lts-seq +---pins2lts-sym +---pins-lib +---pins-open +---pinssim +---prob-lib +---scripts +---spg +--spg-lib +---tests +---torx +---util-lib +---vset-lib +πŸ’€ Testsuite +? Travis +? www + LTSmin [![Build Status](https://travis-ci.org/utwente-fmt/ltsmin.svg?branch=master)](https://travis-ci.org/utwente-fmt/ltsmin) [![FMT](http://fmt.cs.utwente.nl/images/fmt-logo.png)](http://fmt.cs.utwente.nl/) [![UT](https://www.symbitron.eu/wp-content/uploads/2013/10/UT_Logo_2400_Black_EN1-300x58.png)](https://www.utwente.nl/) === From e04c2bd444f37ea88956a260b3fd62aa0eef1e4e Mon Sep 17 00:00:00 2001 From: Codermann63 Date: Wed, 15 Nov 2023 10:28:48 +0100 Subject: [PATCH 03/40] updated conversion list --- README.md | 52 ++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 52 insertions(+) diff --git a/README.md b/README.md index b4987682..11628e3e 100644 --- a/README.md +++ b/README.md @@ -1,59 +1,111 @@ conversion status: + πŸ’€ = not done + (βœ“) = done but not integrationtestd + βœ“ = done + ? = not sure it needs conversion πŸ’€ ROOT configure.ac & makefile.am Ltsmin/... + ? Autotools + ? Contrib + πŸ’€ Doc + (βœ“) Examples [OK – laptop/cmake/ltsmin] + (βœ“) Lemon [OK – laptop/cmake/ltsmin] + πŸ₯Ί Lib [AUTOGEN] + βœ“ Ltl2ba [OK – github] + ? M4 + πŸ’€ Scoop [Convert the github] + ? Spins [Java project] + X Src/.. + ---andl-lib + ---bignum + ---ce + ---dm + ---etf-convert + ---gcf-tool + ---hre + ---hre-io + ---hre-mpi + ---ldd2bdd + ---lts-io + ---lts-lib + ---ltsmin-compare + ---ltsmin-convert + ---ltsmin-lib + ---ltsmin-printtrace + ---ltsmin-reduce + ---ltsmin-reduce-dist + ---mc-lib + ---pins2lts-dist + ---pins2lts-mc + ---pins2lts-seq + ---pins2lts-sym + ---pins-lib + ---pins-open + ---pinssim + ---prob-lib + ---scripts + ---spg + --spg-lib + ---tests + ---torx + ---util-lib + ---vset-lib + πŸ’€ Testsuite + ? Travis + ? www LTSmin [![Build Status](https://travis-ci.org/utwente-fmt/ltsmin.svg?branch=master)](https://travis-ci.org/utwente-fmt/ltsmin) [![FMT](http://fmt.cs.utwente.nl/images/fmt-logo.png)](http://fmt.cs.utwente.nl/) [![UT](https://www.symbitron.eu/wp-content/uploads/2013/10/UT_Logo_2400_Black_EN1-300x58.png)](https://www.utwente.nl/) From acd5af2f19d57dd75b9f65ace6945b56c24ec825 Mon Sep 17 00:00:00 2001 From: Codermann63 Date: Wed, 15 Nov 2023 10:32:09 +0100 Subject: [PATCH 04/40] excluded build folders --- .gitignore | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/.gitignore b/.gitignore index 61823c59..a3e15ec8 100644 --- a/.gitignore +++ b/.gitignore @@ -67,3 +67,7 @@ testsuite/wine.exp /examples/*.lps /examples/abp.pbes nbproject + +#Build files +build/* + From 5a5e1342b74c6d6e64e3ee8fdd63140acd39834f Mon Sep 17 00:00:00 2001 From: Codermann63 Date: Wed, 15 Nov 2023 19:15:04 +0100 Subject: [PATCH 05/40] Converted lemon to cmake --- README.md | 4 ++-- lemon/CMakeLists.txt | 6 ++++++ 2 files changed, 8 insertions(+), 2 deletions(-) create mode 100644 lemon/CMakeLists.txt diff --git a/README.md b/README.md index 11628e3e..aaac6902 100644 --- a/README.md +++ b/README.md @@ -18,9 +18,9 @@ Ltsmin/... πŸ’€ Doc -(βœ“) Examples [OK – laptop/cmake/ltsmin] +βœ“ Examples -(βœ“) Lemon [OK – laptop/cmake/ltsmin] +βœ“ Lemon [OK – from mxf] πŸ₯Ί Lib [AUTOGEN] diff --git a/lemon/CMakeLists.txt b/lemon/CMakeLists.txt new file mode 100644 index 00000000..535dd226 --- /dev/null +++ b/lemon/CMakeLists.txt @@ -0,0 +1,6 @@ +cmake_minimum_required(VERSION 2.7) + + +add_executable(lemon lemon.c) + + From b9489a353e59f760de95d7b37bbca194a3fb705b Mon Sep 17 00:00:00 2001 From: Codermann63 Date: Wed, 15 Nov 2023 20:19:48 +0100 Subject: [PATCH 06/40] changed required version of lemon cmake --- README.md | 4 ++-- lemon/CMakeLists.txt | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/README.md b/README.md index aaac6902..7039d74f 100644 --- a/README.md +++ b/README.md @@ -18,13 +18,13 @@ Ltsmin/... πŸ’€ Doc -βœ“ Examples +πŸ’€ Examples βœ“ Lemon [OK – from mxf] πŸ₯Ί Lib [AUTOGEN] -βœ“ Ltl2ba [OK – github] +βœ“ Ltl2ba [OK – ltl2ba github] ? M4 diff --git a/lemon/CMakeLists.txt b/lemon/CMakeLists.txt index 535dd226..bf6ff5ea 100644 --- a/lemon/CMakeLists.txt +++ b/lemon/CMakeLists.txt @@ -1,4 +1,4 @@ -cmake_minimum_required(VERSION 2.7) +cmake_minimum_required(VERSION 3.12) add_executable(lemon lemon.c) From 99821e7ff2dda700218223fafb958efc63d1e01b Mon Sep 17 00:00:00 2001 From: Codermann63 Date: Thu, 16 Nov 2023 16:26:34 +0100 Subject: [PATCH 07/40] updated targetlist --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 7039d74f..6a41ff2d 100644 --- a/README.md +++ b/README.md @@ -20,7 +20,7 @@ Ltsmin/... πŸ’€ Examples -βœ“ Lemon [OK – from mxf] +βœ“ Lemon [OK – from mcf] πŸ₯Ί Lib [AUTOGEN] From 59dc10f30b549f3f18b5f906e2ef0308a5699139 Mon Sep 17 00:00:00 2001 From: Codermann63 Date: Thu, 16 Nov 2023 16:28:59 +0100 Subject: [PATCH 08/40] added cmake files to gitignore --- .gitignore | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/.gitignore b/.gitignore index a3e15ec8..31c22af1 100644 --- a/.gitignore +++ b/.gitignore @@ -71,3 +71,16 @@ 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 + From 673e32c21a2a570cb0498845987e08d4f0caa8e6 Mon Sep 17 00:00:00 2001 From: Codermann63 Date: Sun, 19 Nov 2023 16:14:50 +0100 Subject: [PATCH 09/40] updated conversion status --- README.md | 104 ++++++++++++++++++++++++++++-------------------------- 1 file changed, 53 insertions(+), 51 deletions(-) diff --git a/README.md b/README.md index 6a41ff2d..f78fe2f2 100644 --- a/README.md +++ b/README.md @@ -1,113 +1,115 @@ conversion status: -πŸ’€ = not done +x = not done -(βœ“) = done but not integrationtestd +- = in progress -βœ“ = done +βœ“ = done (or does not need conversion) ? = not sure it needs conversion -πŸ’€ ROOT configure.ac & makefile.am +------------------------------------------------------ -Ltsmin/... +x ROOT configure.ac & makefile.am -? Autotools +? Ltsmin/Autotools -? Contrib +? Ltsmin/Contrib -πŸ’€ Doc +x Ltsmin/Doc -πŸ’€ Examples +x Ltsmin/Examples -βœ“ Lemon [OK – from mcf] +- Ltsmin/Lemon -πŸ₯Ί Lib [AUTOGEN] +? Ltsmin/lib [Looks autogenerated] -βœ“ Ltl2ba [OK – ltl2ba github] +βœ“ Ltsmin/Ltl2ba [OK – from ltl2ba github] -? M4 +? Ltsmin/M4 -πŸ’€ Scoop [Convert the github] +? Ltsmin/Scoop [Github submodule] -? Spins [Java project] +? Spins [Java project] -X Src/.. +x Ltsmin/Src ----andl-lib +x Ltsmin/Src/andl-lib ----bignum +x Ltsmin/Src/bignum ----ce +x Ltsmin/Src/ce ----dm +x Ltsmin/Src/dm ----etf-convert +x Ltsmin/Src/etf-convert ----gcf-tool +x Ltsmin/Src/gcf-tool ----hre +x Ltsmin/Src/hre ----hre-io +x Ltsmin/Src/hre-io ----hre-mpi +x Ltsmin/Src/hre-mpi ----ldd2bdd +x Ltsmin/Src/ldd2bdd ----lts-io +x Ltsmin/Src/lts-io ----lts-lib +x Ltsmin/Src/lts-lib ----ltsmin-compare +x Ltsmin/Src/ltsmin-compare ----ltsmin-convert +x Ltsmin/Src/ltsmin-convert ----ltsmin-lib +x Ltsmin/Src/ltsmin-lib ----ltsmin-printtrace +x Ltsmin/Src/ltsmin-printtrace ----ltsmin-reduce +x Ltsmin/Src/ltsmin-reduce ----ltsmin-reduce-dist +x Ltsmin/Src/ltsmin-reduce-dist ----mc-lib +x Ltsmin/Src/mc-lib ----pins2lts-dist +x Ltsmin/Src/pins2lts-dist ----pins2lts-mc +x Ltsmin/Src/pins2lts-mc ----pins2lts-seq +x Ltsmin/Src/pins2lts-seq ----pins2lts-sym +x Ltsmin/Src/pins2lts-sym ----pins-lib +x Ltsmin/Src/pins-lib ----pins-open +x Ltsmin/Src/pins-open ----pinssim +x Ltsmin/Src/pinssim ----prob-lib +x Ltsmin/Src/prob-lib ----scripts +x Ltsmin/Src/scripts ----spg +x Ltsmin/Src/spg ---spg-lib +x Ltsmin/Src/spg-lib ----tests +x Ltsmin/Src/tests ----torx +x Ltsmin/Src/torx ----util-lib +x Ltsmin/Src/util-lib ----vset-lib +x Ltsmin/Src/vset-lib -πŸ’€ Testsuite +x Testsuite ? Travis ? www +------------------------------------------------------ + LTSmin [![Build Status](https://travis-ci.org/utwente-fmt/ltsmin.svg?branch=master)](https://travis-ci.org/utwente-fmt/ltsmin) [![FMT](http://fmt.cs.utwente.nl/images/fmt-logo.png)](http://fmt.cs.utwente.nl/) [![UT](https://www.symbitron.eu/wp-content/uploads/2013/10/UT_Logo_2400_Black_EN1-300x58.png)](https://www.utwente.nl/) === From 651b39ced9dcfc9a9372c9d3f34fd593f563d871 Mon Sep 17 00:00:00 2001 From: Codermann63 Date: Wed, 22 Nov 2023 13:35:25 +0100 Subject: [PATCH 10/40] Added installation bash script --- install.sh | 70 ++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 70 insertions(+) create mode 100644 install.sh diff --git a/install.sh b/install.sh new file mode 100644 index 00000000..e0d3d50f --- /dev/null +++ b/install.sh @@ -0,0 +1,70 @@ +#!/bin/bash + +# Update +sudo apt update +sudo apt upgrade + +# Required installs 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 + +# +sudo apt install libpopt-dev -y +sudo apt install zlib1g-dev -y +sudo apt install openjdk-11-jre -y +sudo apt install ant -y + + +########################### install sylvan TODO OUTCOMMENT WHEN IT WORKS ############################# +sudo apt install libgmp-dev -y +sudo apt install libhwloc-dev -y +git clone https://github.com/trolando/sylvan.git +cd sylvan +mkdir build +cd build +cmake .. +make +sudo make install +cd ../.. + +# spins? [OK] +# DVE TODO [OK - dve2lts-mc] +# PNML TODO [OK - pnml2lts-sym] +# pins2lts-sym [ok] +# pins2lts-mc [ok] +# sylvan [okish] +# ltl2ba [ok] + +########################## PNML ############################## +sudo apt install xml2 -y +sudo apt install libxml2-dev -y + + + + +################################# LTSMIN ################################# + + +# Get ltsmin from github, configure and intall +git clone https://github.com/utwente-fmt/ltsmin.git +cd ltsmin +git submodule update --init + # Hack to fix error in ltl2ba TODO: fix it in git-submodule + #rm -r ./ltl2ba + #git clone https://github.com/utwente-fmt/ltl2ba.git +./ltsminreconf + + ########################## SPINS INITIALIZE ########################## + cd spins/src + ant + cd ../.. + +./configure --disable-dependency-tracking --with-spins +make +sudo make install \ No newline at end of file From bf5bc76ae25513bb9d1cbf67a8ce832a267deaea Mon Sep 17 00:00:00 2001 From: Codermann63 <96649204+Codermann63@users.noreply.github.com> Date: Tue, 28 Nov 2023 20:34:37 +0100 Subject: [PATCH 11/40] Cleaned up install script --- install.sh | 49 +++++++++++++------------------------------------ 1 file changed, 13 insertions(+), 36 deletions(-) diff --git a/install.sh b/install.sh index e0d3d50f..3c8279d9 100644 --- a/install.sh +++ b/install.sh @@ -1,10 +1,10 @@ #!/bin/bash # Update -sudo apt update -sudo apt upgrade +sudo apt update -y +sudo apt upgrade -y -# Required installs from github: +# Required dependencies when installing from github: sudo apt install git -y sudo apt install make -y sudo apt install automake -y @@ -14,17 +14,17 @@ 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-jre -y +sudo apt install openjdk-11-jdk -y sudo apt install ant -y - -########################### install sylvan TODO OUTCOMMENT WHEN IT WORKS ############################# +########################### 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/trolando/sylvan.git +git clone https://github.com/Codermann63/sylvan.git cd sylvan mkdir build cd build @@ -33,38 +33,15 @@ make sudo make install cd ../.. -# spins? [OK] -# DVE TODO [OK - dve2lts-mc] -# PNML TODO [OK - pnml2lts-sym] -# pins2lts-sym [ok] -# pins2lts-mc [ok] -# sylvan [okish] -# ltl2ba [ok] - -########################## PNML ############################## +########################## PNML dependencies ############################## sudo apt install xml2 -y sudo apt install libxml2-dev -y - - - -################################# LTSMIN ################################# - - -# Get ltsmin from github, configure and intall +################################# install LTSMIN from github ################################# git clone https://github.com/utwente-fmt/ltsmin.git cd ltsmin git submodule update --init - # Hack to fix error in ltl2ba TODO: fix it in git-submodule - #rm -r ./ltl2ba - #git clone https://github.com/utwente-fmt/ltl2ba.git -./ltsminreconf - - ########################## SPINS INITIALIZE ########################## - cd spins/src - ant - cd ../.. - -./configure --disable-dependency-tracking --with-spins +./ltsminreconf +./configure make -sudo make install \ No newline at end of file +sudo make install From 05e999f8c8d16f66a64d4f5e8e3c0002e95e1383 Mon Sep 17 00:00:00 2001 From: Codermann63 <96649204+Codermann63@users.noreply.github.com> Date: Wed, 29 Nov 2023 13:08:57 +0100 Subject: [PATCH 12/40] added lemon to root CMakeLists --- CMakeLists.txt | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) create mode 100644 CMakeLists.txt diff --git a/CMakeLists.txt b/CMakeLists.txt new file mode 100644 index 00000000..514a663a --- /dev/null +++ b/CMakeLists.txt @@ -0,0 +1,24 @@ +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 +) + +# Add CMake modules path +list(APPEND CMAKE_MODULE_PATH "${CMAKE_CURRENT_LIST_DIR}/cmake/") + +#Dependencies +#TODO get sylvan(?), ltl2ba, scoop, spins via FetchContent + +#TODO add_subdirectory(src) +#TODO LATER add_subdirectory(spins) +#TODO LATER add_subdirectory(scoop) +add_subdirectory(lemon) +#TODO LATER add_subdirectory(ltl2ba) +#TODO add_subdirectory(lib) + + +#TODO add options for examples, tests and documentation From c622dc86c1d97ec4d0de5ade6cc32024d6acc17f Mon Sep 17 00:00:00 2001 From: Codermann63 <96649204+Codermann63@users.noreply.github.com> Date: Mon, 4 Dec 2023 00:12:35 +0100 Subject: [PATCH 13/40] converting src/ce to cmake --- CMakeLists.txt | 6 ++++-- lemon/CMakeLists.txt | 1 - src/CMakeLists.txt | 4 ++++ src/ce/CMakeLists.txt | 23 +++++++++++++++++++++++ 4 files changed, 31 insertions(+), 3 deletions(-) create mode 100644 src/CMakeLists.txt create mode 100644 src/ce/CMakeLists.txt diff --git a/CMakeLists.txt b/CMakeLists.txt index 514a663a..34ce0ef5 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -13,12 +13,14 @@ list(APPEND CMAKE_MODULE_PATH "${CMAKE_CURRENT_LIST_DIR}/cmake/") #Dependencies #TODO get sylvan(?), ltl2ba, scoop, spins via FetchContent -#TODO add_subdirectory(src) +add_subdirectory(src) #TODO LATER add_subdirectory(spins) #TODO LATER add_subdirectory(scoop) add_subdirectory(lemon) #TODO LATER add_subdirectory(ltl2ba) -#TODO add_subdirectory(lib) + + +#TODO add_subdirectory(lib) #TODO not done target_include_directories(ltl2ba PRIVATE ${CMAKE_CURRENT_SOURCE_DIR}/lib) #TODO add options for examples, tests and documentation diff --git a/lemon/CMakeLists.txt b/lemon/CMakeLists.txt index bf6ff5ea..c6650203 100644 --- a/lemon/CMakeLists.txt +++ b/lemon/CMakeLists.txt @@ -3,4 +3,3 @@ cmake_minimum_required(VERSION 3.12) add_executable(lemon lemon.c) - diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt new file mode 100644 index 00000000..1cf3f1a5 --- /dev/null +++ b/src/CMakeLists.txt @@ -0,0 +1,4 @@ +cmake_minimum_required(VERSION 3.21) + +add_subdirectory(ce) + diff --git a/src/ce/CMakeLists.txt b/src/ce/CMakeLists.txt new file mode 100644 index 00000000..eaf6f3e8 --- /dev/null +++ b/src/ce/CMakeLists.txt @@ -0,0 +1,23 @@ +add_library(ce STATIC) + +set(CE_HDRS + bufs.h + Ddlts.h + Dtaudlts.h + groups.h + paint.h + sortcount.h) + +target_sources(ce + PRIVATE + bufs.c + Ddlts.c + ce-mpi.c + Dtaudlts.c + groups.c + paint.c + sortcount.c + ${CE_HDRS} +) + +target_include_directories(ce PRIVATE ${CMAKE_CURRENT_SOURCE_DIR}/src/hre) From 88b1da9c4c69a4480856811aa9a4dc03613a78a6 Mon Sep 17 00:00:00 2001 From: Codermann63 <96649204+Codermann63@users.noreply.github.com> Date: Mon, 4 Dec 2023 09:50:18 +0100 Subject: [PATCH 14/40] push for meeting --- src/CMakeLists.txt | 2 ++ src/hre/CMakeLists.txt | 35 +++++++++++++++++++++++++++++++++++ 2 files changed, 37 insertions(+) create mode 100644 src/hre/CMakeLists.txt diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 1cf3f1a5..023099e5 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -1,4 +1,6 @@ cmake_minimum_required(VERSION 3.21) add_subdirectory(ce) +add_subdirectory(hre) +target_link_libraries(ce hre) diff --git a/src/hre/CMakeLists.txt b/src/hre/CMakeLists.txt new file mode 100644 index 00000000..de583c76 --- /dev/null +++ b/src/hre/CMakeLists.txt @@ -0,0 +1,35 @@ +add_library(hre STATIC) + +set(HRE_HDRS + context.h + dir_ops.h + feedback.h + internal.h + provider.h + queue.h + runtime.h + stringindex.h + table.h + unix.h + user.h) + +target_sources(hre + PRIVATE + hre_context.c + hre_dir_ops.c + hre_feedback.c + hre_main.c + hre_malloc.c + hre_messaging.c + hre_popt.c + hre_pthread.c + hre_queue.c + hre_reduce.c + hre_runtime.c + hre_table.c + hre_timer.c + hre_utils.c + stringindex.c + ${HRE_HDRS} +) + From 8458edd305e3569031060efa7e2408f928d59706 Mon Sep 17 00:00:00 2001 From: Codermann63 <96649204+Codermann63@users.noreply.github.com> Date: Wed, 6 Dec 2023 17:05:39 +0100 Subject: [PATCH 15/40] made an early draft of src/hre and src/ce CMakeLists --- CMakeLists.txt | 12 ++++++++++-- Conversion-to-cmake.txt | 11 +++++++++++ REMOVEWHENDONE.c | 6 ++++++ src/CMakeLists.txt | 2 +- src/ce/CMakeLists.txt | 23 +++++++++++++---------- src/hre/CMakeLists.txt | 28 +++++++++++++++++++++++++--- 6 files changed, 66 insertions(+), 16 deletions(-) create mode 100644 Conversion-to-cmake.txt create mode 100644 REMOVEWHENDONE.c diff --git a/CMakeLists.txt b/CMakeLists.txt index 34ce0ef5..915b270d 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -7,6 +7,9 @@ project(ltsmin LANGUAGES C CXX ) +Set(CMAKE_CXX_STANDARD 11) +Set(CMAKE_CXX_STANDARD_REQUIRED True) + # Add CMake modules path list(APPEND CMAKE_MODULE_PATH "${CMAKE_CURRENT_LIST_DIR}/cmake/") @@ -16,11 +19,16 @@ list(APPEND CMAKE_MODULE_PATH "${CMAKE_CURRENT_LIST_DIR}/cmake/") add_subdirectory(src) #TODO LATER add_subdirectory(spins) #TODO LATER add_subdirectory(scoop) -add_subdirectory(lemon) +#add_subdirectory(lemon) #TODO LATER add_subdirectory(ltl2ba) -#TODO add_subdirectory(lib) #TODO not done target_include_directories(ltl2ba PRIVATE ${CMAKE_CURRENT_SOURCE_DIR}/lib) +add_executable(${PROJECT_NAME} REMOVEWHENDONE.c) + +target_link_libraries(${PROJECT_NAME} PUBLIC ce) +target_link_libraries(${PROJECT_NAME} PUBLIC hre) + + #TODO add options for examples, tests and documentation diff --git a/Conversion-to-cmake.txt b/Conversion-to-cmake.txt new file mode 100644 index 00000000..18b8a64b --- /dev/null +++ b/Conversion-to-cmake.txt @@ -0,0 +1,11 @@ +---------------src/hre---------------- + Note: hre_malloc has compiler error, does not seem to be necessary for autotools to configure the whole project. The error is in the "RTalign" function. You just need to declare ret in the start of the function. + TODO: Check if other sources are necessary for making of project. + TODO: Have a way to generate git_version.h + TODO: 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: check hre_run_time.c. On linux i get "CPU_SETSIZE is undeclared". is fixed by putting #define _GNU_SOURCE on top of the file (line 2). RIGHT NOT IT IS UNCOMMENTED, NOT IN THE hre LIBRARY + +---------------src/ce---------------- + Note: bufs.c: can't find mpi.h + Note: Ddlts.c: can't find mpi.h + Note: I don't know what mpi.h is or where to find/generate it. I cannot find it in the automake build version. A LOT OF FILES DEPEND ON mpi.h in ce diff --git a/REMOVEWHENDONE.c b/REMOVEWHENDONE.c new file mode 100644 index 00000000..34d86c44 --- /dev/null +++ b/REMOVEWHENDONE.c @@ -0,0 +1,6 @@ +#include +int main() { + // printf() displays the string inside quotation + printf("Hello, World!"); + return 0; +} diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 023099e5..efdedd1d 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -1,6 +1,6 @@ cmake_minimum_required(VERSION 3.21) + add_subdirectory(ce) add_subdirectory(hre) -target_link_libraries(ce hre) diff --git a/src/ce/CMakeLists.txt b/src/ce/CMakeLists.txt index eaf6f3e8..236d4a22 100644 --- a/src/ce/CMakeLists.txt +++ b/src/ce/CMakeLists.txt @@ -2,22 +2,25 @@ add_library(ce STATIC) set(CE_HDRS bufs.h - Ddlts.h - Dtaudlts.h - groups.h + #Ddlts.h #can't find mpi.h + #Dtaudlts.h #can't find mpi.h + #groups.h #can't find mpi.h (Linked with Dtaudlts) paint.h sortcount.h) target_sources(ce PRIVATE - bufs.c - Ddlts.c - ce-mpi.c - Dtaudlts.c - groups.c - paint.c + #bufs.c #can't find mpi.h + #Ddlts.c #can't find mpi.h + #ce-mpi.c #can't find mpi.h + #Dtaudlts.c #can't find mpi.h + #roups.c #can't find mpi.h (Linked with Dtaudlts) + #paint.c ##can't find mpi.h (Linked with Dtaudlts) sortcount.c ${CE_HDRS} ) -target_include_directories(ce PRIVATE ${CMAKE_CURRENT_SOURCE_DIR}/src/hre) +target_include_directories(ce PUBLIC ${CMAKE_CURRENT_SOURCE_DIR} + "${CMAKE_CURRENT_SOURCE_DIR}/..") + + diff --git a/src/hre/CMakeLists.txt b/src/hre/CMakeLists.txt index de583c76..639d13ac 100644 --- a/src/hre/CMakeLists.txt +++ b/src/hre/CMakeLists.txt @@ -1,3 +1,6 @@ + +cmake_minimum_required(VERSION 3.10) + add_library(hre STATIC) set(HRE_HDRS @@ -11,7 +14,19 @@ set(HRE_HDRS stringindex.h table.h unix.h - user.h) + user.h + git_version.h #WHERE DOES THIS COME FROM? generated from configure.ac: Comes from some git_version.h.tmp. Is generated with SEE BELOW: +#if HAVE_VERSION_CONTROL +#GIT_DESCRIBE := $(shell cd $(top_srcdir) && git describe --tags --abbrev=6 --dirty 2>/dev/null) +# +#git_version.h: git_version.h.tmp +# @if cmp $< $@ 2>/dev/null; then $(RM) $<; else mv $< $@; fi +# +#git_version.h.tmp: +# @echo "#define GIT_VERSION \"$(GIT_DESCRIBE)\"" > $@ +#.PHONY: git_version.h.tmp +#endif + ) target_sources(hre PRIVATE @@ -19,13 +34,13 @@ target_sources(hre hre_dir_ops.c hre_feedback.c hre_main.c - hre_malloc.c + #hre_malloc.c #Might not be necessary, automake makes without this file ALSO COMPILEERROR hre_messaging.c hre_popt.c hre_pthread.c hre_queue.c hre_reduce.c - hre_runtime.c + #hre_runtime.c #See root/Conversion-to-cmake.txt for more info. (under src/hre) hre_table.c hre_timer.c hre_utils.c @@ -33,3 +48,10 @@ target_sources(hre ${HRE_HDRS} ) +configure_file(${PROJECT_SOURCE_DIR}/src/hre/config.h.in ${PROJECT_SOURCE_DIR}/src/hre/config.h) + + +# Include directories +target_include_directories(hre PUBLIC ${CMAKE_CURRENT_SOURCE_DIR} + "${CMAKE_CURRENT_SOURCE_DIR}/..") + From fd6dd26e3ba5175dd5e2e6907e70f05162f8b836 Mon Sep 17 00:00:00 2001 From: Codermann63 <96649204+Codermann63@users.noreply.github.com> Date: Fri, 8 Dec 2023 14:45:43 +0100 Subject: [PATCH 16/40] Flex and lemon conversion implemented --- CMakeLists.txt | 6 +-- Conversion-to-cmake.txt | 13 ++++++ lemon/CMakeLists.txt | 3 ++ src/CMakeLists.txt | 3 +- src/ltsmin-lib/CMakeLists.txt | 76 +++++++++++++++++++++++++++++++++++ src/pins-lib/CMakeLists.txt | 43 ++++++++++++++++++++ 6 files changed, 140 insertions(+), 4 deletions(-) create mode 100644 src/ltsmin-lib/CMakeLists.txt create mode 100644 src/pins-lib/CMakeLists.txt diff --git a/CMakeLists.txt b/CMakeLists.txt index 915b270d..8e806021 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -19,7 +19,7 @@ list(APPEND CMAKE_MODULE_PATH "${CMAKE_CURRENT_LIST_DIR}/cmake/") add_subdirectory(src) #TODO LATER add_subdirectory(spins) #TODO LATER add_subdirectory(scoop) -#add_subdirectory(lemon) +add_subdirectory(lemon) #TODO LATER add_subdirectory(ltl2ba) @@ -27,8 +27,8 @@ add_executable(${PROJECT_NAME} REMOVEWHENDONE.c) target_link_libraries(${PROJECT_NAME} PUBLIC ce) target_link_libraries(${PROJECT_NAME} PUBLIC hre) - - +target_link_libraries(${PROJECT_NAME} PUBLIC ltsmin-lib) +target_link_libraries(${PROJECT_NAME} PUBLIC pins-lib) #TODO add options for examples, tests and documentation diff --git a/Conversion-to-cmake.txt b/Conversion-to-cmake.txt index 18b8a64b..ba775eaa 100644 --- a/Conversion-to-cmake.txt +++ b/Conversion-to-cmake.txt @@ -9,3 +9,16 @@ Note: bufs.c: can't find mpi.h Note: Ddlts.c: can't find mpi.h Note: I don't know what mpi.h is or where to find/generate it. I cannot find it in the automake build version. A LOT OF FILES DEPEND ON mpi.h in ce + +---------------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 + + + +CURRENTLY WORKING src/pins-lib -> src/ltsmin-libs diff --git a/lemon/CMakeLists.txt b/lemon/CMakeLists.txt index c6650203..19f21da2 100644 --- a/lemon/CMakeLists.txt +++ b/lemon/CMakeLists.txt @@ -3,3 +3,6 @@ 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}) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index efdedd1d..3e7dd2f7 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -3,4 +3,5 @@ cmake_minimum_required(VERSION 3.21) add_subdirectory(ce) add_subdirectory(hre) - +add_subdirectory(pins-lib) +add_subdirectory(ltsmin-lib) diff --git a/src/ltsmin-lib/CMakeLists.txt b/src/ltsmin-lib/CMakeLists.txt new file mode 100644 index 00000000..1efd798d --- /dev/null +++ b/src/ltsmin-lib/CMakeLists.txt @@ -0,0 +1,76 @@ + + +#OLD AUTOMAKE CODE for generating with lemon: +#%.c %.h: %.lemon lempar.c +# $(MAKE) $(MAKE_AMFLAGS) -C $(top_builddir)/lemon +# $(top_builddir)/lemon/lemon$(BUILD_EXEEXT) $(LEMON_FLAGS) $< +# @if test -f $@; then touch $@; fi +# + +#Generate files with lemon +add_custom_command( + OUTPUT ltsmin-grammar.h ltsmin-grammar.c ltsmin-grammar.out + COMMAND ${CMAKE_BINARY_DIR}/lemon/lemon${BUILD_EXEEXT} ${LEMON_FLAGS} ${CMAKE_CURRENT_SOURCE_DIR}/ltsmin-grammar.lemon + COMMENT "Generating ltsmin-grammer files" + DEPENDS lemon +) + +#Generate files with flex + #OLD AUTOMAKE CODE FOR generating with lex: + #%.c %.h: %.l + # $(am__skiplex) $(LEX) $< +#TODO it looks like it is optional in the old automake code. Look into this +FIND_PACKAGE(FLEX REQUIRED) +FLEX_TARGET(LTSMINLEXER ltsmin-lexer.l ${CMAKE_CURRENT_BINARY_DIR}/ltsmin-lexer.c + DEFINES_FILE ${CMAKE_CURRENT_BINARY_DIR}/ltsmin-lexer.h) + + + +add_library(ltsmin-lib STATIC ) +set(LTSMINLIB_HDRS + etf-internal.h + etf-objects.h + etf-util.h + ltl2ba-lex.h + ltl2ba-lex-helper.h + ltl2spot.h + ltsmin-buchi.h + ltsmin-grammar.h + ltsmin-parse-env.h + ltsmin-standard.h + ltsmin-syntax.h + ltsmin-tl.h + ltsmin-type-system.h + lts-type.h + mucalc-parse-env.h + mucalc-syntax.h + +) + +target_sources(ltsmin-lib + PRIVATE + etf-objects.c + etf-parser.c + etf-util.c + ltl2ba-lex.c + ltl2ba-lex-helper.c + ltsmin-syntax.c + ltsmin-tl.c + ltsmin-type-system.c + lts-type.c + mucalc-syntax.c + ltl2spot.cpp + ${LTSMINLIB_HDRS} + ${FLEX_LTSMINLEXER_OUTPUTS} +) + +target_link_libraries(ltsmin-lib ${FLEX_LIBRARIES}) + + + + +target_include_directories(ltsmin-lib PUBLIC ${CMAKE_CURRENT_SOURCE_DIR} + ${CMAKE_CURRENT_BINARY_DIR}/.. + ${CMAKE_CURRENT_SOURCE_DIR}/..) + + diff --git a/src/pins-lib/CMakeLists.txt b/src/pins-lib/CMakeLists.txt new file mode 100644 index 00000000..421a3f9b --- /dev/null +++ b/src/pins-lib/CMakeLists.txt @@ -0,0 +1,43 @@ + +cmake_minimum_required(VERSION 3.21) + +add_library(pins-lib STATIC) + +set(PINSLIB_HDRS + dlopen-api.h + pg-types.h + pins.h + pins2pins-cache.h + pins2pins-check.h + pins2pins-fork.h + pins2pins-group.h + pins2pins-guards.h + pins2pins-ltl.h + pins2pins-mucalc.h + pins-impl.h + pins-util.h + property-semantics.h + ) + + +target_sources(pins-lib + PRIVATE + pins.c + pins2pins-cache.c + pins2pins-check.c + pins2pins-fork.c + pins2pins-group.c + pins2pins-guards.c + pins2pins-ltl.c + pins2pins-mucalc.c + pins-util.c + property-semantics.c + ${PINSLIB_HDRS} +) + +target_include_directories(pins-lib PUBLIC ${CMAKE_CURRENT_SOURCE_DIR} + "${CMAKE_CURRENT_SOURCE_DIR}/..") + +#add_subdirectory(modules) +#add_subdirectory(por) + From 3eb9e92b55015fe8a12d5104f4d3af2720fbd432 Mon Sep 17 00:00:00 2001 From: Codermann63 <96649204+Codermann63@users.noreply.github.com> Date: Fri, 8 Dec 2023 16:18:06 +0100 Subject: [PATCH 17/40] Cmake conversion to work with ltl2ba --- CMakeLists.txt | 29 +++++++++++++++++++++++++++-- Conversion-to-cmake.txt | 8 ++++++++ REMOVEWHENDONE.c | 7 +------ src/hre/CMakeLists.txt | 3 ++- 4 files changed, 38 insertions(+), 9 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 8e806021..5bc1e2c4 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -13,14 +13,37 @@ Set(CMAKE_CXX_STANDARD_REQUIRED True) # Add CMake modules path list(APPEND CMAKE_MODULE_PATH "${CMAKE_CURRENT_LIST_DIR}/cmake/") +# 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() + + #Dependencies -#TODO get sylvan(?), ltl2ba, scoop, spins via FetchContent +#TODO get sylvan(?) via FetchContent? or make it a submodule add_subdirectory(src) #TODO LATER add_subdirectory(spins) #TODO LATER add_subdirectory(scoop) add_subdirectory(lemon) -#TODO LATER add_subdirectory(ltl2ba) +add_subdirectory(ltl2ba) add_executable(${PROJECT_NAME} REMOVEWHENDONE.c) @@ -29,6 +52,8 @@ target_link_libraries(${PROJECT_NAME} PUBLIC ce) target_link_libraries(${PROJECT_NAME} PUBLIC hre) target_link_libraries(${PROJECT_NAME} PUBLIC ltsmin-lib) target_link_libraries(${PROJECT_NAME} PUBLIC pins-lib) +target_link_libraries(${PROJECT_NAME} PUBLIC ltl2ba) + #TODO add options for examples, tests and documentation diff --git a/Conversion-to-cmake.txt b/Conversion-to-cmake.txt index ba775eaa..3fa19300 100644 --- a/Conversion-to-cmake.txt +++ b/Conversion-to-cmake.txt @@ -1,3 +1,6 @@ +GENERAL NOTES: +remove config.h.in from gitignore?? + ---------------src/hre---------------- Note: hre_malloc has compiler error, does not seem to be necessary for autotools to configure the whole project. The error is in the "RTalign" function. You just need to declare ret in the start of the function. TODO: Check if other sources are necessary for making of project. @@ -19,6 +22,11 @@ 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-------------------- +When making with cmake it needs a config.h that was created by autotools (i suggest to create it with configue_file(config.h.in config.h) and manually create a config.h.in) + also remove config.h.in from gitignore +TODO: in gitmodules change from url = https://github.com/codermann63/ltl2ba.git to url = https://github.com/utwente-fmt/ltl2ba.git +------------------------------------------------- CURRENTLY WORKING src/pins-lib -> src/ltsmin-libs diff --git a/REMOVEWHENDONE.c b/REMOVEWHENDONE.c index 34d86c44..40cb9bc6 100644 --- a/REMOVEWHENDONE.c +++ b/REMOVEWHENDONE.c @@ -1,6 +1 @@ -#include -int main() { - // printf() displays the string inside quotation - printf("Hello, World!"); - return 0; -} +//This files is created for developments of the cmake version diff --git a/src/hre/CMakeLists.txt b/src/hre/CMakeLists.txt index 639d13ac..be73a16f 100644 --- a/src/hre/CMakeLists.txt +++ b/src/hre/CMakeLists.txt @@ -53,5 +53,6 @@ configure_file(${PROJECT_SOURCE_DIR}/src/hre/config.h.in ${PROJECT_SOURCE_DIR}/s # Include directories target_include_directories(hre PUBLIC ${CMAKE_CURRENT_SOURCE_DIR} - "${CMAKE_CURRENT_SOURCE_DIR}/..") + "${CMAKE_CURRENT_SOURCE_DIR}/.." + ${CMAKE_CURRENT_BINARY_DIR}/..) From 52977fffca14074ef800a1db70704978761ca75a Mon Sep 17 00:00:00 2001 From: Codermann63 <96649204+Codermann63@users.noreply.github.com> Date: Mon, 18 Dec 2023 09:44:33 +0100 Subject: [PATCH 18/40] Converting ltsmin-lib to cmake --- CMakeLists.txt | 14 ++++++++----- Conversion-to-cmake.txt | 8 +++++++- src/hre/CMakeLists.txt | 2 +- src/ltsmin-lib/CMakeLists.txt | 37 +++++++++++++++++++++++------------ src/pins-lib/CMakeLists.txt | 5 ++++- 5 files changed, 46 insertions(+), 20 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 5bc1e2c4..a3e187df 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -48,11 +48,15 @@ add_subdirectory(ltl2ba) add_executable(${PROJECT_NAME} REMOVEWHENDONE.c) -target_link_libraries(${PROJECT_NAME} PUBLIC ce) -target_link_libraries(${PROJECT_NAME} PUBLIC hre) -target_link_libraries(${PROJECT_NAME} PUBLIC ltsmin-lib) -target_link_libraries(${PROJECT_NAME} PUBLIC pins-lib) -target_link_libraries(${PROJECT_NAME} PUBLIC ltl2ba) +target_include_directories(ltsmin PUBLIC ${CMAKE_SOURCE_DIR}/src + ${CMAKE_SOURCE_DIR}/ltl2ba) + +target_link_libraries(${PROJECT_NAME} PRIVATE ce) +target_link_libraries(${PROJECT_NAME} PRIVATE hre) +target_link_libraries(${PROJECT_NAME} PRIVATE ltsmin-lib) +target_link_libraries(${PROJECT_NAME} PRIVATE pins-lib) +target_link_libraries(${PROJECT_NAME} PRIVATE ltl2ba) + diff --git a/Conversion-to-cmake.txt b/Conversion-to-cmake.txt index 3fa19300..6bbfcf72 100644 --- a/Conversion-to-cmake.txt +++ b/Conversion-to-cmake.txt @@ -1,6 +1,10 @@ GENERAL NOTES: remove config.h.in from gitignore?? +----------------root----------------- +Unsure what ltsmin should be build as? a library needs sources, and an excecutable creates an executable (which automake does not do) + + ---------------src/hre---------------- Note: hre_malloc has compiler error, does not seem to be necessary for autotools to configure the whole project. The error is in the "RTalign" function. You just need to declare ret in the start of the function. TODO: Check if other sources are necessary for making of project. @@ -16,6 +20,7 @@ remove config.h.in from gitignore?? ---------------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. + TODO: uncomment ltl2spot.cpp and make it depend if spot is enabled or disabled ---------------lemon--------------------- @@ -29,4 +34,5 @@ TODO: in gitmodules change from url = https://github.com/codermann63/ltl2ba.git ------------------------------------------------- -CURRENTLY WORKING src/pins-lib -> src/ltsmin-libs +CURRENTLY WORKING src/pins-lib: + in src/ltsmin-lib make_custom_coman -> make_custom_target and make ltsmin-lib depend on it diff --git a/src/hre/CMakeLists.txt b/src/hre/CMakeLists.txt index be73a16f..bc00032d 100644 --- a/src/hre/CMakeLists.txt +++ b/src/hre/CMakeLists.txt @@ -34,7 +34,7 @@ target_sources(hre hre_dir_ops.c hre_feedback.c hre_main.c - #hre_malloc.c #Might not be necessary, automake makes without this file ALSO COMPILEERROR + #hre_malloc.c #Might not be necessary, automake makes without this file: ALSO COMPILEERROR hre_messaging.c hre_popt.c hre_pthread.c diff --git a/src/ltsmin-lib/CMakeLists.txt b/src/ltsmin-lib/CMakeLists.txt index 1efd798d..18b36c4a 100644 --- a/src/ltsmin-lib/CMakeLists.txt +++ b/src/ltsmin-lib/CMakeLists.txt @@ -8,21 +8,29 @@ # #Generate files with lemon -add_custom_command( - OUTPUT ltsmin-grammar.h ltsmin-grammar.c ltsmin-grammar.out - COMMAND ${CMAKE_BINARY_DIR}/lemon/lemon${BUILD_EXEEXT} ${LEMON_FLAGS} ${CMAKE_CURRENT_SOURCE_DIR}/ltsmin-grammar.lemon - COMMENT "Generating ltsmin-grammer files" - DEPENDS lemon -) +set(LEMONFILES ltsmin-grammar mucalc-grammar) +foreach(LEMONFILE ${LEMONFILES}) + add_custom_command( + OUTPUT ${LEMONFILE}.h ${LEMONFILE}.c + COMMAND ${CMAKE_BINARY_DIR}/lemon/lemon${BUILD_EXEEXT} ${LEMON_FLAGS} ${CMAKE_CURRENT_SOURCE_DIR}/${LEMONFILE}.lemon + COMMENT "Generating ltsmin-grammer files" + #WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR} + DEPENDS lemon + ) +endforeach() #Generate files with flex #OLD AUTOMAKE CODE FOR generating with lex: #%.c %.h: %.l # $(am__skiplex) $(LEX) $< #TODO it looks like it is optional in the old automake code. Look into this + +set(FLEXFILES ltsmin-lexer mucalc-lexer) FIND_PACKAGE(FLEX REQUIRED) -FLEX_TARGET(LTSMINLEXER ltsmin-lexer.l ${CMAKE_CURRENT_BINARY_DIR}/ltsmin-lexer.c - DEFINES_FILE ${CMAKE_CURRENT_BINARY_DIR}/ltsmin-lexer.h) +foreach(FLEXFILE ${FLEXFILES}) + FLEX_TARGET(LTSMINLEXER ${FLEXFILE}.l ${CMAKE_CURRENT_BINARY_DIR}/${FLEXFILE}.c + DEFINES_FILE ${CMAKE_CURRENT_BINARY_DIR}/${FLEXFILE}.h) +endforeach() @@ -35,13 +43,14 @@ set(LTSMINLIB_HDRS ltl2ba-lex-helper.h ltl2spot.h ltsmin-buchi.h - ltsmin-grammar.h ltsmin-parse-env.h + ltsmin-grammar.h ltsmin-standard.h ltsmin-syntax.h ltsmin-tl.h ltsmin-type-system.h lts-type.h + mucalc-grammar.h mucalc-parse-env.h mucalc-syntax.h @@ -54,12 +63,14 @@ target_sources(ltsmin-lib etf-util.c ltl2ba-lex.c ltl2ba-lex-helper.c + ltsmin-grammar.c ltsmin-syntax.c ltsmin-tl.c ltsmin-type-system.c lts-type.c + mucalc-grammar.c mucalc-syntax.c - ltl2spot.cpp + #ltl2spot.cpp ${LTSMINLIB_HDRS} ${FLEX_LTSMINLEXER_OUTPUTS} ) @@ -70,7 +81,9 @@ target_link_libraries(ltsmin-lib ${FLEX_LIBRARIES}) target_include_directories(ltsmin-lib PUBLIC ${CMAKE_CURRENT_SOURCE_DIR} - ${CMAKE_CURRENT_BINARY_DIR}/.. - ${CMAKE_CURRENT_SOURCE_DIR}/..) + ${CMAKE_CURRENT_BINARY_DIR}/.. + ${CMAKE_SOURCE_DIR}/ltl2ba + ${CMAKE_SOURCE_DIR}/src) + diff --git a/src/pins-lib/CMakeLists.txt b/src/pins-lib/CMakeLists.txt index 421a3f9b..25eef314 100644 --- a/src/pins-lib/CMakeLists.txt +++ b/src/pins-lib/CMakeLists.txt @@ -36,7 +36,10 @@ target_sources(pins-lib ) target_include_directories(pins-lib PUBLIC ${CMAKE_CURRENT_SOURCE_DIR} - "${CMAKE_CURRENT_SOURCE_DIR}/..") + "${CMAKE_CURRENT_SOURCE_DIR}/.." + ${CMAKE_CURRENT_BINARY_DIR}/..) + +add_dependencies(pins-lib ltsmin-lib) #add_subdirectory(modules) #add_subdirectory(por) From 4b6c1c82543d56487e499a0b46cc87c5232daf23 Mon Sep 17 00:00:00 2001 From: Codermann63 <96649204+Codermann63@users.noreply.github.com> Date: Mon, 18 Dec 2023 12:04:53 +0100 Subject: [PATCH 19/40] Made ce optional --- Conversion-to-cmake.txt | 25 +++++++++++++++---------- src/CMakeLists.txt | 32 ++++++++++++++++++++++++++++++-- 2 files changed, 45 insertions(+), 12 deletions(-) diff --git a/Conversion-to-cmake.txt b/Conversion-to-cmake.txt index 6bbfcf72..95d223ea 100644 --- a/Conversion-to-cmake.txt +++ b/Conversion-to-cmake.txt @@ -6,16 +6,16 @@ Unsure what ltsmin should be build as? a library needs sources, and an excecutab ---------------src/hre---------------- - Note: hre_malloc has compiler error, does not seem to be necessary for autotools to configure the whole project. The error is in the "RTalign" function. You just need to declare ret in the start of the function. - TODO: Check if other sources are necessary for making of project. - TODO: Have a way to generate git_version.h - TODO: 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: check hre_run_time.c. On linux i get "CPU_SETSIZE is undeclared". is fixed by putting #define _GNU_SOURCE on top of the file (line 2). RIGHT NOT IT IS UNCOMMENTED, NOT IN THE hre LIBRARY + Note: FILE:hre_malloc has compiler error, does not seem to be necessary for autotools to configure the whole project. The error is in the "RTalign" function. You just need to declare ret in the start of the function. + TODO: Check if other sources can be left out for making of project. + TODO: FILE:git_version.h is generated. Figure our how + 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:hre_run_time.c. (compile-error)On linux i get "CPU_SETSIZE is undeclared". is fixed by putting #define _GNU_SOURCE on top of the file (line 2). RIGHT NOW hre_run_time.c IS NOT INCLUDED IN CMAKEMAKELISTS. ----------------src/ce---------------- +---------------src/ce---------------- OPTIONAL Note: bufs.c: can't find mpi.h Note: Ddlts.c: can't find mpi.h - Note: I don't know what mpi.h is or where to find/generate it. I cannot find it in the automake build version. A LOT OF FILES DEPEND ON mpi.h in ce + Note: I don't know what mpi.h is or where to find/generate it. I cannot find it in the automake build version. A LOT OF FILES DEPEND ON mpi.h in ce: https://stackoverflow.com/questions/26920083/fatal-error-mpi-h-no-such-file-or-directory-include-mpi-h ---------------src/ltmin-libs---------------- .lemon and .l files are used for generation of .c and .h files with lemon and flex @@ -30,9 +30,14 @@ Unsure what ltsmin should be build as? a library needs sources, and an excecutab ---------------ltl2ba-------------------- When making with cmake it needs a config.h that was created by autotools (i suggest to create it with configue_file(config.h.in config.h) and manually create a config.h.in) also remove config.h.in from gitignore -TODO: in gitmodules change from url = https://github.com/codermann63/ltl2ba.git to url = https://github.com/utwente-fmt/ltl2ba.git - +TODO: GITERROR:"ltl2ba cannot be made with cmake" in gitmodules change from "url = https://github.com/codermann63/ltl2ba.git" to u"rl = https://github.com/utwente-fmt/ltl2ba.git" + + +---------------src/pins-lib: -------------------- + Note: is dependend on generated files from ltsmin-lib ------------------------------------------------- -CURRENTLY WORKING src/pins-lib: + + +CURRENTLY WORKING in src/ltsmin-lib make_custom_coman -> make_custom_target and make ltsmin-lib depend on it diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 3e7dd2f7..a7f30b8b 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -1,7 +1,35 @@ -cmake_minimum_required(VERSION 3.21) +# 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 +# +# +cmake_minimum_required(VERSION 3.21) -add_subdirectory(ce) +Option(HAVE_CE OFF) +if (HAVE_CE) + add_subdirectory(ce) +endif() add_subdirectory(hre) add_subdirectory(pins-lib) add_subdirectory(ltsmin-lib) From 08431679e31032b4332eb5f1303bf8f5b70fb1ff Mon Sep 17 00:00:00 2001 From: Codermann63 <96649204+Codermann63@users.noreply.github.com> Date: Tue, 2 Jan 2024 12:55:42 +0100 Subject: [PATCH 20/40] Begin conversion to cmake of lts-sym --- .gitignore | 2 +- CMakeLists.txt | 1 + Conversion-to-cmake.txt | 2 +- config.h.in | 0 src/CMakeLists.txt | 1 + src/hre/config.h.in | 19 +++++++++++++++++++ src/pins2lts-sym/CMakeLists.txt | 3 +++ 7 files changed, 26 insertions(+), 2 deletions(-) create mode 100644 config.h.in create mode 100644 src/hre/config.h.in create mode 100644 src/pins2lts-sym/CMakeLists.txt diff --git a/.gitignore b/.gitignore index 31c22af1..78cc0afe 100644 --- a/.gitignore +++ b/.gitignore @@ -13,7 +13,7 @@ TAGS *.sum *.plist *.dSYM -config.h.in +# config.h.in Removed for cmake compilation .libs/ .metadata/ .project diff --git a/CMakeLists.txt b/CMakeLists.txt index a3e187df..6476812b 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -45,6 +45,7 @@ add_subdirectory(src) add_subdirectory(lemon) add_subdirectory(ltl2ba) +configure_file(${PROJECT_SOURCE_DIR}/config.h.in ${PROJECT_SOURCE_DIR}/ltl2ba/config.h) add_executable(${PROJECT_NAME} REMOVEWHENDONE.c) diff --git a/Conversion-to-cmake.txt b/Conversion-to-cmake.txt index 95d223ea..9e2331d5 100644 --- a/Conversion-to-cmake.txt +++ b/Conversion-to-cmake.txt @@ -1,5 +1,5 @@ GENERAL NOTES: -remove config.h.in from gitignore?? +- Check if flex installation in install script is good enough. Maybe a make error? If no error when running make, delete this note. ----------------root----------------- Unsure what ltsmin should be build as? a library needs sources, and an excecutable creates an executable (which automake does not do) diff --git a/config.h.in b/config.h.in new file mode 100644 index 00000000..e69de29b diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index a7f30b8b..73cfabb2 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -33,3 +33,4 @@ endif() add_subdirectory(hre) add_subdirectory(pins-lib) add_subdirectory(ltsmin-lib) +add_subdirectory(pins2lts-sym) diff --git a/src/hre/config.h.in b/src/hre/config.h.in new file mode 100644 index 00000000..734c170a --- /dev/null +++ b/src/hre/config.h.in @@ -0,0 +1,19 @@ + +/* Define maximal length of pathnames */ +#define LTSMIN_PATHNAME_MAX 1024 + +/* Define to the address where bug reports for this package should be sent. */ +#define PACKAGE_BUGREPORT "ltsmin-support@lists.utwente.nl" + +/* Define to the full name and version of this package. */ +#define PACKAGE_STRING "ltsmin 3.1.0" + +/* Log2 size of the machine's cache line */ +#define CACHE_LINE 6 + +/* Size of the machine's cache line */ +#define CACHE_LINE_SIZE 64 + +/* Hard coded that we are on linux*/ +/* Other variables are __APPLE__ _WIN32*/ +#define __linux__ 1 diff --git a/src/pins2lts-sym/CMakeLists.txt b/src/pins2lts-sym/CMakeLists.txt new file mode 100644 index 00000000..b28b04f6 --- /dev/null +++ b/src/pins2lts-sym/CMakeLists.txt @@ -0,0 +1,3 @@ + + + From 3fe7324ebf8e1a814fc9bee18d099f44b29f443b Mon Sep 17 00:00:00 2001 From: Codermann63 <96649204+Codermann63@users.noreply.github.com> Date: Fri, 5 Jan 2024 09:03:24 +0100 Subject: [PATCH 21/40] converted vset-lib to cmake --- CMakeLists.txt | 16 ++++----- Conversion-to-cmake.txt | 8 +++-- REMOVEWHENDONE.c | 4 +++ src/CMakeLists.txt | 2 ++ src/pins-lib/CMakeLists.txt | 6 ++-- src/pins2lts-sym/CMakeLists.txt | 40 ++++++++++++++++++++++ src/vset-lib/CMakeLists.txt | 59 +++++++++++++++++++++++++++++++++ 7 files changed, 122 insertions(+), 13 deletions(-) create mode 100644 src/vset-lib/CMakeLists.txt diff --git a/CMakeLists.txt b/CMakeLists.txt index 6476812b..45e9b9f8 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -47,16 +47,16 @@ add_subdirectory(ltl2ba) configure_file(${PROJECT_SOURCE_DIR}/config.h.in ${PROJECT_SOURCE_DIR}/ltl2ba/config.h) -add_executable(${PROJECT_NAME} REMOVEWHENDONE.c) +#add_executable(${PROJECT_NAME} REMOVEWHENDONE.c) -target_include_directories(ltsmin PUBLIC ${CMAKE_SOURCE_DIR}/src - ${CMAKE_SOURCE_DIR}/ltl2ba) +#target_include_directories(ltsmin PUBLIC ${CMAKE_SOURCE_DIR}/src +# ${CMAKE_SOURCE_DIR}/ltl2ba) -target_link_libraries(${PROJECT_NAME} PRIVATE ce) -target_link_libraries(${PROJECT_NAME} PRIVATE hre) -target_link_libraries(${PROJECT_NAME} PRIVATE ltsmin-lib) -target_link_libraries(${PROJECT_NAME} PRIVATE pins-lib) -target_link_libraries(${PROJECT_NAME} PRIVATE ltl2ba) +#target_link_libraries(${PROJECT_NAME} PRIVATE ce) +#target_link_libraries(${PROJECT_NAME} PRIVATE hre) +#target_link_libraries(${PROJECT_NAME} PRIVATE ltsmin-lib) +#target_link_libraries(${PROJECT_NAME} PRIVATE pins-lib) +#target_link_libraries(${PROJECT_NAME} PRIVATE ltl2ba) diff --git a/Conversion-to-cmake.txt b/Conversion-to-cmake.txt index 9e2331d5..816a4f5e 100644 --- a/Conversion-to-cmake.txt +++ b/Conversion-to-cmake.txt @@ -36,8 +36,10 @@ TODO: GITERROR:"ltl2ba cannot be made with cmake" in gitmodules change from "url ---------------src/pins-lib: -------------------- Note: is dependend on generated files from ltsmin-lib -------------------------------------------------- +---------------src/pins2lts-sym--------------------- + Note: Automake generates .la and .lo files it uses to link libraries. It is recommended to use pkgconf to link libraries instead. + +---------------src/vset-lib--------------------- + Note: a lot of optional content. I've tried to copy the options from the automake script -CURRENTLY WORKING - in src/ltsmin-lib make_custom_coman -> make_custom_target and make ltsmin-lib depend on it diff --git a/REMOVEWHENDONE.c b/REMOVEWHENDONE.c index 40cb9bc6..6f07c386 100644 --- a/REMOVEWHENDONE.c +++ b/REMOVEWHENDONE.c @@ -1 +1,5 @@ //This files is created for developments of the cmake version + +int main() { + return 0; +} diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 73cfabb2..1ce3b5e5 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -34,3 +34,5 @@ add_subdirectory(hre) add_subdirectory(pins-lib) add_subdirectory(ltsmin-lib) add_subdirectory(pins2lts-sym) +add_subdirectory(vset-lib) +add_subdirectory(util-lib) diff --git a/src/pins-lib/CMakeLists.txt b/src/pins-lib/CMakeLists.txt index 25eef314..b4abfbfa 100644 --- a/src/pins-lib/CMakeLists.txt +++ b/src/pins-lib/CMakeLists.txt @@ -36,10 +36,12 @@ target_sources(pins-lib ) target_include_directories(pins-lib PUBLIC ${CMAKE_CURRENT_SOURCE_DIR} - "${CMAKE_CURRENT_SOURCE_DIR}/.." + ${CMAKE_CURRENT_SOURCE_DIR}/.. ${CMAKE_CURRENT_BINARY_DIR}/..) -add_dependencies(pins-lib ltsmin-lib) +add_dependencies(pins-lib + ltsmin-lib + hre) #add_subdirectory(modules) #add_subdirectory(por) diff --git a/src/pins2lts-sym/CMakeLists.txt b/src/pins2lts-sym/CMakeLists.txt index b28b04f6..66dcd9aa 100644 --- a/src/pins2lts-sym/CMakeLists.txt +++ b/src/pins2lts-sym/CMakeLists.txt @@ -1,3 +1,43 @@ +############REQUIRED################## +#pins2ltsmin-sym +#set(LIBZZZ +# libpins2lts_sym.la +# ../pins-lib/libpins.la +# ../vset-lib/libvset.la +# maxsum/libmaxsum.la +# ../spg-lib/libspg.la +# ../mc-lib/libmc.la +# $(top_builddir)/lib/libgnu.la) + +add_executable( pins2lts-sym pins2lts-sym.c ) +target_link_libraries(pins2lts-sym PRIVATE + pins-lib + ltsmin-lib + hre + vset-lib + util-lib) +#mc-lib? +#lts-io +#dm + +target_include_directories(pins2lts-sym PUBLIC ${CMAKE_CURRENT_SOURCE_DIR} + ${CMAKE_CURRENT_SOURCE_DIR}/.. + ${CMAKE_CURRENT_BINARY_DIR}/..) + + +#################Required NOT included yet###################3 +#eft: eft2lts-sym + + +#################Optional NOT included yet################ +#libstep: lpo2lts-sym +#libmcrl2: lps2lts-sym +#scoop: mapa2lts-sym +#libpbes: pbes2lts-sym +#DVE: dve2lts-sym +#SPINS: prom2lts-sym +#PNML: pnml2lts-sym +#PROB: prob2lts-sym diff --git a/src/vset-lib/CMakeLists.txt b/src/vset-lib/CMakeLists.txt new file mode 100644 index 00000000..15771a7e --- /dev/null +++ b/src/vset-lib/CMakeLists.txt @@ -0,0 +1,59 @@ + +add_library(vset-lib STATIC) +add_dependencies(vset-lib util-lib) + +set(VSET_HDRS + vdom_object.h + vector.h + vector_set.h + ) + +target_sources(vset-lib PRIVATE + vector.c + vector_set.c + vset_listdd.c + vset_listdd64.c + ${VSET_HDRS} +) + +OPTION(HAVE_BUDDY off) +OPTION(HAVE_SYLVAN off) +OPTION(HAVE_LIBMCRL off) +OPTION(HAVE_SDD off) +OPTION(HAVE_LIBDDD off) + +if(HAVE_SDD) + target_sources(vset-lib PRIVATE + vset_buddy.c) +endif() + + +if(HAVE_SDD) + target_sources(vset-lib PRIVATE + vset_sylvan.c + vset_lddmc.c) +endif() + + +if(HAVE_SDD) + target_sources(vset-lib PRIVATE + vset_atermdd.c) +endif() + + +if(HAVE_SDD) + target_sources(vset-lib PRIVATE + sdd_utils.c sdd_utils.h + vset_sdd.c vset_sdd.h + vset_sdd_utils.c vset_sdd_utils.h + vtree_utils.c vtree_utils.h) +endif() + +if(HAVE_LIBDDD) + target_sources(vset-lib PRIVATE + vset_ddd.cpp) +endif() + +target_include_directories(vset-lib PUBLIC ${CMAKE_CURRENT_SOURCE_DIR} + ${CMAKE_CURRENT_SOURCE_DIR}/.. + ${CMAKE_CURRENT_BINARY_DIR}/..) From 45ce8190f81fd8d26e1679663be9f5c663b31c3f Mon Sep 17 00:00:00 2001 From: Codermann63 <96649204+Codermann63@users.noreply.github.com> Date: Fri, 5 Jan 2024 09:27:16 +0100 Subject: [PATCH 22/40] converted util-lib to cmake --- Conversion-to-cmake.txt | 5 ++++ src/pins2lts-sym/CMakeLists.txt | 3 +- src/util-lib/CMakeLists.txt | 52 +++++++++++++++++++++++++++++++++ src/util-lib/fast_set.c | 2 +- src/util-lib/simplemap.h | 2 +- src/vset-lib/vset_listdd64.c | 2 +- 6 files changed, 62 insertions(+), 4 deletions(-) create mode 100644 src/util-lib/CMakeLists.txt diff --git a/Conversion-to-cmake.txt b/Conversion-to-cmake.txt index 816a4f5e..1cee948b 100644 --- a/Conversion-to-cmake.txt +++ b/Conversion-to-cmake.txt @@ -42,4 +42,9 @@ TODO: GITERROR:"ltl2ba cannot be made with cmake" in gitmodules change from "url ---------------src/vset-lib--------------------- Note: a lot of optional content. I've tried to copy the options from the automake script + TODO: vset_listdd64.c could not find config.h. I've changed the include to hre/config.h (because vset_listdd has and include for hre/config.h). CHECK IF CORRECT +---------------src/util-lib--------------------- + QUESTION: fast_set.c has an include to config.h. Automake does not generate one with its make and fast_hash.c has an include to hre/config.h. I've changed the include to hre/config.h. TODO check if correct + ADDITIONAL INFO: fast_set.h has include of hre/config.h + TODO: the same problem with simplemap.h diff --git a/src/pins2lts-sym/CMakeLists.txt b/src/pins2lts-sym/CMakeLists.txt index 66dcd9aa..dd5bd78a 100644 --- a/src/pins2lts-sym/CMakeLists.txt +++ b/src/pins2lts-sym/CMakeLists.txt @@ -17,7 +17,8 @@ target_link_libraries(pins2lts-sym PRIVATE ltsmin-lib hre vset-lib - util-lib) + util-lib + ) #mc-lib? #lts-io #dm diff --git a/src/util-lib/CMakeLists.txt b/src/util-lib/CMakeLists.txt new file mode 100644 index 00000000..13ffc183 --- /dev/null +++ b/src/util-lib/CMakeLists.txt @@ -0,0 +1,52 @@ +add_library(util-lib STATIC) +add_dependencies(util-lib hre) + +target_include_directories(util-lib PUBLIC ${CMAKE_CURRENT_SOURCE_DIR} + ${CMAKE_CURRENT_SOURCE_DIR}/.. + ${CMAKE_CURRENT_BINARY_DIR}/..) + +set(UTILLIB_HDRS + balloc.h + bitmultiset.h + bitset.h + chunk_support.h + chunk_table_factory.h + dfs-stack.h + dynamic-array.h + fast_hash.h + fast_set.h + is-balloc.h + MurmurHash3.h + rationals.h + simplemap.h + string-map.h + tables.h + treedbs.h + util.h + zobrist.h +) + +target_sources(util-lib + PRIVATE + balloc.c + bitmultiset.c + bitset.c + chunk_support.c + chunk_table_factory.c + dfs-stack.c + dynamic-array.c + fast_hash.c + fast_set.c + is-balloc.c + MurmurHash3.c + rationals.c + simplemap.c + string-map.c + tables.c + treedbs.c + util.c + zobrist.c + ${UTILLIB_HDRS} + ) + + diff --git a/src/util-lib/fast_set.c b/src/util-lib/fast_set.c index 13461643..59758034 100644 --- a/src/util-lib/fast_set.c +++ b/src/util-lib/fast_set.c @@ -1,4 +1,4 @@ -#include +#include #include #include diff --git a/src/util-lib/simplemap.h b/src/util-lib/simplemap.h index 4edafd4d..1fa544e8 100644 --- a/src/util-lib/simplemap.h +++ b/src/util-lib/simplemap.h @@ -8,7 +8,7 @@ #ifndef SIMPLEMAP_H_ #define SIMPLEMAP_H_ -#include +#include #include #include diff --git a/src/vset-lib/vset_listdd64.c b/src/vset-lib/vset_listdd64.c index d4493167..5d1c9584 100644 --- a/src/vset-lib/vset_listdd64.c +++ b/src/vset-lib/vset_listdd64.c @@ -1,4 +1,4 @@ -#include +#include #include #include From 6c1018f91a15920a6dd552ccfef8c5eb8fff262e Mon Sep 17 00:00:00 2001 From: Codermann63 <96649204+Codermann63@users.noreply.github.com> Date: Sat, 6 Jan 2024 20:18:23 +0100 Subject: [PATCH 23/40] Implemented an executable for pins2lts-sym --- Conversion-to-cmake.txt | 8 +++- src/CMakeLists.txt | 3 ++ src/dm/CMakeLists.txt | 32 +++++++++++++ src/lts-io/CMakeLists.txt | 29 ++++++++++++ src/ltsmin-lib/CMakeLists.txt | 6 --- src/mc-lib/CMakeLists.txt | 52 +++++++++++++++++++++ src/pins-lib/CMakeLists.txt | 4 +- src/pins2lts-sym/CMakeLists.txt | 65 +++++++++++++++++++++++--- src/pins2lts-sym/maxsum/CMakeLists.txt | 12 +++++ 9 files changed, 194 insertions(+), 17 deletions(-) create mode 100644 src/dm/CMakeLists.txt create mode 100644 src/lts-io/CMakeLists.txt create mode 100644 src/mc-lib/CMakeLists.txt create mode 100644 src/pins2lts-sym/maxsum/CMakeLists.txt diff --git a/Conversion-to-cmake.txt b/Conversion-to-cmake.txt index 1cee948b..c7007385 100644 --- a/Conversion-to-cmake.txt +++ b/Conversion-to-cmake.txt @@ -35,10 +35,11 @@ TODO: GITERROR:"ltl2ba cannot be made with cmake" in gitmodules change from "url ---------------src/pins-lib: -------------------- - Note: is dependend on generated files from ltsmin-lib + Note: is dependend on generated files from ltsmin-libΒ¨ + TODO: convert subdirectory por and add it as subdirectory to CMakeLists.txt ---------------src/pins2lts-sym--------------------- - Note: Automake generates .la and .lo files it uses to link libraries. It is recommended to use pkgconf to link libraries instead. + TODO: check if all compiler flags are given like the automake version ---------------src/vset-lib--------------------- Note: a lot of optional content. I've tried to copy the options from the automake script @@ -47,4 +48,7 @@ TODO: GITERROR:"ltl2ba cannot be made with cmake" in gitmodules change from "url QUESTION: fast_set.c has an include to config.h. Automake does not generate one with its make and fast_hash.c has an include to hre/config.h. I've changed the include to hre/config.h. TODO check if correct ADDITIONAL INFO: fast_set.h has include of hre/config.h TODO: the same problem with simplemap.h +---------------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/--------------------- diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 1ce3b5e5..625f0dd6 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -36,3 +36,6 @@ 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) diff --git a/src/dm/CMakeLists.txt b/src/dm/CMakeLists.txt new file mode 100644 index 00000000..0ab067d9 --- /dev/null +++ b/src/dm/CMakeLists.txt @@ -0,0 +1,32 @@ +add_library(dm STATIC) + +set(DM_HDRS + bitvector.h + dm.h + sloan_ordering.hpp + ) + +target_sources(dm + PRIVATE + bitvector.c + dm.c + ${DM_HDRS} +) + +OPTION(HAVE_BOOST off) +OPTION(HAVE_VIENNACL off) +if (HAVE_BOOST) + target_sources(dm PRIVATE + dm_boost.cpp dm_boost.h) +endif() +if (HAVE_VIENNACL) + target_sources(dm PRIVATE + dm_viennacl.cpp dm_viennacl.h) +endif() + +# Include directories +target_include_directories(dm PUBLIC ${CMAKE_CURRENT_SOURCE_DIR} + ${CMAKE_CURRENT_SOURCE_DIR}/.. + ${CMAKE_CURRENT_BINARY_DIR}/..) + + diff --git a/src/lts-io/CMakeLists.txt b/src/lts-io/CMakeLists.txt new file mode 100644 index 00000000..dc6ad944 --- /dev/null +++ b/src/lts-io/CMakeLists.txt @@ -0,0 +1,29 @@ +add_library(lts-io STATIC) + +set(LTSIO_HDRS + internal.h + provider.h + user.h + ) + +target_sources(lts-io + PRIVATE + aut_io.c + bcg_io.c + file-base.c + filter_write.c + fsm_write.c + lts_file_misc.c + lts-type-io.c + vector_read.c + vector_write.c + ${LTSIO_HDRS} +) + +# Include directories +target_include_directories(lts-io PUBLIC ${CMAKE_CURRENT_SOURCE_DIR} + ${CMAKE_CURRENT_SOURCE_DIR}/.. + ${CMAKE_CURRENT_BINARY_DIR}/..) + + + diff --git a/src/ltsmin-lib/CMakeLists.txt b/src/ltsmin-lib/CMakeLists.txt index 18b36c4a..70643566 100644 --- a/src/ltsmin-lib/CMakeLists.txt +++ b/src/ltsmin-lib/CMakeLists.txt @@ -1,11 +1,5 @@ -#OLD AUTOMAKE CODE for generating with lemon: -#%.c %.h: %.lemon lempar.c -# $(MAKE) $(MAKE_AMFLAGS) -C $(top_builddir)/lemon -# $(top_builddir)/lemon/lemon$(BUILD_EXEEXT) $(LEMON_FLAGS) $< -# @if test -f $@; then touch $@; fi -# #Generate files with lemon set(LEMONFILES ltsmin-grammar mucalc-grammar) diff --git a/src/mc-lib/CMakeLists.txt b/src/mc-lib/CMakeLists.txt new file mode 100644 index 00000000..afda44e8 --- /dev/null +++ b/src/mc-lib/CMakeLists.txt @@ -0,0 +1,52 @@ + +cmake_minimum_required(VERSION 3.21) + +add_library(mc-lib STATIC) + +set(MCLIB_HDRS + atomics.h + bitvector-ll.h + cctables.h + clt_table.h + dbs-ll.h + dlopen_extra.h + hashtable.h + lb.h + lmap.h + renault-unionfind.h + set-ll.h + statistics.h + stats.h + trace.h + treedbs-ll.h + unionfind.h + ) + + +target_sources(mc-lib + PRIVATE + bitvector-ll.c + cctables.c + clt_table.c + dbs-ll.c + dlopen_extra.c + hashtable.c + lb.c + lmap.c + renault-unionfind.c + set-ll.c + statistics.c + trace.c + treedbs-ll.c + unionfind.c + ${MCLIB_HDRS} +) + +target_include_directories(mc-lib PUBLIC ${CMAKE_CURRENT_SOURCE_DIR} + ${CMAKE_CURRENT_SOURCE_DIR}/.. + ${CMAKE_CURRENT_BINARY_DIR}/..) + +#add_dependencies(pins-lib +# ltsmin-lib +# hre) + diff --git a/src/pins-lib/CMakeLists.txt b/src/pins-lib/CMakeLists.txt index b4abfbfa..5b44ad5d 100644 --- a/src/pins-lib/CMakeLists.txt +++ b/src/pins-lib/CMakeLists.txt @@ -43,6 +43,6 @@ add_dependencies(pins-lib ltsmin-lib hre) -#add_subdirectory(modules) -#add_subdirectory(por) + +#TODO: add_subdirectory(por) diff --git a/src/pins2lts-sym/CMakeLists.txt b/src/pins2lts-sym/CMakeLists.txt index dd5bd78a..e08b72a3 100644 --- a/src/pins2lts-sym/CMakeLists.txt +++ b/src/pins2lts-sym/CMakeLists.txt @@ -11,24 +11,75 @@ # ../mc-lib/libmc.la # $(top_builddir)/lib/libgnu.la) -add_executable( pins2lts-sym pins2lts-sym.c ) -target_link_libraries(pins2lts-sym PRIVATE +add_library( libpins2lts-sym pins2lts-sym.c ) + +target_sources(libpins2lts-sym PRIVATE + auxiliary/options.h + alg/bfs.c alg/bfs.h + alg/chain.c alg/chain.h + alg/pg.c alg/pg.h + alg/mu.c alg/mu.h + alg/reach.c alg/reach.h + alg/sat.c alg/sat.h + auxiliary/output.c auxiliary/output.h + auxiliary/prop.c auxiliary/prop.h) +target_link_libraries(libpins2lts-sym PRIVATE pins-lib ltsmin-lib hre vset-lib util-lib + lts-io + dm + maxsum + mc-lib ) #mc-lib? -#lts-io -#dm + -target_include_directories(pins2lts-sym PUBLIC ${CMAKE_CURRENT_SOURCE_DIR} +target_include_directories(libpins2lts-sym PUBLIC ${CMAKE_CURRENT_SOURCE_DIR} ${CMAKE_CURRENT_SOURCE_DIR}/.. - ${CMAKE_CURRENT_BINARY_DIR}/..) - + ${CMAKE_CURRENT_BINARY_DIR}/.. + ${CMAKE_SOURCE_DIR}/src + ${CMAKE_CURRENT_SOURCE_DIR}/auxiliary + ${CMAKE_CURRENT_SOURCE_DIR}/alg) +target_compile_options(libpins2lts-sym + PUBLIC -DPINS_DLL#UNSURE IF THIS SHOULD BE PUBLIC + +) +add_subdirectory(maxsum) +################### EXECUTABLES: pins2lts-sym#################### +#add_executable(pins2lts-sym +# auxiliary/options.c +# ../pins-lib/modules/dlopen-pins.c ../pins-lib/modules/dlopen-pins.h +#) +#target_link_libraries(pins2lts-sym PRIVATE +# libpins2lts-sym +# LTDL-lib +# ) +#target_include_directories(pins2lts-sym PUBLIC ${CMAKE_CURRENT_SOURCE_DIR} +# ${CMAKE_CURRENT_SOURCE_DIR}/.. +# ${CMAKE_CURRENT_BINARY_DIR}/.. +# ${CMAKE_SOURCE_DIR}/src +# ${CMAKE_CURRENT_SOURCE_DIR}/auxiliary +# ${CMAKE_CURRENT_SOURCE_DIR}/alg) +################### EXECUTABLES: eft2lts-sym#################### +add_executable(eft2lts-sym + auxiliary/options.c + ../pins-lib/modules/etf-pins.c ../pins-lib/modules/etf-pins.h +) +target_link_libraries(eft2lts-sym PRIVATE + libpins2lts-sym + ) +target_include_directories(eft2lts-sym PUBLIC ${CMAKE_CURRENT_SOURCE_DIR} + ${CMAKE_CURRENT_SOURCE_DIR}/.. + ${CMAKE_CURRENT_BINARY_DIR}/.. + ${CMAKE_SOURCE_DIR}/src + ${CMAKE_CURRENT_SOURCE_DIR}/auxiliary + ${CMAKE_CURRENT_SOURCE_DIR}/alg) #################Required NOT included yet###################3 + #eft: eft2lts-sym diff --git a/src/pins2lts-sym/maxsum/CMakeLists.txt b/src/pins2lts-sym/maxsum/CMakeLists.txt new file mode 100644 index 00000000..6c00f488 --- /dev/null +++ b/src/pins2lts-sym/maxsum/CMakeLists.txt @@ -0,0 +1,12 @@ +add_library(maxsum STATIC) + +target_sources(maxsum + PRIVATE + maxsum.c + maxsum.h +) + +target_include_directories(maxsum PUBLIC ${CMAKE_CURRENT_SOURCE_DIR} + ${CMAKE_SOURCE_DIR}/src + ${CMAKE_BINARY_DIR}/src) + From a289d0a5166757c50cf67f9b72232dee2d8b4e09 Mon Sep 17 00:00:00 2001 From: Codermann63 <96649204+Codermann63@users.noreply.github.com> Date: Sun, 7 Jan 2024 14:45:55 +0100 Subject: [PATCH 24/40] added spg-lib to cmake --- Conversion-to-cmake.txt | 2 +- src/CMakeLists.txt | 1 + src/hre/CMakeLists.txt | 12 ++++++-- src/hre/config.h.in | 13 +++++++++ src/pins2lts-sym/CMakeLists.txt | 50 ++++++++++++++++----------------- src/spg-lib/CMakeLists.txt | 28 ++++++++++++++++++ 6 files changed, 77 insertions(+), 29 deletions(-) create mode 100644 src/spg-lib/CMakeLists.txt diff --git a/Conversion-to-cmake.txt b/Conversion-to-cmake.txt index c7007385..04f09bec 100644 --- a/Conversion-to-cmake.txt +++ b/Conversion-to-cmake.txt @@ -10,7 +10,7 @@ Unsure what ltsmin should be build as? a library needs sources, and an excecutab TODO: Check if other sources can be left out for making of project. TODO: FILE:git_version.h is generated. Figure our how 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:hre_run_time.c. (compile-error)On linux i get "CPU_SETSIZE is undeclared". is fixed by putting #define _GNU_SOURCE on top of the file (line 2). RIGHT NOW hre_run_time.c IS NOT INCLUDED IN CMAKEMAKELISTS. + TODO: FILE:config.h.in check if _GNU_SOURCE is defined correctly ---------------src/ce---------------- OPTIONAL Note: bufs.c: can't find mpi.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 625f0dd6..23270e79 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -39,3 +39,4 @@ add_subdirectory(util-lib) add_subdirectory(lts-io) add_subdirectory(dm) add_subdirectory(mc-lib) +add_subdirectory(spg-lib) diff --git a/src/hre/CMakeLists.txt b/src/hre/CMakeLists.txt index bc00032d..99257af4 100644 --- a/src/hre/CMakeLists.txt +++ b/src/hre/CMakeLists.txt @@ -34,13 +34,13 @@ target_sources(hre hre_dir_ops.c hre_feedback.c hre_main.c - #hre_malloc.c #Might not be necessary, automake makes without this file: ALSO COMPILEERROR + hre_malloc.c hre_messaging.c hre_popt.c hre_pthread.c hre_queue.c hre_reduce.c - #hre_runtime.c #See root/Conversion-to-cmake.txt for more info. (under src/hre) + hre_runtime.c hre_table.c hre_timer.c hre_utils.c @@ -48,11 +48,17 @@ target_sources(hre ${HRE_HDRS} ) +SET(HAVE_POSIX_MEMALIGN "system has posix memalign" ON) +SET(_GNU_SOURCE "System uses GNU" ON) + configure_file(${PROJECT_SOURCE_DIR}/src/hre/config.h.in ${PROJECT_SOURCE_DIR}/src/hre/config.h) +target_compile_options(hre + PUBLIC -I${CMAKE_SOURCE_DIR}/lib -I${CMAKE_SOURCE_DIR}/lib +) # Include directories target_include_directories(hre PUBLIC ${CMAKE_CURRENT_SOURCE_DIR} - "${CMAKE_CURRENT_SOURCE_DIR}/.." + ${CMAKE_CURRENT_SOURCE_DIR}/.. ${CMAKE_CURRENT_BINARY_DIR}/..) diff --git a/src/hre/config.h.in b/src/hre/config.h.in index 734c170a..61dc2e9b 100644 --- a/src/hre/config.h.in +++ b/src/hre/config.h.in @@ -17,3 +17,16 @@ /* Hard coded that we are on linux*/ /* Other variables are __APPLE__ _WIN32*/ #define __linux__ 1 + +/* Enable GNU extensions on systems that have them. */ +/* FAKE IT CODE */ +/*#cmakedefine _GNU_SOURCE*/ +#ifndef _GNU_SOURCE +# define _GNU_SOURCE 1 +#endif + +/* Define to 1 if you have the `posix_memalign' function. */ +#cmakedefine HAVE_POSIX_MEMALIGN + +/* Define to 1 if you have the `_aligned_malloc' function. */ +#cmakedefine HAVE__ALIGNED_MALLOC diff --git a/src/pins2lts-sym/CMakeLists.txt b/src/pins2lts-sym/CMakeLists.txt index e08b72a3..91a8263b 100644 --- a/src/pins2lts-sym/CMakeLists.txt +++ b/src/pins2lts-sym/CMakeLists.txt @@ -1,3 +1,4 @@ +add_subdirectory(maxsum) ############REQUIRED################## #pins2ltsmin-sym @@ -13,8 +14,8 @@ add_library( libpins2lts-sym pins2lts-sym.c ) -target_sources(libpins2lts-sym PRIVATE - auxiliary/options.h +target_sources(libpins2lts-sym INTERFACE + alg/auxiliary.c alg/auxiliary.h alg/bfs.c alg/bfs.h alg/chain.c alg/chain.h alg/pg.c alg/pg.h @@ -23,7 +24,7 @@ target_sources(libpins2lts-sym PRIVATE alg/sat.c alg/sat.h auxiliary/output.c auxiliary/output.h auxiliary/prop.c auxiliary/prop.h) -target_link_libraries(libpins2lts-sym PRIVATE +target_link_libraries(libpins2lts-sym PUBLIC pins-lib ltsmin-lib hre @@ -32,10 +33,9 @@ target_link_libraries(libpins2lts-sym PRIVATE lts-io dm maxsum - mc-lib + mc-lib + spg-lib ) -#mc-lib? - target_include_directories(libpins2lts-sym PUBLIC ${CMAKE_CURRENT_SOURCE_DIR} ${CMAKE_CURRENT_SOURCE_DIR}/.. @@ -43,26 +43,26 @@ target_include_directories(libpins2lts-sym PUBLIC ${CMAKE_CURRENT_SOURCE_DIR} ${CMAKE_SOURCE_DIR}/src ${CMAKE_CURRENT_SOURCE_DIR}/auxiliary ${CMAKE_CURRENT_SOURCE_DIR}/alg) -target_compile_options(libpins2lts-sym - PUBLIC -DPINS_DLL#UNSURE IF THIS SHOULD BE PUBLIC - -) -add_subdirectory(maxsum) + + ################### EXECUTABLES: pins2lts-sym#################### -#add_executable(pins2lts-sym -# auxiliary/options.c -# ../pins-lib/modules/dlopen-pins.c ../pins-lib/modules/dlopen-pins.h -#) -#target_link_libraries(pins2lts-sym PRIVATE -# libpins2lts-sym -# LTDL-lib -# ) -#target_include_directories(pins2lts-sym PUBLIC ${CMAKE_CURRENT_SOURCE_DIR} -# ${CMAKE_CURRENT_SOURCE_DIR}/.. -# ${CMAKE_CURRENT_BINARY_DIR}/.. -# ${CMAKE_SOURCE_DIR}/src -# ${CMAKE_CURRENT_SOURCE_DIR}/auxiliary -# ${CMAKE_CURRENT_SOURCE_DIR}/alg) +add_executable(pins2lts-sym + auxiliary/options.c auxiliary/options.h + ../pins-lib/modules/dlopen-pins.c ../pins-lib/modules/dlopen-pins.h +) +target_link_libraries(pins2lts-sym PUBLIC + libpins2lts-sym + hre + ) +target_include_directories(pins2lts-sym PUBLIC ${CMAKE_CURRENT_SOURCE_DIR} + ${CMAKE_CURRENT_SOURCE_DIR}/.. + ${CMAKE_CURRENT_BINARY_DIR}/.. + ${CMAKE_SOURCE_DIR}/src + ${CMAKE_CURRENT_SOURCE_DIR}/auxiliary + ${CMAKE_CURRENT_SOURCE_DIR}/alg) +target_compile_options(pins2lts-sym + PRIVATE -DPINS_DLL +) ################### EXECUTABLES: eft2lts-sym#################### add_executable(eft2lts-sym auxiliary/options.c diff --git a/src/spg-lib/CMakeLists.txt b/src/spg-lib/CMakeLists.txt new file mode 100644 index 00000000..fd0e9220 --- /dev/null +++ b/src/spg-lib/CMakeLists.txt @@ -0,0 +1,28 @@ +cmake_minimum_required(VERSION 3.21) + +add_library(spg-lib STATIC) + +set(SPGLIB_HDRS + spg.h + spg-attr.h + spg-options.h + spg-solve.h + spg-strategy.h + ) + + +target_sources(spg-lib + PRIVATE + spg.c + spg-attr.c + spg-options.c + spg-solve.c + spg-strategy.c + ${SPGLIB_HDRS} +) + +target_include_directories(spg-lib PUBLIC ${CMAKE_CURRENT_SOURCE_DIR} + ${CMAKE_CURRENT_SOURCE_DIR}/.. + ${CMAKE_CURRENT_BINARY_DIR}/..) + + From a13a735ea431010efdf90183d4e01a09e3480713 Mon Sep 17 00:00:00 2001 From: Codermann63 <96649204+Codermann63@users.noreply.github.com> Date: Sun, 7 Jan 2024 15:12:07 +0100 Subject: [PATCH 25/40] added bignum with cmake --- Conversion-to-cmake.txt | 3 ++- src/CMakeLists.txt | 1 + src/bignum/CMakeLists.txt | 37 +++++++++++++++++++++++++++++++++++++ src/spg-lib/CMakeLists.txt | 1 + 4 files changed, 41 insertions(+), 1 deletion(-) create mode 100644 src/bignum/CMakeLists.txt diff --git a/Conversion-to-cmake.txt b/Conversion-to-cmake.txt index 04f09bec..4a42dd85 100644 --- a/Conversion-to-cmake.txt +++ b/Conversion-to-cmake.txt @@ -50,5 +50,6 @@ TODO: GITERROR:"ltl2ba cannot be made with cmake" in gitmodules change from "url TODO: the same problem with simplemap.h ---------------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: variablity in #if defined(HAVE_GMP_H) and #elif defined(HAVE_TOMMATH_H) ---------------src/--------------------- diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 23270e79..d9288a83 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -40,3 +40,4 @@ add_subdirectory(lts-io) add_subdirectory(dm) add_subdirectory(mc-lib) add_subdirectory(spg-lib) +add_subdirectory(bignum) diff --git a/src/bignum/CMakeLists.txt b/src/bignum/CMakeLists.txt new file mode 100644 index 00000000..e52cfbd4 --- /dev/null +++ b/src/bignum/CMakeLists.txt @@ -0,0 +1,37 @@ + +cmake_minimum_required(VERSION 3.21) + +add_library(bignum STATIC) + +set(HAVE_GMP_H on) + +target_sources(bignum + PRIVATE + bignum.h +) +option(HAVE_LIBGMP off) +if(HAVE_LIBGMP) + target_sources(bignum + PRIVATE + bignum-gmp.c + #add lib -lgmp + ) + +option(HAVE_LIBTOMMATH off) +elseif(HAVE_LIBTOMMATH) + target_sources(bignum + PRIVATE + bignum-tommath.c + #add lib -tommath + ) +else() + target_sources(bignum + PRIVATE + bignum-ll.c + ) +endif() + +target_include_directories(bignum PUBLIC ${CMAKE_CURRENT_SOURCE_DIR} + ${CMAKE_CURRENT_SOURCE_DIR}/.. + ${CMAKE_CURRENT_BINARY_DIR}/..) + diff --git a/src/spg-lib/CMakeLists.txt b/src/spg-lib/CMakeLists.txt index fd0e9220..d22084d7 100644 --- a/src/spg-lib/CMakeLists.txt +++ b/src/spg-lib/CMakeLists.txt @@ -25,4 +25,5 @@ target_include_directories(spg-lib PUBLIC ${CMAKE_CURRENT_SOURCE_DIR} ${CMAKE_CURRENT_SOURCE_DIR}/.. ${CMAKE_CURRENT_BINARY_DIR}/..) +target_link_libraries(spg-lib bignum) From fabf0b39414f91678cc8ad30ec82a02b6421b7c9 Mon Sep 17 00:00:00 2001 From: Codermann63 <96649204+Codermann63@users.noreply.github.com> Date: Wed, 10 Jan 2024 12:58:18 +0100 Subject: [PATCH 26/40] implemented executable for pins2lts-sym --- CMakeLists.txt | 1 + Conversion-to-cmake.txt | 4 ++++ REMOVEWHENDONE.c | 5 ----- lib/CMakeLists.txt | 17 ++++++++++++++++ src/CMakeLists.txt | 2 ++ src/hre-io/CMakeLists.txt | 36 +++++++++++++++++++++++++++++++++ src/hre/CMakeLists.txt | 10 ++++++++- src/hre/config.h.in | 4 ++++ src/lts-io/CMakeLists.txt | 2 ++ src/ltsmin-lib/CMakeLists.txt | 8 ++++++-- src/pins-lib/CMakeLists.txt | 3 ++- src/pins-lib/por/CMakeLists.txt | 33 ++++++++++++++++++++++++++++++ src/pins2lts-sym/CMakeLists.txt | 4 +++- src/vset-lib/CMakeLists.txt | 4 ++++ 14 files changed, 123 insertions(+), 10 deletions(-) delete mode 100644 REMOVEWHENDONE.c create mode 100644 lib/CMakeLists.txt create mode 100644 src/hre-io/CMakeLists.txt create mode 100644 src/pins-lib/por/CMakeLists.txt diff --git a/CMakeLists.txt b/CMakeLists.txt index 45e9b9f8..efc7a18b 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -40,6 +40,7 @@ endif() #TODO get sylvan(?) via FetchContent? or make it a submodule add_subdirectory(src) +add_subdirectory(lib) #TODO LATER add_subdirectory(spins) #TODO LATER add_subdirectory(scoop) add_subdirectory(lemon) diff --git a/Conversion-to-cmake.txt b/Conversion-to-cmake.txt index 4a42dd85..3fcd6a18 100644 --- a/Conversion-to-cmake.txt +++ b/Conversion-to-cmake.txt @@ -1,5 +1,9 @@ GENERAL NOTES: - Check if flex installation in install script 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 +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 ----------------root----------------- Unsure what ltsmin should be build as? a library needs sources, and an excecutable creates an executable (which automake does not do) diff --git a/REMOVEWHENDONE.c b/REMOVEWHENDONE.c deleted file mode 100644 index 6f07c386..00000000 --- a/REMOVEWHENDONE.c +++ /dev/null @@ -1,5 +0,0 @@ -//This files is created for developments of the cmake version - -int main() { - return 0; -} diff --git a/lib/CMakeLists.txt b/lib/CMakeLists.txt new file mode 100644 index 00000000..67442af8 --- /dev/null +++ b/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) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index d9288a83..9317bb1e 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -41,3 +41,5 @@ add_subdirectory(dm) add_subdirectory(mc-lib) add_subdirectory(spg-lib) add_subdirectory(bignum) +add_subdirectory(hre-io) + diff --git a/src/hre-io/CMakeLists.txt b/src/hre-io/CMakeLists.txt new file mode 100644 index 00000000..4e50b6e7 --- /dev/null +++ b/src/hre-io/CMakeLists.txt @@ -0,0 +1,36 @@ + +cmake_minimum_required(VERSION 3.10) + +add_library(hre-io STATIC) + +target_sources(hre-io + PRIVATE + user.h types.h + hre_archive.c archive.h arch_object.h + hre_archive_dir.c + hre_client_server.c client-server.h + hre_fifo.c fifo.h + hre_gcf_common.c gcf_common.h + hre_gcf_read.c + hre_gcf_write.c + hre_gzstream.c + hre_raf.c raf.h raf_object.h + hre_stream.c stream.h stream_object.h + hre_stream_buffer.c + hre_stream_diff32.c + hre_stream_fd.c + hre_stream_mem.c + hre_stream_rle32.c + hre_struct_io.c struct_io.h + hre_zip_io.c +) + +# hre uses zlib +find_package(ZLIB REQUIRED) +target_link_libraries(hre-io ZLIB::ZLIB util-lib) + +# Include directories +target_include_directories(hre-io PUBLIC ${CMAKE_CURRENT_SOURCE_DIR} + ${CMAKE_CURRENT_SOURCE_DIR}/.. + ${CMAKE_CURRENT_BINARY_DIR}/..) + diff --git a/src/hre/CMakeLists.txt b/src/hre/CMakeLists.txt index 99257af4..84e8fe4f 100644 --- a/src/hre/CMakeLists.txt +++ b/src/hre/CMakeLists.txt @@ -48,13 +48,21 @@ target_sources(hre ${HRE_HDRS} ) +# hre uses popt +find_library(POPT_LIB popt REQUIRED) +target_link_libraries(hre ${POPT_LIB}) + +# hre uses LTDL. +find_library(LTDL_LIB ltdl REQUIRED) +target_link_libraries(hre ${LTDL_LIB}) + SET(HAVE_POSIX_MEMALIGN "system has posix memalign" ON) SET(_GNU_SOURCE "System uses GNU" ON) configure_file(${PROJECT_SOURCE_DIR}/src/hre/config.h.in ${PROJECT_SOURCE_DIR}/src/hre/config.h) target_compile_options(hre - PUBLIC -I${CMAKE_SOURCE_DIR}/lib -I${CMAKE_SOURCE_DIR}/lib + PUBLIC -I${CMAKE_SOURCE_DIR}/lib -I${CMAKE_BINARY_DIR}/lib ) # Include directories diff --git a/src/hre/config.h.in b/src/hre/config.h.in index 61dc2e9b..09b1e7e9 100644 --- a/src/hre/config.h.in +++ b/src/hre/config.h.in @@ -30,3 +30,7 @@ /* Define to 1 if you have the `_aligned_malloc' function. */ #cmakedefine HAVE__ALIGNED_MALLOC + +/* Provide a hint to the optimizer */ +#define __assume(cond) do { if (!(cond)) __builtin_unreachable(); } while (0) + diff --git a/src/lts-io/CMakeLists.txt b/src/lts-io/CMakeLists.txt index dc6ad944..57b3d1dc 100644 --- a/src/lts-io/CMakeLists.txt +++ b/src/lts-io/CMakeLists.txt @@ -20,6 +20,8 @@ target_sources(lts-io ${LTSIO_HDRS} ) +target_link_libraries(lts-io hre-io util-lib hre) + # Include directories target_include_directories(lts-io PUBLIC ${CMAKE_CURRENT_SOURCE_DIR} ${CMAKE_CURRENT_SOURCE_DIR}/.. diff --git a/src/ltsmin-lib/CMakeLists.txt b/src/ltsmin-lib/CMakeLists.txt index 70643566..e69e61fe 100644 --- a/src/ltsmin-lib/CMakeLists.txt +++ b/src/ltsmin-lib/CMakeLists.txt @@ -24,6 +24,7 @@ FIND_PACKAGE(FLEX REQUIRED) foreach(FLEXFILE ${FLEXFILES}) FLEX_TARGET(LTSMINLEXER ${FLEXFILE}.l ${CMAKE_CURRENT_BINARY_DIR}/${FLEXFILE}.c DEFINES_FILE ${CMAKE_CURRENT_BINARY_DIR}/${FLEXFILE}.h) + list(APPEND FLEXOUTPUTLIST ${FLEX_LTSMINLEXER_OUTPUTS}) endforeach() @@ -66,10 +67,13 @@ target_sources(ltsmin-lib mucalc-syntax.c #ltl2spot.cpp ${LTSMINLIB_HDRS} - ${FLEX_LTSMINLEXER_OUTPUTS} + ${FLEXOUTPUTLIST} ) -target_link_libraries(ltsmin-lib ${FLEX_LIBRARIES}) + + +target_link_libraries(ltsmin-lib ${FLEX_LIBRARIES} + ltl2ba) diff --git a/src/pins-lib/CMakeLists.txt b/src/pins-lib/CMakeLists.txt index 5b44ad5d..7bfcafad 100644 --- a/src/pins-lib/CMakeLists.txt +++ b/src/pins-lib/CMakeLists.txt @@ -43,6 +43,7 @@ add_dependencies(pins-lib ltsmin-lib hre) +target_link_libraries(pins-lib por-lib) -#TODO: add_subdirectory(por) +add_subdirectory(por) diff --git a/src/pins-lib/por/CMakeLists.txt b/src/pins-lib/por/CMakeLists.txt new file mode 100644 index 00000000..47f9b682 --- /dev/null +++ b/src/pins-lib/por/CMakeLists.txt @@ -0,0 +1,33 @@ + +cmake_minimum_required(VERSION 3.21) + +add_library(por-lib STATIC) + +set(PORLIB_HDRS + pins2pins-por.h + pins2pins-por-check.h + por-ample.h + por-beam.h + por-deletion.h + por-internal.h + por-leap.h + por-lipton.h + por-tr.h +) + +target_sources(por-lib + PRIVATE + pins2pins-por.c + pins2pins-por-check.c + por-ample.c + por-beam.c + por-deletion.c + por-leap.c + por-lipton.c + por-tr.c + ${PORLIB_HDRS} +) + +target_include_directories(por-lib PUBLIC ${CMAKE_CURRENT_SOURCE_DIR} + ${CMAKE_SOURCE_DIR}/src + ${CMAKE_BINARY_DIR}/src) diff --git a/src/pins2lts-sym/CMakeLists.txt b/src/pins2lts-sym/CMakeLists.txt index 91a8263b..f1ce30e7 100644 --- a/src/pins2lts-sym/CMakeLists.txt +++ b/src/pins2lts-sym/CMakeLists.txt @@ -53,6 +53,7 @@ add_executable(pins2lts-sym target_link_libraries(pins2lts-sym PUBLIC libpins2lts-sym hre + general-lib ) target_include_directories(pins2lts-sym PUBLIC ${CMAKE_CURRENT_SOURCE_DIR} ${CMAKE_CURRENT_SOURCE_DIR}/.. @@ -60,8 +61,9 @@ target_include_directories(pins2lts-sym PUBLIC ${CMAKE_CURRENT_SOURCE_DIR} ${CMAKE_SOURCE_DIR}/src ${CMAKE_CURRENT_SOURCE_DIR}/auxiliary ${CMAKE_CURRENT_SOURCE_DIR}/alg) + target_compile_options(pins2lts-sym - PRIVATE -DPINS_DLL + PRIVATE -DPINS_DLL -I${CMAKE_SOURCE_DIR}/lib -I${CMAKE_BINARY_DIR}/lib ) ################### EXECUTABLES: eft2lts-sym#################### add_executable(eft2lts-sym diff --git a/src/vset-lib/CMakeLists.txt b/src/vset-lib/CMakeLists.txt index 15771a7e..f9375751 100644 --- a/src/vset-lib/CMakeLists.txt +++ b/src/vset-lib/CMakeLists.txt @@ -54,6 +54,10 @@ if(HAVE_LIBDDD) vset_ddd.cpp) endif() +target_link_libraries(vset-lib PUBLIC + util-lib + hre-io) + target_include_directories(vset-lib PUBLIC ${CMAKE_CURRENT_SOURCE_DIR} ${CMAKE_CURRENT_SOURCE_DIR}/.. ${CMAKE_CURRENT_BINARY_DIR}/..) From 761b6e4aee6c6e6003fd301a00db3e7933ca1b3f Mon Sep 17 00:00:00 2001 From: Codermann63 <96649204+Codermann63@users.noreply.github.com> Date: Wed, 10 Jan 2024 13:28:07 +0100 Subject: [PATCH 27/40] implemented the executable of eft2lts-sym --- src/pins2lts-sym/CMakeLists.txt | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/pins2lts-sym/CMakeLists.txt b/src/pins2lts-sym/CMakeLists.txt index f1ce30e7..93cd1685 100644 --- a/src/pins2lts-sym/CMakeLists.txt +++ b/src/pins2lts-sym/CMakeLists.txt @@ -72,6 +72,8 @@ add_executable(eft2lts-sym ) target_link_libraries(eft2lts-sym PRIVATE libpins2lts-sym + hre + general-lib ) target_include_directories(eft2lts-sym PUBLIC ${CMAKE_CURRENT_SOURCE_DIR} ${CMAKE_CURRENT_SOURCE_DIR}/.. @@ -79,7 +81,9 @@ target_include_directories(eft2lts-sym PUBLIC ${CMAKE_CURRENT_SOURCE_DIR} ${CMAKE_SOURCE_DIR}/src ${CMAKE_CURRENT_SOURCE_DIR}/auxiliary ${CMAKE_CURRENT_SOURCE_DIR}/alg) - +target_compile_options(eft2lts-sym + PRIVATE -DETF -I${CMAKE_SOURCE_DIR}/lib -I${CMAKE_BINARY_DIR}/lib +) #################Required NOT included yet###################3 #eft: eft2lts-sym From 47929de5bd2add8c7f6a390d807a378504a2f7bc Mon Sep 17 00:00:00 2001 From: Codermann63 <96649204+Codermann63@users.noreply.github.com> Date: Wed, 10 Jan 2024 16:48:02 +0100 Subject: [PATCH 28/40] implemented executable of pnml2lts-sym --- src/CMakeLists.txt | 2 +- src/andl-lib/CMakeLists.txt | 51 +++++++++++++++++++++++++++++++++ src/pins2lts-sym/CMakeLists.txt | 31 ++++++++++++++++++-- 3 files changed, 80 insertions(+), 4 deletions(-) create mode 100644 src/andl-lib/CMakeLists.txt diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 9317bb1e..bd41cbaa 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -42,4 +42,4 @@ add_subdirectory(mc-lib) add_subdirectory(spg-lib) add_subdirectory(bignum) add_subdirectory(hre-io) - +add_subdirectory(andl-lib) diff --git a/src/andl-lib/CMakeLists.txt b/src/andl-lib/CMakeLists.txt new file mode 100644 index 00000000..95123d0b --- /dev/null +++ b/src/andl-lib/CMakeLists.txt @@ -0,0 +1,51 @@ + + + +#BISON_TARGET(MyParser parser.y ${CMAKE_CURRENT_BINARY_DIR}/parser.cpp +# DEFINES_FILE ${CMAKE_CURRENT_BINARY_DIR}/parser.h) + +FIND_PACKAGE(FLEX REQUIRED) + +FLEX_TARGET(ANDLLEXER andl-lexer.l ${CMAKE_CURRENT_BINARY_DIR}/andl-lexer.c + DEFINES_FILE ${CMAKE_CURRENT_BINARY_DIR}/andl-lexer.h) + +find_package(BISON REQUIRED) + +# Hack around FindBISON's incorrect use of separate_arguments https://stackoverflow.com/questions/71369325/cmake-incorrectly-escapes-bison-target-option +if (CMAKE_VERSION VERSION_LESS 3.24) + function(patch_flags variable access value ip stack) + set(invalid "${CMAKE_CURRENT_BINARY_DIR}") + separate_arguments(invalid) + string(REPLACE "${invalid}" "${CMAKE_CURRENT_BINARY_DIR}" "${variable}" "${value}") + set("${variable}" "${${variable}}" PARENT_SCOPE) + endfunction() + variable_watch(BISON_TARGET_cmdopt patch_flags) + + BISON_TARGET(ANDLPARSER "andl-parser.y" "${CMAKE_CURRENT_BINARY_DIR}/libandl_la-andl-parser.c" + COMPILE_FLAGS "--defines=${CMAKE_CURRENT_BINARY_DIR}/libandl_la-andl-parser.h") +else() + BISON_TARGET(ANDLPARSER "andl-parser.y" "${CMAKE_CURRENT_BINARY_DIR}/libandl_la-andl-parser.c" + DEFINE_FILE "${CMAKE_CURRENT_BINARY_DIR}/libandl_la-andl-parser.h") +endif () + + + +ADD_FLEX_BISON_DEPENDENCY(ANDLLEXER ANDLPARSER) + + +add_library(andl-lib STATIC + andl-parser.y + ${FLEX_ANDLLEXER_OUTPUTS} + ${BISON_ANDLPARSER_OUTPUTS} + ) + + +target_link_libraries(andl-lib ${FLEX_LIBRARIES} ${BISON_LIBRARIES}) + +target_include_directories(andl-lib PUBLIC ${CMAKE_CURRENT_SOURCE_DIR} + ${CMAKE_CURRENT_BINARY_DIR}/.. + ${CMAKE_SOURCE_DIR}/ltl2ba + ${CMAKE_SOURCE_DIR}/src) + + + diff --git a/src/pins2lts-sym/CMakeLists.txt b/src/pins2lts-sym/CMakeLists.txt index 93cd1685..411cd149 100644 --- a/src/pins2lts-sym/CMakeLists.txt +++ b/src/pins2lts-sym/CMakeLists.txt @@ -84,9 +84,34 @@ target_include_directories(eft2lts-sym PUBLIC ${CMAKE_CURRENT_SOURCE_DIR} target_compile_options(eft2lts-sym PRIVATE -DETF -I${CMAKE_SOURCE_DIR}/lib -I${CMAKE_BINARY_DIR}/lib ) -#################Required NOT included yet###################3 -#eft: eft2lts-sym + +################### OPTIONAL XECUTABLES: eft2lts-sym#################### +set(HAVE_PNML ON) #TODO remove this when pnml check is implemented +if (HAVE_PNML) + add_executable(pnml2lts-sym + auxiliary/options.c + ../pins-lib/modules/pnml-pins.c ../pins-lib/modules/pnml-pins.h + ) + find_package(LibXml2 REQUIRED) + target_link_libraries(pnml2lts-sym PRIVATE + libpins2lts-sym + hre + general-lib + andl-lib + LibXml2::LibXml2 + ) + target_include_directories(pnml2lts-sym PUBLIC ${CMAKE_CURRENT_SOURCE_DIR} + ${CMAKE_CURRENT_SOURCE_DIR}/.. + ${CMAKE_CURRENT_BINARY_DIR}/.. + ${CMAKE_SOURCE_DIR}/src + ${CMAKE_CURRENT_SOURCE_DIR}/auxiliary + ${CMAKE_CURRENT_SOURCE_DIR}/alg) + target_compile_options(pnml2lts-sym + PRIVATE -DPNML -I${CMAKE_SOURCE_DIR}/lib -I${CMAKE_BINARY_DIR}/lib + ) +endif() +#PNML: pnml2lts-sym #################Optional NOT included yet################ @@ -96,6 +121,6 @@ target_compile_options(eft2lts-sym #libpbes: pbes2lts-sym #DVE: dve2lts-sym #SPINS: prom2lts-sym -#PNML: pnml2lts-sym + #PROB: prob2lts-sym From 407f4cb232dc78fdf53043e12f05afc5456c0bed Mon Sep 17 00:00:00 2001 From: Codermann63 <96649204+Codermann63@users.noreply.github.com> Date: Wed, 10 Jan 2024 16:54:47 +0100 Subject: [PATCH 29/40] implemented executable dve2lts-sym --- src/pins2lts-sym/CMakeLists.txt | 36 +++++++++++++++++++++++++++++++-- 1 file changed, 34 insertions(+), 2 deletions(-) diff --git a/src/pins2lts-sym/CMakeLists.txt b/src/pins2lts-sym/CMakeLists.txt index 411cd149..0d8d5bad 100644 --- a/src/pins2lts-sym/CMakeLists.txt +++ b/src/pins2lts-sym/CMakeLists.txt @@ -86,7 +86,7 @@ target_compile_options(eft2lts-sym ) -################### OPTIONAL XECUTABLES: eft2lts-sym#################### +################### OPTIONAL EXECUTABLES: pnml2lts-sym#################### set(HAVE_PNML ON) #TODO remove this when pnml check is implemented if (HAVE_PNML) add_executable(pnml2lts-sym @@ -111,9 +111,41 @@ if (HAVE_PNML) PRIVATE -DPNML -I${CMAKE_SOURCE_DIR}/lib -I${CMAKE_BINARY_DIR}/lib ) endif() -#PNML: pnml2lts-sym +################### OPTIONAL EXECUTABLES: dve2lts-sym#################### +set(HAVE_DVE ON) #TODO remove this when pnml check is implemented +if (HAVE_DVE) + add_executable(dve2lts-sym + auxiliary/options.c + ../pins-lib/modules/dve-pins.c ../pins-lib/modules/dve-pins.h + ) + find_package(LibXml2 REQUIRED) + target_link_libraries(dve2lts-sym PRIVATE + libpins2lts-sym + hre + general-lib + ) + target_include_directories(dve2lts-sym PUBLIC ${CMAKE_CURRENT_SOURCE_DIR} + ${CMAKE_CURRENT_SOURCE_DIR}/.. + ${CMAKE_CURRENT_BINARY_DIR}/.. + ${CMAKE_SOURCE_DIR}/src + ${CMAKE_CURRENT_SOURCE_DIR}/auxiliary + ${CMAKE_CURRENT_SOURCE_DIR}/alg) + target_compile_options(dve2lts-sym + PRIVATE -DDIVINE -I${CMAKE_SOURCE_DIR}/lib -I${CMAKE_BINARY_DIR}/lib + ) +endif() + + +# dve2lts-sym +#dve2lts_sym_SOURCES = auxiliary/options.c +#dve2lts_sym_SOURCES += ../pins-lib/modules/dve-pins.c ../pins-lib/modules/dve-pins.h +#dve2lts_sym_LDADD = $(LIBZZZ) $(DVE_LIBS) $(LIBLTDL) +#dve2lts_sym_CFLAGS = $(SYM_C_FLAGS) +#dve2lts_sym_CPPFLAGS = -DDIVINE $(DIVINE_CPPFLAGS) $(LTDLINCL) $(SYM_CPP_FLAGS) +#dve2lts_sym_LDFLAGS = $(DIVINE_LDFLAGS) $(SYM_LD_FLAGS) +#nodist_EXTRA_dve2lts_sym_SOURCES = automake-force-linker.cxx # req. by vset #################Optional NOT included yet################ #libstep: lpo2lts-sym #libmcrl2: lps2lts-sym From f3411d52c81706389fda188bf7afc37c088d92e4 Mon Sep 17 00:00:00 2001 From: Codermann63 <96649204+Codermann63@users.noreply.github.com> Date: Fri, 12 Jan 2024 10:21:48 +0100 Subject: [PATCH 30/40] Cleanup --- CMakeLists.txt | 16 +------------ Conversion-to-cmake.txt | 42 ++++++++++++++++----------------- src/ce/CMakeLists.txt | 1 + src/ltsmin-lib/CMakeLists.txt | 7 +++++- src/pins2lts-sym/CMakeLists.txt | 38 +++++++---------------------- src/util-lib/CMakeLists.txt | 3 ++- src/util-lib/fast_set.c | 2 +- src/util-lib/simplemap.h | 2 +- src/vset-lib/CMakeLists.txt | 3 ++- src/vset-lib/vset_listdd64.c | 2 +- 10 files changed, 44 insertions(+), 72 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index efc7a18b..dec3a7d6 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -10,7 +10,7 @@ project(ltsmin Set(CMAKE_CXX_STANDARD 11) Set(CMAKE_CXX_STANDARD_REQUIRED True) -# Add CMake modules path +# Add CMake modules path | TODO don't think this is necessary list(APPEND CMAKE_MODULE_PATH "${CMAKE_CURRENT_LIST_DIR}/cmake/") # update submodules: @@ -41,25 +41,11 @@ endif() add_subdirectory(src) add_subdirectory(lib) -#TODO LATER add_subdirectory(spins) -#TODO LATER add_subdirectory(scoop) add_subdirectory(lemon) add_subdirectory(ltl2ba) configure_file(${PROJECT_SOURCE_DIR}/config.h.in ${PROJECT_SOURCE_DIR}/ltl2ba/config.h) -#add_executable(${PROJECT_NAME} REMOVEWHENDONE.c) - -#target_include_directories(ltsmin PUBLIC ${CMAKE_SOURCE_DIR}/src -# ${CMAKE_SOURCE_DIR}/ltl2ba) - -#target_link_libraries(${PROJECT_NAME} PRIVATE ce) -#target_link_libraries(${PROJECT_NAME} PRIVATE hre) -#target_link_libraries(${PROJECT_NAME} PRIVATE ltsmin-lib) -#target_link_libraries(${PROJECT_NAME} PRIVATE pins-lib) -#target_link_libraries(${PROJECT_NAME} PRIVATE ltl2ba) - - #TODO add options for examples, tests and documentation diff --git a/Conversion-to-cmake.txt b/Conversion-to-cmake.txt index 3fcd6a18..c2990af8 100644 --- a/Conversion-to-cmake.txt +++ b/Conversion-to-cmake.txt @@ -1,30 +1,26 @@ GENERAL NOTES: -- Check if flex installation in install script is good enough. Maybe a make error? If no error when running make, delete this note. +- 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 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 ----------------root----------------- -Unsure what ltsmin should be build as? a library needs sources, and an excecutable creates an executable (which automake does not do) ---------------src/hre---------------- - Note: FILE:hre_malloc has compiler error, does not seem to be necessary for autotools to configure the whole project. The error is in the "RTalign" function. You just need to declare ret in the start of the function. - TODO: Check if other sources can be left out for making of project. 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 - Note: bufs.c: can't find mpi.h - Note: Ddlts.c: can't find mpi.h - Note: I don't know what mpi.h is or where to find/generate it. I cannot find it in the automake build version. A LOT OF FILES DEPEND ON mpi.h in ce: https://stackoverflow.com/questions/26920083/fatal-error-mpi-h-no-such-file-or-directory-include-mpi-h + 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. - TODO: uncomment ltl2spot.cpp and make it depend if spot is enabled or disabled ---------------lemon--------------------- @@ -32,28 +28,30 @@ Unsure what ltsmin should be build as? a library needs sources, and an excecutab 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-------------------- -When making with cmake it needs a config.h that was created by autotools (i suggest to create it with configue_file(config.h.in config.h) and manually create a config.h.in) - also remove config.h.in from gitignore -TODO: GITERROR:"ltl2ba cannot be made with cmake" in gitmodules change from "url = https://github.com/codermann63/ltl2ba.git" to u"rl = https://github.com/utwente-fmt/ltl2ba.git" - - + 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: -------------------- - Note: is dependend on generated files from ltsmin-libΒ¨ - TODO: convert subdirectory por and add it as subdirectory to CMakeLists.txt ---------------src/pins2lts-sym--------------------- - TODO: check if all compiler flags are given like the automake version - + 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 - TODO: vset_listdd64.c could not find config.h. I've changed the include to hre/config.h (because vset_listdd has and include for hre/config.h). CHECK IF CORRECT + ---------------src/util-lib--------------------- - QUESTION: fast_set.c has an include to config.h. Automake does not generate one with its make and fast_hash.c has an include to hre/config.h. I've changed the include to hre/config.h. TODO check if correct - ADDITIONAL INFO: fast_set.h has include of hre/config.h - TODO: the same problem with simplemap.h + ---------------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: variablity in #if defined(HAVE_GMP_H) and #elif defined(HAVE_TOMMATH_H) + TODO: implement variablity in #if defined(HAVE_GMP_H) and #elif defined(HAVE_TOMMATH_H) ---------------src/--------------------- + + + + diff --git a/src/ce/CMakeLists.txt b/src/ce/CMakeLists.txt index 236d4a22..8478bd53 100644 --- a/src/ce/CMakeLists.txt +++ b/src/ce/CMakeLists.txt @@ -1,3 +1,4 @@ +#TODO. this is not finished add_library(ce STATIC) set(CE_HDRS diff --git a/src/ltsmin-lib/CMakeLists.txt b/src/ltsmin-lib/CMakeLists.txt index e69e61fe..8101da12 100644 --- a/src/ltsmin-lib/CMakeLists.txt +++ b/src/ltsmin-lib/CMakeLists.txt @@ -65,11 +65,16 @@ target_sources(ltsmin-lib lts-type.c mucalc-grammar.c mucalc-syntax.c - #ltl2spot.cpp ${LTSMINLIB_HDRS} ${FLEXOUTPUTLIST} ) +if(HAVE_SPOT) + target_sources(ltsmin-lib + PRIVATE + ltl2spot.cpp) +endif() + target_link_libraries(ltsmin-lib ${FLEX_LIBRARIES} diff --git a/src/pins2lts-sym/CMakeLists.txt b/src/pins2lts-sym/CMakeLists.txt index 0d8d5bad..5ec0c2ba 100644 --- a/src/pins2lts-sym/CMakeLists.txt +++ b/src/pins2lts-sym/CMakeLists.txt @@ -1,17 +1,5 @@ add_subdirectory(maxsum) -############REQUIRED################## -#pins2ltsmin-sym - - -#set(LIBZZZ -# libpins2lts_sym.la -# ../pins-lib/libpins.la -# ../vset-lib/libvset.la -# maxsum/libmaxsum.la -# ../spg-lib/libspg.la -# ../mc-lib/libmc.la -# $(top_builddir)/lib/libgnu.la) - +################### LIBRARY: pins2lts-sym#################### add_library( libpins2lts-sym pins2lts-sym.c ) target_sources(libpins2lts-sym INTERFACE @@ -24,6 +12,7 @@ target_sources(libpins2lts-sym INTERFACE alg/sat.c alg/sat.h auxiliary/output.c auxiliary/output.h auxiliary/prop.c auxiliary/prop.h) + target_link_libraries(libpins2lts-sym PUBLIC pins-lib ltsmin-lib @@ -44,7 +33,6 @@ target_include_directories(libpins2lts-sym PUBLIC ${CMAKE_CURRENT_SOURCE_DIR} ${CMAKE_CURRENT_SOURCE_DIR}/auxiliary ${CMAKE_CURRENT_SOURCE_DIR}/alg) - ################### EXECUTABLES: pins2lts-sym#################### add_executable(pins2lts-sym auxiliary/options.c auxiliary/options.h @@ -63,7 +51,7 @@ target_include_directories(pins2lts-sym PUBLIC ${CMAKE_CURRENT_SOURCE_DIR} ${CMAKE_CURRENT_SOURCE_DIR}/alg) target_compile_options(pins2lts-sym - PRIVATE -DPINS_DLL -I${CMAKE_SOURCE_DIR}/lib -I${CMAKE_BINARY_DIR}/lib + PRIVATE -DPINS_DLL -I${CMAKE_SOURCE_DIR}/lib -I${CMAKE_BINARY_DIR}/lib #include of lib might not be necessary ) ################### EXECUTABLES: eft2lts-sym#################### add_executable(eft2lts-sym @@ -108,8 +96,9 @@ if (HAVE_PNML) ${CMAKE_CURRENT_SOURCE_DIR}/auxiliary ${CMAKE_CURRENT_SOURCE_DIR}/alg) target_compile_options(pnml2lts-sym - PRIVATE -DPNML -I${CMAKE_SOURCE_DIR}/lib -I${CMAKE_BINARY_DIR}/lib - ) + PRIVATE -DPNML -I${CMAKE_SOURCE_DIR}/lib -I${CMAKE_BINARY_DIR}/lib #include of lib might not be necessary +) + endif() @@ -133,25 +122,16 @@ if (HAVE_DVE) ${CMAKE_CURRENT_SOURCE_DIR}/auxiliary ${CMAKE_CURRENT_SOURCE_DIR}/alg) target_compile_options(dve2lts-sym - PRIVATE -DDIVINE -I${CMAKE_SOURCE_DIR}/lib -I${CMAKE_BINARY_DIR}/lib - ) + PRIVATE -DDIVINE -I${CMAKE_SOURCE_DIR}/lib -I${CMAKE_BINARY_DIR}/lib #include of lib might not be necessary +) + endif() - -# dve2lts-sym -#dve2lts_sym_SOURCES = auxiliary/options.c -#dve2lts_sym_SOURCES += ../pins-lib/modules/dve-pins.c ../pins-lib/modules/dve-pins.h -#dve2lts_sym_LDADD = $(LIBZZZ) $(DVE_LIBS) $(LIBLTDL) -#dve2lts_sym_CFLAGS = $(SYM_C_FLAGS) -#dve2lts_sym_CPPFLAGS = -DDIVINE $(DIVINE_CPPFLAGS) $(LTDLINCL) $(SYM_CPP_FLAGS) -#dve2lts_sym_LDFLAGS = $(DIVINE_LDFLAGS) $(SYM_LD_FLAGS) -#nodist_EXTRA_dve2lts_sym_SOURCES = automake-force-linker.cxx # req. by vset #################Optional NOT included yet################ #libstep: lpo2lts-sym #libmcrl2: lps2lts-sym #scoop: mapa2lts-sym #libpbes: pbes2lts-sym -#DVE: dve2lts-sym #SPINS: prom2lts-sym #PROB: prob2lts-sym diff --git a/src/util-lib/CMakeLists.txt b/src/util-lib/CMakeLists.txt index 13ffc183..3fab8530 100644 --- a/src/util-lib/CMakeLists.txt +++ b/src/util-lib/CMakeLists.txt @@ -3,7 +3,8 @@ add_dependencies(util-lib hre) target_include_directories(util-lib PUBLIC ${CMAKE_CURRENT_SOURCE_DIR} ${CMAKE_CURRENT_SOURCE_DIR}/.. - ${CMAKE_CURRENT_BINARY_DIR}/..) + ${CMAKE_CURRENT_BINARY_DIR}/.. + ${CMAKE_SOURCE_DIR}/src/hre) set(UTILLIB_HDRS balloc.h diff --git a/src/util-lib/fast_set.c b/src/util-lib/fast_set.c index 59758034..13461643 100644 --- a/src/util-lib/fast_set.c +++ b/src/util-lib/fast_set.c @@ -1,4 +1,4 @@ -#include +#include #include #include diff --git a/src/util-lib/simplemap.h b/src/util-lib/simplemap.h index 1fa544e8..4edafd4d 100644 --- a/src/util-lib/simplemap.h +++ b/src/util-lib/simplemap.h @@ -8,7 +8,7 @@ #ifndef SIMPLEMAP_H_ #define SIMPLEMAP_H_ -#include +#include #include #include diff --git a/src/vset-lib/CMakeLists.txt b/src/vset-lib/CMakeLists.txt index f9375751..fda0c144 100644 --- a/src/vset-lib/CMakeLists.txt +++ b/src/vset-lib/CMakeLists.txt @@ -60,4 +60,5 @@ target_link_libraries(vset-lib PUBLIC target_include_directories(vset-lib PUBLIC ${CMAKE_CURRENT_SOURCE_DIR} ${CMAKE_CURRENT_SOURCE_DIR}/.. - ${CMAKE_CURRENT_BINARY_DIR}/..) + ${CMAKE_CURRENT_BINARY_DIR}/.. + ${CMAKE_SOURCE_DIR}/src/hre) diff --git a/src/vset-lib/vset_listdd64.c b/src/vset-lib/vset_listdd64.c index 5d1c9584..d4493167 100644 --- a/src/vset-lib/vset_listdd64.c +++ b/src/vset-lib/vset_listdd64.c @@ -1,4 +1,4 @@ -#include +#include #include #include From 614b6af47f33993a37bda9c01846f696fac6c084 Mon Sep 17 00:00:00 2001 From: Codermann63 <96649204+Codermann63@users.noreply.github.com> Date: Fri, 12 Jan 2024 11:46:18 +0100 Subject: [PATCH 31/40] added bitset_test --- CMakeLists.txt | 4 ++++ Conversion-to-cmake.txt | 2 +- src/CMakeLists.txt | 1 + src/hre/CMakeLists.txt | 2 ++ src/tests/CMakeLists.txt | 21 +++++++++++++++++++++ src/util-lib/CMakeLists.txt | 2 +- 6 files changed, 30 insertions(+), 2 deletions(-) create mode 100644 src/tests/CMakeLists.txt diff --git a/CMakeLists.txt b/CMakeLists.txt index dec3a7d6..2b38c472 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -1,5 +1,7 @@ cmake_minimum_required(VERSION 3.21) + + project(ltsmin VERSION 3.0.3 DESCRIPTION "TODO" @@ -10,6 +12,8 @@ project(ltsmin Set(CMAKE_CXX_STANDARD 11) Set(CMAKE_CXX_STANDARD_REQUIRED True) +include(CTest) + # Add CMake modules path | TODO don't think this is necessary list(APPEND CMAKE_MODULE_PATH "${CMAKE_CURRENT_LIST_DIR}/cmake/") diff --git a/Conversion-to-cmake.txt b/Conversion-to-cmake.txt index c2990af8..b39a2418 100644 --- a/Conversion-to-cmake.txt +++ b/Conversion-to-cmake.txt @@ -45,7 +45,7 @@ NEW DEPENDENCIES? 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 diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index bd41cbaa..0dc93d4a 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -43,3 +43,4 @@ add_subdirectory(spg-lib) add_subdirectory(bignum) add_subdirectory(hre-io) add_subdirectory(andl-lib) +add_subdirectory(tests) diff --git a/src/hre/CMakeLists.txt b/src/hre/CMakeLists.txt index 84e8fe4f..9432ddb0 100644 --- a/src/hre/CMakeLists.txt +++ b/src/hre/CMakeLists.txt @@ -56,6 +56,8 @@ target_link_libraries(hre ${POPT_LIB}) find_library(LTDL_LIB ltdl REQUIRED) target_link_libraries(hre ${LTDL_LIB}) +target_link_libraries(hre util-lib) + SET(HAVE_POSIX_MEMALIGN "system has posix memalign" ON) SET(_GNU_SOURCE "System uses GNU" ON) diff --git a/src/tests/CMakeLists.txt b/src/tests/CMakeLists.txt new file mode 100644 index 00000000..8a0de66c --- /dev/null +++ b/src/tests/CMakeLists.txt @@ -0,0 +1,21 @@ + + +#add_test(NAME TestName COMMAND ExecutableToRun arg1 arg2 ...) + + +#add_executable(TestInstantiator TestInstantiator.cxx) +#target_link_libraries(TestInstantiator vtkCommon) +#add_test(NAME TestInstantiator +# COMMAND TestInstantiator) + +#add_test(test_bitset COMMAND test-bitset${EXEEXT}) + +add_executable(TestInstantiator test-bitset.c) +target_link_libraries(TestInstantiator + pins-lib + ltsmin-lib + hre-io + lts-io + hre) +add_test(NAME TestInstantiator + COMMAND TestInstantiator) diff --git a/src/util-lib/CMakeLists.txt b/src/util-lib/CMakeLists.txt index 3fab8530..b279b1f5 100644 --- a/src/util-lib/CMakeLists.txt +++ b/src/util-lib/CMakeLists.txt @@ -1,5 +1,5 @@ add_library(util-lib STATIC) -add_dependencies(util-lib hre) +target_link_libraries(util-lib hre) target_include_directories(util-lib PUBLIC ${CMAKE_CURRENT_SOURCE_DIR} ${CMAKE_CURRENT_SOURCE_DIR}/.. From b35510a9e1386d5e094719f5d01064b17eba0be5 Mon Sep 17 00:00:00 2001 From: Codermann63 <96649204+Codermann63@users.noreply.github.com> Date: Fri, 12 Jan 2024 12:01:08 +0100 Subject: [PATCH 32/40] minor name changes --- src/tests/CMakeLists.txt | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/tests/CMakeLists.txt b/src/tests/CMakeLists.txt index 8a0de66c..262e805c 100644 --- a/src/tests/CMakeLists.txt +++ b/src/tests/CMakeLists.txt @@ -10,12 +10,12 @@ #add_test(test_bitset COMMAND test-bitset${EXEEXT}) -add_executable(TestInstantiator test-bitset.c) -target_link_libraries(TestInstantiator +add_executable(bitset_test test-bitset.c) +target_link_libraries(bitset_test pins-lib ltsmin-lib hre-io lts-io hre) -add_test(NAME TestInstantiator - COMMAND TestInstantiator) +add_test(NAME bitset_test + COMMAND bitset_test) From 87a7e47a7d26d78d3db41e8d35280c237f121482 Mon Sep 17 00:00:00 2001 From: Codermann63 <96649204+Codermann63@users.noreply.github.com> Date: Mon, 15 Jan 2024 15:20:59 +0100 Subject: [PATCH 33/40] implemented tests in cmake --- Conversion-to-cmake.txt | 4 ++ src/bignum/CMakeLists.txt | 3 + src/dm/CMakeLists.txt | 2 + src/tests/CMakeLists.txt | 128 ++++++++++++++++++++++++++++++++++++ src/vset-lib/CMakeLists.txt | 3 +- 5 files changed, 139 insertions(+), 1 deletion(-) diff --git a/Conversion-to-cmake.txt b/Conversion-to-cmake.txt index b39a2418..be8e6de1 100644 --- a/Conversion-to-cmake.txt +++ b/Conversion-to-cmake.txt @@ -1,3 +1,7 @@ +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 diff --git a/src/bignum/CMakeLists.txt b/src/bignum/CMakeLists.txt index e52cfbd4..1664f787 100644 --- a/src/bignum/CMakeLists.txt +++ b/src/bignum/CMakeLists.txt @@ -29,8 +29,11 @@ else() PRIVATE bignum-ll.c ) + target_link_libraries(bignum + general-lib) # maybe this link needs to be outside the if statement endif() + target_include_directories(bignum PUBLIC ${CMAKE_CURRENT_SOURCE_DIR} ${CMAKE_CURRENT_SOURCE_DIR}/.. ${CMAKE_CURRENT_BINARY_DIR}/..) diff --git a/src/dm/CMakeLists.txt b/src/dm/CMakeLists.txt index 0ab067d9..53b8dafd 100644 --- a/src/dm/CMakeLists.txt +++ b/src/dm/CMakeLists.txt @@ -13,6 +13,8 @@ target_sources(dm ${DM_HDRS} ) +target_link_libraries(dm general-lib) + OPTION(HAVE_BOOST off) OPTION(HAVE_VIENNACL off) if (HAVE_BOOST) diff --git a/src/tests/CMakeLists.txt b/src/tests/CMakeLists.txt index 262e805c..56324bfb 100644 --- a/src/tests/CMakeLists.txt +++ b/src/tests/CMakeLists.txt @@ -10,6 +10,7 @@ #add_test(test_bitset COMMAND test-bitset${EXEEXT}) +#test-bitset.c add_executable(bitset_test test-bitset.c) target_link_libraries(bitset_test pins-lib @@ -19,3 +20,130 @@ target_link_libraries(bitset_test hre) add_test(NAME bitset_test COMMAND bitset_test) + + +#test-dbs.c +add_executable(dbs_test test-dbs.c) +target_link_libraries(dbs_test + pins-lib + ltsmin-lib + hre-io + lts-io + hre + mc-lib + dm) +add_test(NAME dbs_test + COMMAND dbs_test) + +#test-dfs-stack.c +add_executable(dfs-stack_test test-dfs-stack.c) +target_link_libraries(dfs-stack_test + pins-lib + ltsmin-lib + hre-io + lts-io + hre + mc-lib + dm) +add_test(NAME dfs-stack_test + COMMAND dfs-stack_test) + +#test-dm.c +add_executable(dm_test test-dm.c) +target_link_libraries(dm_test + pins-lib + ltsmin-lib + hre-io + lts-io + hre + mc-lib + dm) +add_test(NAME dm_test + COMMAND dm_test) + +#test-hre.c +add_executable(hre_test test-hre.c) +target_link_libraries(hre_test + pins-lib + ltsmin-lib + hre-io + lts-io + hre + mc-lib + dm) +add_test(NAME hre_test + COMMAND hre_test) + +#test-is-balloc.c +add_executable(is-balloc_test test-is-balloc.c) +target_link_libraries(is-balloc_test + pins-lib + ltsmin-lib + hre-io + lts-io + hre + mc-lib + dm) +add_test(NAME is-balloc_test + COMMAND is-balloc_test) + +# test-ltsmin-parse.c +# Disabled because it requires a flag (comment from original automake code) + +#test-mucalc-parser.c +add_executable(mucalc-parser_test test-mucalc-parser.c) +target_link_libraries(mucalc-parser_test + pins-lib + ltsmin-lib + hre-io + lts-io + hre + mc-lib + dm) +add_test(NAME mucalc-parser_test + COMMAND mucalc-parser_test) + +#test-regroup.c +# Disabled because it requires a read from stdin (comment from original automake code) + +#test-simplemap.c +add_executable(simplemap_test test-simplemap.c) +target_link_libraries(simplemap_test + pins-lib + ltsmin-lib + hre-io + lts-io + hre + mc-lib + dm) +add_test(NAME simplemap_test + COMMAND simplemap_test) + +#test-treedbs.c +add_executable(treedbs_test test-treedbs.c) +target_link_libraries(treedbs_test + pins-lib + ltsmin-lib + hre-io + lts-io + hre + mc-lib + dm) +add_test(NAME treedbs_test + COMMAND treedbs_test) + +#test-vset.c +add_executable(vset_test test-vset.c) +target_link_libraries(vset_test + pins-lib + ltsmin-lib + hre-io + lts-io + hre + mc-lib + dm + vset-lib) +add_test(NAME vset_test + COMMAND vset_test) + + diff --git a/src/vset-lib/CMakeLists.txt b/src/vset-lib/CMakeLists.txt index fda0c144..ce91545c 100644 --- a/src/vset-lib/CMakeLists.txt +++ b/src/vset-lib/CMakeLists.txt @@ -56,7 +56,8 @@ endif() target_link_libraries(vset-lib PUBLIC util-lib - hre-io) + hre-io + bignum) target_include_directories(vset-lib PUBLIC ${CMAKE_CURRENT_SOURCE_DIR} ${CMAKE_CURRENT_SOURCE_DIR}/.. From 678515443d406b2582e42be92c06ed66354e6c36 Mon Sep 17 00:00:00 2001 From: Codermann63 <96649204+Codermann63@users.noreply.github.com> Date: Mon, 15 Jan 2024 15:30:47 +0100 Subject: [PATCH 34/40] removed unnecassary cmake_minimum_required --- src/CMakeLists.txt | 4 +--- src/andl-lib/CMakeLists.txt | 5 ----- src/bignum/CMakeLists.txt | 3 --- src/hre-io/CMakeLists.txt | 3 --- src/hre/CMakeLists.txt | 3 --- src/ltsmin-lib/CMakeLists.txt | 5 ----- src/mc-lib/CMakeLists.txt | 7 ------- src/pins-lib/CMakeLists.txt | 3 --- src/pins-lib/por/CMakeLists.txt | 3 --- src/spg-lib/CMakeLists.txt | 2 -- src/tests/CMakeLists.txt | 12 ------------ 11 files changed, 1 insertion(+), 49 deletions(-) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 0dc93d4a..12e92e07 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -24,9 +24,7 @@ # # -cmake_minimum_required(VERSION 3.21) - -Option(HAVE_CE OFF) +Option(HAVE_CE OFF) # TODO change when actual variability management has been made if (HAVE_CE) add_subdirectory(ce) endif() diff --git a/src/andl-lib/CMakeLists.txt b/src/andl-lib/CMakeLists.txt index 95123d0b..d37e6fa1 100644 --- a/src/andl-lib/CMakeLists.txt +++ b/src/andl-lib/CMakeLists.txt @@ -1,9 +1,4 @@ - - -#BISON_TARGET(MyParser parser.y ${CMAKE_CURRENT_BINARY_DIR}/parser.cpp -# DEFINES_FILE ${CMAKE_CURRENT_BINARY_DIR}/parser.h) - FIND_PACKAGE(FLEX REQUIRED) FLEX_TARGET(ANDLLEXER andl-lexer.l ${CMAKE_CURRENT_BINARY_DIR}/andl-lexer.c diff --git a/src/bignum/CMakeLists.txt b/src/bignum/CMakeLists.txt index 1664f787..731367ff 100644 --- a/src/bignum/CMakeLists.txt +++ b/src/bignum/CMakeLists.txt @@ -1,6 +1,3 @@ - -cmake_minimum_required(VERSION 3.21) - add_library(bignum STATIC) set(HAVE_GMP_H on) diff --git a/src/hre-io/CMakeLists.txt b/src/hre-io/CMakeLists.txt index 4e50b6e7..d06ce6e1 100644 --- a/src/hre-io/CMakeLists.txt +++ b/src/hre-io/CMakeLists.txt @@ -1,6 +1,3 @@ - -cmake_minimum_required(VERSION 3.10) - add_library(hre-io STATIC) target_sources(hre-io diff --git a/src/hre/CMakeLists.txt b/src/hre/CMakeLists.txt index 9432ddb0..509da2fd 100644 --- a/src/hre/CMakeLists.txt +++ b/src/hre/CMakeLists.txt @@ -1,6 +1,3 @@ - -cmake_minimum_required(VERSION 3.10) - add_library(hre STATIC) set(HRE_HDRS diff --git a/src/ltsmin-lib/CMakeLists.txt b/src/ltsmin-lib/CMakeLists.txt index 8101da12..2c73e56f 100644 --- a/src/ltsmin-lib/CMakeLists.txt +++ b/src/ltsmin-lib/CMakeLists.txt @@ -14,11 +14,6 @@ foreach(LEMONFILE ${LEMONFILES}) endforeach() #Generate files with flex - #OLD AUTOMAKE CODE FOR generating with lex: - #%.c %.h: %.l - # $(am__skiplex) $(LEX) $< -#TODO it looks like it is optional in the old automake code. Look into this - set(FLEXFILES ltsmin-lexer mucalc-lexer) FIND_PACKAGE(FLEX REQUIRED) foreach(FLEXFILE ${FLEXFILES}) diff --git a/src/mc-lib/CMakeLists.txt b/src/mc-lib/CMakeLists.txt index afda44e8..bf692f17 100644 --- a/src/mc-lib/CMakeLists.txt +++ b/src/mc-lib/CMakeLists.txt @@ -1,6 +1,3 @@ - -cmake_minimum_required(VERSION 3.21) - add_library(mc-lib STATIC) set(MCLIB_HDRS @@ -46,7 +43,3 @@ target_include_directories(mc-lib PUBLIC ${CMAKE_CURRENT_SOURCE_DIR} ${CMAKE_CURRENT_SOURCE_DIR}/.. ${CMAKE_CURRENT_BINARY_DIR}/..) -#add_dependencies(pins-lib -# ltsmin-lib -# hre) - diff --git a/src/pins-lib/CMakeLists.txt b/src/pins-lib/CMakeLists.txt index 7bfcafad..3d5c2f6c 100644 --- a/src/pins-lib/CMakeLists.txt +++ b/src/pins-lib/CMakeLists.txt @@ -1,6 +1,3 @@ - -cmake_minimum_required(VERSION 3.21) - add_library(pins-lib STATIC) set(PINSLIB_HDRS diff --git a/src/pins-lib/por/CMakeLists.txt b/src/pins-lib/por/CMakeLists.txt index 47f9b682..0e55d1e3 100644 --- a/src/pins-lib/por/CMakeLists.txt +++ b/src/pins-lib/por/CMakeLists.txt @@ -1,6 +1,3 @@ - -cmake_minimum_required(VERSION 3.21) - add_library(por-lib STATIC) set(PORLIB_HDRS diff --git a/src/spg-lib/CMakeLists.txt b/src/spg-lib/CMakeLists.txt index d22084d7..e813d7cd 100644 --- a/src/spg-lib/CMakeLists.txt +++ b/src/spg-lib/CMakeLists.txt @@ -1,5 +1,3 @@ -cmake_minimum_required(VERSION 3.21) - add_library(spg-lib STATIC) set(SPGLIB_HDRS diff --git a/src/tests/CMakeLists.txt b/src/tests/CMakeLists.txt index 56324bfb..d5fe7269 100644 --- a/src/tests/CMakeLists.txt +++ b/src/tests/CMakeLists.txt @@ -1,15 +1,3 @@ - - -#add_test(NAME TestName COMMAND ExecutableToRun arg1 arg2 ...) - - -#add_executable(TestInstantiator TestInstantiator.cxx) -#target_link_libraries(TestInstantiator vtkCommon) -#add_test(NAME TestInstantiator -# COMMAND TestInstantiator) - -#add_test(test_bitset COMMAND test-bitset${EXEEXT}) - #test-bitset.c add_executable(bitset_test test-bitset.c) target_link_libraries(bitset_test From 33df8a67168377516f189d2a58cf4f7116fcb2c5 Mon Sep 17 00:00:00 2001 From: Codermann63 <96649204+Codermann63@users.noreply.github.com> Date: Tue, 16 Jan 2024 15:33:42 +0100 Subject: [PATCH 35/40] minor changes --- CMakeLists.txt | 23 +++++++++ Conversion-to-cmake.txt | 2 +- README.md | 112 ---------------------------------------- src/hre/config.h.in | 2 +- 4 files changed, 25 insertions(+), 114 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 2b38c472..9825ec73 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -51,5 +51,28 @@ add_subdirectory(ltl2ba) configure_file(${PROJECT_SOURCE_DIR}/config.h.in ${PROJECT_SOURCE_DIR}/ltl2ba/config.h) +###### OPTIONS ###### + +#check OS https://gitlab.kitware.com/cmake/community/-/wikis/doc/tutorials/How-To-Write-Platform-Checks + if (WIN32) + message("WIN32") + endif (WIN32) + + if (UNIX) + message("UNIX") + set(__linux__ ON) + endif (UNIX) + + if (MSVC) + message("MSVC") + endif (MSVC) + +if(qwer) + message("qwer is defined") +else() + message("qwer is not defined") +endif() + + #TODO add options for examples, tests and documentation diff --git a/Conversion-to-cmake.txt b/Conversion-to-cmake.txt index be8e6de1..5cd60b0d 100644 --- a/Conversion-to-cmake.txt +++ b/Conversion-to-cmake.txt @@ -8,7 +8,7 @@ GENERAL NOTES: - Files that might be needed from root/lib: verify.h 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. ----------------root----------------- diff --git a/README.md b/README.md index f78fe2f2..cf2522c1 100644 --- a/README.md +++ b/README.md @@ -1,115 +1,3 @@ -conversion status: - -x = not done - -- = in progress - -βœ“ = done (or does not need conversion) - -? = not sure it needs conversion - ------------------------------------------------------- - -x ROOT configure.ac & makefile.am - -? Ltsmin/Autotools - -? Ltsmin/Contrib - -x Ltsmin/Doc - -x Ltsmin/Examples - -- Ltsmin/Lemon - -? Ltsmin/lib [Looks autogenerated] - -βœ“ Ltsmin/Ltl2ba [OK – from ltl2ba github] - -? Ltsmin/M4 - -? Ltsmin/Scoop [Github submodule] - -? Spins [Java project] - -x Ltsmin/Src - -x Ltsmin/Src/andl-lib - -x Ltsmin/Src/bignum - -x Ltsmin/Src/ce - -x Ltsmin/Src/dm - -x Ltsmin/Src/etf-convert - -x Ltsmin/Src/gcf-tool - -x Ltsmin/Src/hre - -x Ltsmin/Src/hre-io - -x Ltsmin/Src/hre-mpi - -x Ltsmin/Src/ldd2bdd - -x Ltsmin/Src/lts-io - -x Ltsmin/Src/lts-lib - -x Ltsmin/Src/ltsmin-compare - -x Ltsmin/Src/ltsmin-convert - -x Ltsmin/Src/ltsmin-lib - -x Ltsmin/Src/ltsmin-printtrace - -x Ltsmin/Src/ltsmin-reduce - -x Ltsmin/Src/ltsmin-reduce-dist - -x Ltsmin/Src/mc-lib - -x Ltsmin/Src/pins2lts-dist - -x Ltsmin/Src/pins2lts-mc - -x Ltsmin/Src/pins2lts-seq - -x Ltsmin/Src/pins2lts-sym - -x Ltsmin/Src/pins-lib - -x Ltsmin/Src/pins-open - -x Ltsmin/Src/pinssim - -x Ltsmin/Src/prob-lib - -x Ltsmin/Src/scripts - -x Ltsmin/Src/spg - -x Ltsmin/Src/spg-lib - -x Ltsmin/Src/tests - -x Ltsmin/Src/torx - -x Ltsmin/Src/util-lib - -x Ltsmin/Src/vset-lib - -x Testsuite - -? Travis - -? www - ------------------------------------------------------- - LTSmin [![Build Status](https://travis-ci.org/utwente-fmt/ltsmin.svg?branch=master)](https://travis-ci.org/utwente-fmt/ltsmin) [![FMT](http://fmt.cs.utwente.nl/images/fmt-logo.png)](http://fmt.cs.utwente.nl/) [![UT](https://www.symbitron.eu/wp-content/uploads/2013/10/UT_Logo_2400_Black_EN1-300x58.png)](https://www.utwente.nl/) === diff --git a/src/hre/config.h.in b/src/hre/config.h.in index 09b1e7e9..6221f23c 100644 --- a/src/hre/config.h.in +++ b/src/hre/config.h.in @@ -16,7 +16,7 @@ /* Hard coded that we are on linux*/ /* Other variables are __APPLE__ _WIN32*/ -#define __linux__ 1 +#cmakedefine __linux__ /* Enable GNU extensions on systems that have them. */ /* FAKE IT CODE */ From c2def83f2729983d5f9bb0556aa27153db41947e Mon Sep 17 00:00:00 2001 From: Codermann63 <96649204+Codermann63@users.noreply.github.com> Date: Wed, 17 Jan 2024 12:21:06 +0100 Subject: [PATCH 36/40] minor variability development --- CMakeLists.txt | 61 +++++++++++++++++++++++++++-------------- Conversion-to-cmake.txt | 3 ++ src/hre/config.h.in | 9 +++--- 3 files changed, 48 insertions(+), 25 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 9825ec73..405a551e 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -11,12 +11,10 @@ project(ltsmin Set(CMAKE_CXX_STANDARD 11) Set(CMAKE_CXX_STANDARD_REQUIRED True) - +set(PACKAGE_STRING "${CMAKE_PROJECT_NAME} ${CMAKE_PROJECT_VERSION}") +set(PACKAGE_BUGREPORT "ltsmin-support@lists.utwente.nl") include(CTest) -# Add CMake modules path | TODO don't think this is necessary -list(APPEND CMAKE_MODULE_PATH "${CMAKE_CURRENT_LIST_DIR}/cmake/") - # update submodules: find_package(Git QUIET) if(GIT_FOUND AND EXISTS "${PROJECT_SOURCE_DIR}/.git") @@ -51,28 +49,49 @@ add_subdirectory(ltl2ba) configure_file(${PROJECT_SOURCE_DIR}/config.h.in ${PROJECT_SOURCE_DIR}/ltl2ba/config.h) -###### OPTIONS ###### +###### CONFIGURATION ###### #check OS https://gitlab.kitware.com/cmake/community/-/wikis/doc/tutorials/How-To-Write-Platform-Checks if (WIN32) - message("WIN32") - endif (WIN32) - - if (UNIX) - message("UNIX") + set(_WIN32) + elseif (UNIX) set(__linux__ ON) - endif (UNIX) - - if (MSVC) - message("MSVC") - endif (MSVC) - -if(qwer) - message("qwer is defined") -else() - message("qwer is not defined") -endif() + elseif (${CMAKE_SYSTEM_NAME} MATCHES "Darwin") + set(_APPLE_ ON) + else () + message(FATAL_ERROR "OS not accounted for in this program") + endif() +option(with_bignum off) + +####### cmake configuration output ###### +#This will output which modules are active when executing the cmake command +message("cmake configuration:") +message("====================") +#ASCIIDOC +message(BIGNUM = ${with_bignum}) +#BUDDY +#CADP +#CC +#CXX +#LIBDDD +#MCRL +#MCRL2 +#MPICC +#MPICXX +#OPAAL +#PBES +#SCOOP +#SPINS +#SPOT +#XMLTO +#BOOST +#VIENNACL +#PNML +#PROB +#SDD +#SYLVAN +message("====================") #TODO add options for examples, tests and documentation diff --git a/Conversion-to-cmake.txt b/Conversion-to-cmake.txt index 5cd60b0d..ebce7a77 100644 --- a/Conversion-to-cmake.txt +++ b/Conversion-to-cmake.txt @@ -6,6 +6,9 @@ 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. diff --git a/src/hre/config.h.in b/src/hre/config.h.in index 6221f23c..fa2e56e5 100644 --- a/src/hre/config.h.in +++ b/src/hre/config.h.in @@ -3,10 +3,10 @@ #define LTSMIN_PATHNAME_MAX 1024 /* Define to the address where bug reports for this package should be sent. */ -#define PACKAGE_BUGREPORT "ltsmin-support@lists.utwente.nl" +#cmakedefine PACKAGE_BUGREPORT "@PACKAGE_BUGREPORT@" /* Define to the full name and version of this package. */ -#define PACKAGE_STRING "ltsmin 3.1.0" +#cmakedefine PACKAGE_STRING "@PACKAGE_STRING@" /* Log2 size of the machine's cache line */ #define CACHE_LINE 6 @@ -14,9 +14,10 @@ /* Size of the machine's cache line */ #define CACHE_LINE_SIZE 64 -/* Hard coded that we are on linux*/ -/* Other variables are __APPLE__ _WIN32*/ +/* Variables for OS*/ #cmakedefine __linux__ +#cmakedefine __APPLE__ +#cmakedefine _WIN32 /* Enable GNU extensions on systems that have them. */ /* FAKE IT CODE */ From 022d51e74f993c3c948651914e2033e9da3ce731 Mon Sep 17 00:00:00 2001 From: Codermann63 <96649204+Codermann63@users.noreply.github.com> Date: Wed, 17 Jan 2024 12:29:19 +0100 Subject: [PATCH 37/40] changed name of install script --- install.sh => install_on_ubuntu.sh | 0 1 file changed, 0 insertions(+), 0 deletions(-) rename install.sh => install_on_ubuntu.sh (100%) diff --git a/install.sh b/install_on_ubuntu.sh similarity index 100% rename from install.sh rename to install_on_ubuntu.sh From 4eb8a74b19c1f5b02740899ed2d087ea57b8483c Mon Sep 17 00:00:00 2001 From: Codermann63 <96649204+Codermann63@users.noreply.github.com> Date: Wed, 17 Jan 2024 13:35:57 +0100 Subject: [PATCH 38/40] added install targets --- CMakeLists.txt | 6 +++--- src/pins2lts-sym/CMakeLists.txt | 26 ++++++++++++++------------ 2 files changed, 17 insertions(+), 15 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 405a551e..8e6ec5ea 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -38,15 +38,13 @@ if(NOT EXISTS "${PROJECT_SOURCE_DIR}/ltl2ba/CMakeLists.txt" OR endif() -#Dependencies #TODO get sylvan(?) via FetchContent? or make it a submodule - add_subdirectory(src) add_subdirectory(lib) add_subdirectory(lemon) add_subdirectory(ltl2ba) -configure_file(${PROJECT_SOURCE_DIR}/config.h.in ${PROJECT_SOURCE_DIR}/ltl2ba/config.h) + ###### CONFIGURATION ###### @@ -64,6 +62,8 @@ configure_file(${PROJECT_SOURCE_DIR}/config.h.in ${PROJECT_SOURCE_DIR}/ltl2ba/co option(with_bignum off) +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:") diff --git a/src/pins2lts-sym/CMakeLists.txt b/src/pins2lts-sym/CMakeLists.txt index 5ec0c2ba..eb37c57b 100644 --- a/src/pins2lts-sym/CMakeLists.txt +++ b/src/pins2lts-sym/CMakeLists.txt @@ -52,26 +52,28 @@ target_include_directories(pins2lts-sym PUBLIC ${CMAKE_CURRENT_SOURCE_DIR} target_compile_options(pins2lts-sym PRIVATE -DPINS_DLL -I${CMAKE_SOURCE_DIR}/lib -I${CMAKE_BINARY_DIR}/lib #include of lib might not be necessary -) + ) +install(TARGETS pins2lts-sym) + ################### EXECUTABLES: eft2lts-sym#################### -add_executable(eft2lts-sym +add_executable(etf2lts-sym auxiliary/options.c ../pins-lib/modules/etf-pins.c ../pins-lib/modules/etf-pins.h ) -target_link_libraries(eft2lts-sym PRIVATE +target_link_libraries(etf2lts-sym PRIVATE libpins2lts-sym hre general-lib ) -target_include_directories(eft2lts-sym PUBLIC ${CMAKE_CURRENT_SOURCE_DIR} +target_include_directories(etf2lts-sym PUBLIC ${CMAKE_CURRENT_SOURCE_DIR} ${CMAKE_CURRENT_SOURCE_DIR}/.. ${CMAKE_CURRENT_BINARY_DIR}/.. ${CMAKE_SOURCE_DIR}/src ${CMAKE_CURRENT_SOURCE_DIR}/auxiliary ${CMAKE_CURRENT_SOURCE_DIR}/alg) -target_compile_options(eft2lts-sym - PRIVATE -DETF -I${CMAKE_SOURCE_DIR}/lib -I${CMAKE_BINARY_DIR}/lib -) +target_compile_options(etf2lts-sym + PRIVATE -DETF -I${CMAKE_SOURCE_DIR}/lib -I${CMAKE_BINARY_DIR}/lib) +install(TARGETS etf2lts-sym) ################### OPTIONAL EXECUTABLES: pnml2lts-sym#################### @@ -97,8 +99,8 @@ if (HAVE_PNML) ${CMAKE_CURRENT_SOURCE_DIR}/alg) target_compile_options(pnml2lts-sym PRIVATE -DPNML -I${CMAKE_SOURCE_DIR}/lib -I${CMAKE_BINARY_DIR}/lib #include of lib might not be necessary -) - + ) + install(TARGETS pnml2lts-sym) endif() @@ -123,11 +125,11 @@ if (HAVE_DVE) ${CMAKE_CURRENT_SOURCE_DIR}/alg) target_compile_options(dve2lts-sym PRIVATE -DDIVINE -I${CMAKE_SOURCE_DIR}/lib -I${CMAKE_BINARY_DIR}/lib #include of lib might not be necessary -) - + ) + install(TARGETS dve2lts-sym) endif() -#################Optional NOT included yet################ +#################Optional executables NOT included yet################ #libstep: lpo2lts-sym #libmcrl2: lps2lts-sym #scoop: mapa2lts-sym From 6c7223307a11a14775822f45504e7e0951957628 Mon Sep 17 00:00:00 2001 From: Codermann63 <96649204+Codermann63@users.noreply.github.com> Date: Fri, 19 Jan 2024 10:09:40 +0100 Subject: [PATCH 39/40] added some variablility management and fixed some old syntax errors --- CMakeLists.txt | 94 ++++++++++++++++++++++++--------- Conversion-to-cmake.txt | 2 + src/CMakeLists.txt | 4 +- src/bignum/CMakeLists.txt | 8 +-- src/ce/CMakeLists.txt | 27 ---------- src/dm/CMakeLists.txt | 4 +- src/ltsmin-lib/CMakeLists.txt | 2 +- src/pins2lts-sym/CMakeLists.txt | 4 +- src/vset-lib/CMakeLists.txt | 15 ++---- 9 files changed, 88 insertions(+), 72 deletions(-) delete mode 100644 src/ce/CMakeLists.txt diff --git a/CMakeLists.txt b/CMakeLists.txt index 8e6ec5ea..1ffcaa43 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -14,6 +14,7 @@ Set(CMAKE_CXX_STANDARD_REQUIRED True) set(PACKAGE_STRING "${CMAKE_PROJECT_NAME} ${CMAKE_PROJECT_VERSION}") set(PACKAGE_BUGREPORT "ltsmin-support@lists.utwente.nl") include(CTest) +set(CMAKE_MODULE_PATH cmake_modules/) # update submodules: find_package(Git QUIET) @@ -60,7 +61,7 @@ add_subdirectory(ltl2ba) message(FATAL_ERROR "OS not accounted for in this program") endif() -option(with_bignum off) + configure_file(${PROJECT_SOURCE_DIR}/config.h.in ${PROJECT_SOURCE_DIR}/ltl2ba/config.h) @@ -68,29 +69,74 @@ configure_file(${PROJECT_SOURCE_DIR}/config.h.in ${PROJECT_SOURCE_DIR}/ltl2ba/co #This will output which modules are active when executing the cmake command message("cmake configuration:") message("====================") -#ASCIIDOC -message(BIGNUM = ${with_bignum}) -#BUDDY -#CADP -#CC -#CXX -#LIBDDD -#MCRL -#MCRL2 -#MPICC -#MPICXX -#OPAAL -#PBES -#SCOOP -#SPINS -#SPOT -#XMLTO -#BOOST -#VIENNACL -#PNML -#PROB -#SDD -#SYLVAN +###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) + endif() + + if(${SYLVAN_FOUND}) + set(have_sylvan ON) + message("SYLVAN = ON. (override with -Dwithout-sylvan)") + else() + message("SYLVAN = OFF. SYLVAN not found, or disabled") + endif() message("====================") diff --git a/Conversion-to-cmake.txt b/Conversion-to-cmake.txt index ebce7a77..2fa680e4 100644 --- a/Conversion-to-cmake.txt +++ b/Conversion-to-cmake.txt @@ -12,6 +12,8 @@ GENERAL NOTES: 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----------------- diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 12e92e07..4c0f942d 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -24,8 +24,8 @@ # # -Option(HAVE_CE OFF) # TODO change when actual variability management has been made -if (HAVE_CE) +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) diff --git a/src/bignum/CMakeLists.txt b/src/bignum/CMakeLists.txt index 731367ff..76f88c9d 100644 --- a/src/bignum/CMakeLists.txt +++ b/src/bignum/CMakeLists.txt @@ -6,16 +6,16 @@ target_sources(bignum PRIVATE bignum.h ) -option(HAVE_LIBGMP off) -if(HAVE_LIBGMP) +option(have_libgmp "does the project have libgmp?" off) #TODO implement actually checking for libgmp +if(${HAVE_LIBGMP}) target_sources(bignum PRIVATE bignum-gmp.c #add lib -lgmp ) -option(HAVE_LIBTOMMATH off) -elseif(HAVE_LIBTOMMATH) +option(HAVE_LIBTOMMATH "does the project have tommath?" off)#TODO implement actually checking for tommath +elseif(${HAVE_LIBTOMMATH}) target_sources(bignum PRIVATE bignum-tommath.c diff --git a/src/ce/CMakeLists.txt b/src/ce/CMakeLists.txt deleted file mode 100644 index 8478bd53..00000000 --- a/src/ce/CMakeLists.txt +++ /dev/null @@ -1,27 +0,0 @@ -#TODO. this is not finished -add_library(ce STATIC) - -set(CE_HDRS - bufs.h - #Ddlts.h #can't find mpi.h - #Dtaudlts.h #can't find mpi.h - #groups.h #can't find mpi.h (Linked with Dtaudlts) - paint.h - sortcount.h) - -target_sources(ce - PRIVATE - #bufs.c #can't find mpi.h - #Ddlts.c #can't find mpi.h - #ce-mpi.c #can't find mpi.h - #Dtaudlts.c #can't find mpi.h - #roups.c #can't find mpi.h (Linked with Dtaudlts) - #paint.c ##can't find mpi.h (Linked with Dtaudlts) - sortcount.c - ${CE_HDRS} -) - -target_include_directories(ce PUBLIC ${CMAKE_CURRENT_SOURCE_DIR} - "${CMAKE_CURRENT_SOURCE_DIR}/..") - - diff --git a/src/dm/CMakeLists.txt b/src/dm/CMakeLists.txt index 53b8dafd..abf4ed2e 100644 --- a/src/dm/CMakeLists.txt +++ b/src/dm/CMakeLists.txt @@ -15,8 +15,8 @@ target_sources(dm target_link_libraries(dm general-lib) -OPTION(HAVE_BOOST off) -OPTION(HAVE_VIENNACL off) +OPTION(have_boost "does the project have boost?" off)#TODO: check for boost +OPTION(have_viennacl "does the project have viennaCL?" off) #TODO check for viennacl if (HAVE_BOOST) target_sources(dm PRIVATE dm_boost.cpp dm_boost.h) diff --git a/src/ltsmin-lib/CMakeLists.txt b/src/ltsmin-lib/CMakeLists.txt index 2c73e56f..a50dcc4c 100644 --- a/src/ltsmin-lib/CMakeLists.txt +++ b/src/ltsmin-lib/CMakeLists.txt @@ -64,7 +64,7 @@ target_sources(ltsmin-lib ${FLEXOUTPUTLIST} ) -if(HAVE_SPOT) +if(${have_spot}) target_sources(ltsmin-lib PRIVATE ltl2spot.cpp) diff --git a/src/pins2lts-sym/CMakeLists.txt b/src/pins2lts-sym/CMakeLists.txt index eb37c57b..9c47a3a6 100644 --- a/src/pins2lts-sym/CMakeLists.txt +++ b/src/pins2lts-sym/CMakeLists.txt @@ -78,7 +78,7 @@ install(TARGETS etf2lts-sym) ################### OPTIONAL EXECUTABLES: pnml2lts-sym#################### set(HAVE_PNML ON) #TODO remove this when pnml check is implemented -if (HAVE_PNML) +if (${HAVE_PNML}) add_executable(pnml2lts-sym auxiliary/options.c ../pins-lib/modules/pnml-pins.c ../pins-lib/modules/pnml-pins.h @@ -106,7 +106,7 @@ endif() ################### OPTIONAL EXECUTABLES: dve2lts-sym#################### set(HAVE_DVE ON) #TODO remove this when pnml check is implemented -if (HAVE_DVE) +if (${HAVE_DVE}) add_executable(dve2lts-sym auxiliary/options.c ../pins-lib/modules/dve-pins.c ../pins-lib/modules/dve-pins.h diff --git a/src/vset-lib/CMakeLists.txt b/src/vset-lib/CMakeLists.txt index ce91545c..bfca3c45 100644 --- a/src/vset-lib/CMakeLists.txt +++ b/src/vset-lib/CMakeLists.txt @@ -16,32 +16,27 @@ target_sources(vset-lib PRIVATE ${VSET_HDRS} ) -OPTION(HAVE_BUDDY off) -OPTION(HAVE_SYLVAN off) -OPTION(HAVE_LIBMCRL off) -OPTION(HAVE_SDD off) -OPTION(HAVE_LIBDDD off) -if(HAVE_SDD) +if(${have_buddy}) target_sources(vset-lib PRIVATE vset_buddy.c) endif() -if(HAVE_SDD) +if(${have_sylvan}) target_sources(vset-lib PRIVATE vset_sylvan.c vset_lddmc.c) endif() -if(HAVE_SDD) +if(${have_libmcrl}) target_sources(vset-lib PRIVATE vset_atermdd.c) endif() -if(HAVE_SDD) +if(${have_sdd}) target_sources(vset-lib PRIVATE sdd_utils.c sdd_utils.h vset_sdd.c vset_sdd.h @@ -49,7 +44,7 @@ if(HAVE_SDD) vtree_utils.c vtree_utils.h) endif() -if(HAVE_LIBDDD) +if(${have_libddd}) target_sources(vset-lib PRIVATE vset_ddd.cpp) endif() From a9c4192dc5176d46304e602d92d5bd433fee1293 Mon Sep 17 00:00:00 2001 From: codermann63 Date: Tue, 23 Jan 2024 11:40:02 +0100 Subject: [PATCH 40/40] have sylvan --- CMakeLists.txt | 22 ++++++++++++++-------- src/hre/config.h.in | 2 ++ src/pins2lts-sym/CMakeLists.txt | 6 ++++++ src/tests/CMakeLists.txt | 2 -- src/vset-lib/CMakeLists.txt | 5 ++++- 5 files changed, 26 insertions(+), 11 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 1ffcaa43..6fe10d32 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -39,11 +39,6 @@ if(NOT EXISTS "${PROJECT_SOURCE_DIR}/ltl2ba/CMakeLists.txt" OR endif() -#TODO get sylvan(?) via FetchContent? or make it a submodule -add_subdirectory(src) -add_subdirectory(lib) -add_subdirectory(lemon) -add_subdirectory(ltl2ba) @@ -52,7 +47,7 @@ add_subdirectory(ltl2ba) #check OS https://gitlab.kitware.com/cmake/community/-/wikis/doc/tutorials/How-To-Write-Platform-Checks if (WIN32) - set(_WIN32) + set(_WIN32 ON) elseif (UNIX) set(__linux__ ON) elseif (${CMAKE_SYSTEM_NAME} MATCHES "Darwin") @@ -129,11 +124,12 @@ message("====================") else() find_package(LACE) find_package(SYLVAN) + #set( ON) endif() if(${SYLVAN_FOUND}) - set(have_sylvan ON) - message("SYLVAN = ON. (override with -Dwithout-sylvan)") + set(HAVE_SYLVAN ON) + message("SYLVAN = ON. (override with -Dwithout-sylvan=1)") else() message("SYLVAN = OFF. SYLVAN not found, or disabled") endif() @@ -141,3 +137,13 @@ 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) + + diff --git a/src/hre/config.h.in b/src/hre/config.h.in index fa2e56e5..cdb94fef 100644 --- a/src/hre/config.h.in +++ b/src/hre/config.h.in @@ -32,6 +32,8 @@ /* Define to 1 if you have the `_aligned_malloc' function. */ #cmakedefine HAVE__ALIGNED_MALLOC +#cmakedefine HAVE_SYLVAN + /* Provide a hint to the optimizer */ #define __assume(cond) do { if (!(cond)) __builtin_unreachable(); } while (0) diff --git a/src/pins2lts-sym/CMakeLists.txt b/src/pins2lts-sym/CMakeLists.txt index 9c47a3a6..3be41ade 100644 --- a/src/pins2lts-sym/CMakeLists.txt +++ b/src/pins2lts-sym/CMakeLists.txt @@ -26,6 +26,12 @@ target_link_libraries(libpins2lts-sym PUBLIC spg-lib ) +if (${HAVE_SYLVAN}) + target_link_libraries(libpins2lts-sym PUBLIC + sylvan + lace) +endif() + target_include_directories(libpins2lts-sym PUBLIC ${CMAKE_CURRENT_SOURCE_DIR} ${CMAKE_CURRENT_SOURCE_DIR}/.. ${CMAKE_CURRENT_BINARY_DIR}/.. diff --git a/src/tests/CMakeLists.txt b/src/tests/CMakeLists.txt index d5fe7269..c15fc67f 100644 --- a/src/tests/CMakeLists.txt +++ b/src/tests/CMakeLists.txt @@ -133,5 +133,3 @@ target_link_libraries(vset_test vset-lib) add_test(NAME vset_test COMMAND vset_test) - - diff --git a/src/vset-lib/CMakeLists.txt b/src/vset-lib/CMakeLists.txt index bfca3c45..1f17bdfb 100644 --- a/src/vset-lib/CMakeLists.txt +++ b/src/vset-lib/CMakeLists.txt @@ -23,10 +23,13 @@ if(${have_buddy}) endif() -if(${have_sylvan}) +if(${HAVE_SYLVAN}) target_sources(vset-lib PRIVATE vset_sylvan.c vset_lddmc.c) + target_link_libraries(vset-lib PUBLIC + sylvan + lace) endif()