Closed MicroEnder closed 1 year ago
fredher
commented
1 year ago Dear MicroEnder, I apologize, the tutorial has not been updated since release v0.4. It is now up-to-date w.r.t v0.5 (and latest commits). Please, let us know if it still does not work for you. Also, we will be very interested to know what you plan to use TChecker for, as it is very motivating for us to keep in touch with our users. Best regards, Frédéric
MicroEnder
commented
1 year ago Dear Frédéric, Thanks alot for your reply! I am a student studying formal verification and I would like to perform some verification on timed automata. TChecker is the only fully open-source software I have found so far, and I want to implement and practice my algorithm on TChecker. I'll try the new tutorial you provided and will reach out to you if I have any questions. Thank you once again for your assistance.
Many Thanks, MicroEnder
Hello! While following the tutorial on Implementing a reachability algorithm using TChecker libraries, I encountered an error during the "make" step following cmake, as shown below:
`root@LAPTOP-6C8O0TJG:/usr/local/reachability-tutorial-v0.4/build# make Scanning dependencies of target reach-4 [ 8%] Building CXX object CMakeFiles/reach-4.dir/reach-4.cc.o /usr/local/reachability-tutorial-v0.4/src/reach-4.cc: In constructor ‘graph_t::graph_t(const std::shared_ptr&, std::size_t, std::size_t)’:
/usr/local/reachability-tutorial-v0.4/src/reach-4.cc:72:11: error: no matching function for call to ‘tchecker::graph::reachability::graph_t<node_t, edge_t, node_hash_t, node_equal_to_t>::graph_t(std::size_t&, std::size_t&)’
72 | _zg(zg)
| ^
In file included from /usr/local/reachability-tutorial-v0.4/src/reach-4.cc:18:
/usr/local/include/tchecker/graph/reachability_graph.hh:217:3: note: candidate: ‘tchecker::graph::reachability::graph_t<NODE, EDGE, NODE_HASH, NODE_EQUAL>::graph_t(std::size_t, std::size_t, const NODE_HASH&, const NODE_EQUAL&) [with NODE = node_t; EDGE = edge_t; NODE_HASH = node_hash_t; NODE_EQUAL = node_equal_to_t; std::size_t = long unsigned int]’
217 | graph_t(std::size_t block_size, std::size_t table_size, NODE_HASH const & node_hash, NODE_EQUAL const & node_equal_to)
| ^&, tchecker::zg::semantics_type_t, tchecker::zg::extrapolation_type_t, std::size_t&)’
186 | std::shared_ptr zg{tchecker::zg::factory(system, tchecker::zg::ELAPSED_SEMANTICS, tchecker::zg::EXTRA_LU_PLUS_LOCAL, block_size)};
| tchecker::zg::factory(const std::shared_ptr&, semantics_type_t, extrapolation_type_t, std::size_t, std::size_t)’
554 | tchecker::zg::zg_t factory(std::shared_ptr const & system,
| ^ tchecker::zg::factory(const std::shared_ptr&, semantics_type_t, extrapolation_type_t, const tchecker::clockbounds::clockbounds_t&, std::size_t, std::size_t)’
571 | tchecker::zg::zg_t * factory(std::shared_ptr const & system,
| ^::shared_ptr()’
186 | ::factory(system, tchecker::zg::ELAPSED_SEMANTICS, tchecker::zg::EXTRA_LU_PLUS_LOCAL, block_size)};
| ^
~~ /usr/local/include/tchecker/graph/reachability_graph.hh:217:3: note: candidate expects 4 arguments, 2 provided /usr/local/reachability-tutorial-v0.4/src/reach-4.cc: In function ‘int main(int, char*)’: /usr/local/reachability-tutorial-v0.4/src/reach-4.cc:186:65: error: no matching function for call to ‘factory(std::shared_ptr~~~~~^~~~~~~~~~~~~~~~~~~~ In file included from /usr/local/reachability-tutorial-v0.4/src/reach-4.cc:25: /usr/local/include/tchecker/zg/zg.hh:554:22: note: candidate: ‘tchecker::zg::zg_t~~ /usr/local/include/tchecker/zg/zg.hh:554:22: note: candidate expects 5 arguments, 4 provided /usr/local/include/tchecker/zg/zg.hh:571:22: note: candidate: ‘tchecker::zg::zg_t~~ /usr/local/include/tchecker/zg/zg.hh:571:22: note: candidate expects 6 arguments, 4 provided /usr/local/reachability-tutorial-v0.4/src/reach-4.cc:186:153: error: no matching function for call to ‘std::shared_ptrIn file included from /usr/local/gcc-13.1.0/include/c++/13.1.0/memory:80, from /usr/local/reachability-tutorial-v0.4/src/reach-4.cc:10: /usr/local/gcc-13.1.0/include/c++/13.1.0/bits/shared_ptr.h:463:9: note: candidate: ‘template<class _Alloc, class ... _Args> std::shared_ptr<_Tp>::shared_ptr(std::_Sp_alloc_shared_tag<_Tp>, _Args&& ...) [with _Args = _Alloc; _Tp = tchecker::zg::zg_t]’ 463 | shared_ptr(_Sp_alloc_shared_tag<_Alloc> tag, _Args&&... __args) | ^ = _Del; _Tp = tchecker::zg::zg_t]’
395 | shared_ptr(unique_ptr<_Yp, _Del>&& r)
| ^ = _Yp; _Tp = tchecker::zg::zg_t]’
380 | explicit shared_ptr(const weak_ptr<_Yp>& r)
| ^ = _Yp; _Tp = tchecker::zg::zg_t]’
368 | shared_ptr(shared_ptr<_Yp>&& r) noexcept
| ^ = _Yp; _Tp = tchecker::zg::zg_t]’
351 | shared_ptr(const shared_ptr<_Yp>& r) noexcept
| ^ std::shared_ptr<_Tp>::shared_ptr(const std::shared_ptr<_Yp>&, element_type) [with _Tp = tchecker::zg::zg_t]’
311 | shared_ptr(const shared_ptr<_Yp>& __r, element_type p) noexcept
| ^ = _Alloc; _Tp = tchecker::zg::zg_t]’
268 | shared_ptr(_Yp p, _Deleter d, _Alloc a)
| ^ std::shared_ptr<_Tp>::shared_ptr(std::nullptr_t, _Deleter) [with _Tp = tchecker::zg::zg_t]’
248 | shared_ptr(nullptr_t p, _Deleter d)
| ^ = _Deleter; _Tp = tchecker::zg::zg_t]’
231 | shared_ptr(_Yp p, _Deleter d)
| ^ = _Yp; _Tp = tchecker::zg::zg_t]’
214 | shared_ptr(_Yp p) : shared_ptr<_Tp>(p) { }
| ^
~~~~~ /usr/local/gcc-13.1.0/include/c++/13.1.0/bits/shared_ptr.h:463:9: note: template argument deduction/substitution failed: /usr/local/gcc-13.1.0/include/c++/13.1.0/bits/shared_ptr.h:395:9: note: candidate: ‘template<class _Yp, class _Del, class> std::shared_ptr<_Tp>::shared_ptr(std::unique_ptr<_Up, _Ep>&&) [with _Del = _Yp;~~~~~ /usr/local/gcc-13.1.0/include/c++/13.1.0/bits/shared_ptr.h:395:9: note: template argument deduction/substitution failed: /usr/local/gcc-13.1.0/include/c++/13.1.0/bits/shared_ptr.h:387:9: note: candidate: ‘template<class _Yp, class> std::shared_ptr<_Tp>::shared_ptr(std::auto_ptr<_Up>&&) [with _Yp = _Tp1; _Tp = tchecker::zg::zg_t]’ 387 | shared_ptr(auto_ptr<_Yp>&& r); | ^~~~~~ /usr/local/gcc-13.1.0/include/c++/13.1.0/bits/shared_ptr.h:387:9: note: template argument deduction/substitution failed: /usr/local/gcc-13.1.0/include/c++/13.1.0/bits/shared_ptr.h:380:18: note: candidate: ‘template<class _Yp, class> std::shared_ptr<_Tp>::shared_ptr(const std::weak_ptr<_Yp>&) [with~~~~~ /usr/local/gcc-13.1.0/include/c++/13.1.0/bits/shared_ptr.h:380:18: note: template argument deduction/substitution failed: /usr/local/gcc-13.1.0/include/c++/13.1.0/bits/shared_ptr.h:368:9: note: candidate: ‘template<class _Yp, class> std::shared_ptr<_Tp>::shared_ptr(std::shared_ptr<_Yp>&&) [with~~~~~ /usr/local/gcc-13.1.0/include/c++/13.1.0/bits/shared_ptr.h:368:9: note: template argument deduction/substitution failed: /usr/local/gcc-13.1.0/include/c++/13.1.0/bits/shared_ptr.h:351:9: note: candidate: ‘template<class _Yp, class> std::shared_ptr<_Tp>::shared_ptr(const std::shared_ptr<_Yp>&) [with~~~~~ /usr/local/gcc-13.1.0/include/c++/13.1.0/bits/shared_ptr.h:351:9: note: template argument deduction/substitution failed: /usr/local/gcc-13.1.0/include/c++/13.1.0/bits/shared_ptr.h:311:9: note: candidate: ‘template~~~~~ /usr/local/gcc-13.1.0/include/c++/13.1.0/bits/shared_ptr.h:311:9: note: template argument deduction/substitution failed: /usr/local/gcc-13.1.0/include/c++/13.1.0/bits/shared_ptr.h:287:9: note: candidate: ‘template<class _Deleter, class _Alloc> std::shared_ptr<_Tp>::shared_ptr(std::nullptr_t, _Deleter, _Alloc) [with _Alloc = _Deleter; _Tp = tchecker::zg::zg_t]’ 287 | shared_ptr(nullptr_t p, _Deleter d, _Alloc a) | ^~~~~~ /usr/local/gcc-13.1.0/include/c++/13.1.0/bits/shared_ptr.h:287:9: note: template argument deduction/substitution failed: /usr/local/gcc-13.1.0/include/c++/13.1.0/bits/shared_ptr.h:268:9: note: candidate: ‘template<class _Yp, class _Deleter, class _Alloc, class> std::shared_ptr<_Tp>::shared_ptr(_Yp, _Deleter, _Alloc) [with _Deleter = _Yp; _Alloc = _Deleter;~~~~~ /usr/local/gcc-13.1.0/include/c++/13.1.0/bits/shared_ptr.h:268:9: note: template argument deduction/substitution failed: /usr/local/gcc-13.1.0/include/c++/13.1.0/bits/shared_ptr.h:248:9: note: candidate: ‘template~~~~~ /usr/local/gcc-13.1.0/include/c++/13.1.0/bits/shared_ptr.h:248:9: note: template argument deduction/substitution failed: /usr/local/gcc-13.1.0/include/c++/13.1.0/bits/shared_ptr.h:231:9: note: candidate: ‘template<class _Yp, class _Deleter, class> std::shared_ptr<_Tp>::shared_ptr(_Yp, _Deleter) [with _Deleter = _Yp;~~~~~ /usr/local/gcc-13.1.0/include/c++/13.1.0/bits/shared_ptr.h:231:9: note: template argument deduction/substitution failed: /usr/local/gcc-13.1.0/include/c++/13.1.0/bits/shared_ptr.h:214:9: note: candidate: ‘template<class _Yp, class> std::shared_ptr<_Tp>::shared_ptr(_Yp) [with~~~~~ /usr/local/gcc-13.1.0/include/c++/13.1.0/bits/shared_ptr.h:214:9: note: template argument deduction/substitution failed: /usr/local/gcc-13.1.0/include/c++/13.1.0/bits/shared_ptr.h:535:7: note: candidate: ‘std::shared_ptr<_Tp>::shared_ptr(const std::weak_ptr<_Tp>&, std::nothrow_t) [with _Tp = tchecker::zg::zg_t]’ 535 | shared_ptr(const weak_ptr<_Tp>& r, std::nothrow_t) noexcept | ^~~~~~ /usr/local/gcc-13.1.0/include/c++/13.1.0/bits/shared_ptr.h:535:7: note: candidate expects 2 arguments, 1 provided /usr/local/gcc-13.1.0/include/c++/13.1.0/bits/shared_ptr.h:412:17: note: candidate: ‘constexpr std::shared_ptr<_Tp>::shared_ptr(std::nullptr_t) [with _Tp = tchecker::zg::zg_t; std::nullptr_t = std::nullptr_t]’ 412 | constexpr shared_ptr(nullptr_t) noexcept : shared_ptr() { } | ^~~~~~ /usr/local/gcc-13.1.0/include/c++/13.1.0/bits/shared_ptr.h:412:17: note: conversion of argument 1 would be ill-formed: /usr/local/gcc-13.1.0/include/c++/13.1.0/bits/shared_ptr.h:359:7: note: candidate: ‘std::shared_ptr<_Tp>::shared_ptr(std::shared_ptr<_Tp>&&) [with _Tp = tchecker::zg::zg_t]’ 359 | shared_ptr(shared_ptr&& __r) noexcept | ^~~~~~ /usr/local/gcc-13.1.0/include/c++/13.1.0/bits/shared_ptr.h:359:7: note: conversion of argument 1 would be ill-formed: /usr/local/gcc-13.1.0/include/c++/13.1.0/bits/shared_ptr.h:204:7: note: candidate: ‘std::shared_ptr<_Tp>::shared_ptr(const std::shared_ptr<_Tp>&) [with _Tp = tchecker::zg::zg_t]’ 204 | shared_ptr(const shared_ptr&) noexcept = default; ///< Copy constructor | ^~~~~~ /usr/local/gcc-13.1.0/include/c++/13.1.0/bits/shared_ptr.h:204:7: note: conversion of argument 1 would be ill-formed: /usr/local/gcc-13.1.0/include/c++/13.1.0/bits/shared_ptr.h:202:17: note: candidate: ‘constexpr std::shared_ptr<_Tp>::shared_ptr() [with _Tp = tchecker::zg::zg_t]’ 202 | constexpr shared_ptr() noexcept : shared_ptr<_Tp>() { } | ^~~~~~ /usr/local/gcc-13.1.0/include/c++/13.1.0/bits/shared_ptr.h:202:17: note: candidate expects 0 arguments, 1 provided make[2]: [CMakeFiles/reach-4.dir/build.make:63: CMakeFiles/reach-4.dir/reach-4.cc.o] Error 1 make[1]: [CMakeFiles/Makefile2:86: CMakeFiles/reach-4.dir/all] Error 2 make: *** [Makefile:84: all] Error 2 `I would like to know how to solve this problem. Here are the versions of the packages I am using: `root@LAPTOP-6C8O0TJG:/usr/local# g++ --version g++ (GCC) 13.1.0 Copyright (C) 2023 Free Software Foundation, Inc. This is free software; see the source for copying conditions. There is NO warranty; not even for MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
root@LAPTOP-6C8O0TJG:/usr/local# cmake --version cmake version 3.16.3
CMake suite maintained and supported by Kitware (kitware.com/cmake). root@LAPTOP-6C8O0TJG:/usr/local# flex --version flex 2.6.4 root@LAPTOP-6C8O0TJG:/usr/local# bison --version bison (GNU Bison) 3.5.1 Written by Robert Corbett and Richard Stallman.
Copyright (C) 2020 Free Software Foundation, Inc. This is free software; see the source for copying conditions. There is NO warranty; not even for MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. root@LAPTOP-6C8O0TJG:/usr/local# dpkg -s 'libboost-dev' | grep ^Version Version: 1.71.0.0ubuntu2 root@LAPTOP-6C8O0TJG:/usr/local# doxygen --version 1.8.17 root@LAPTOP-6C8O0TJG:/usr/local# dpkg -s 'libc-dev-bin' | grep ^Version Version: 2.31-0ubuntu9.9`
Catch2 was compiled from their GitHub repo with the same CXXFLAGS exported variable.
I don't know what to do now,cou you please help me? Many thanks!