ticktac-project / tchecker Goto Github PK

View Code? Open in Web Editor NEW

20.0 11.0 16.0 25.05 MB

TChecker is an open-source verification tool for timed automata

Home Page: https://github.com/ticktac-project/tchecker/wiki

License: MIT License

CMake 2.06% C++ 95.97% LLVM 0.40% Yacc 1.00% Shell 0.52% Dockerfile 0.05%

model-checking timed-automata

tchecker's People

Contributors

Stargazers

Watchers

Forkers

sparsa zuxichen schlepil mukherjee-sayan fredher arnabsur adrienpmlt nagsides philippschlehubercaissier echtzeitsysteme moeinij pictavien areynoua

tchecker's Issues

Segmentation fault

Hey, I've been following this guide to implement a reachability algorithm on Ubuntu 21.10. More specifically, in the 'Before we start' section, after cmake has succeeded, when I run the make command from the build directory, I get this error:

[  8%] Linking CXX executable reach-4
during IPA pass: icf
lto1: internal compiler error: Errore di segmentazione
0x9db587 crash_signal
  ../../src/gcc/toplev.c:327
0x7f755c10c51f ???
  ./signal/../sysdeps/unix/sysv/linux/x86_64/libc_sigaction.c:0
0x1297c16 varpool_node::get_constructor()
  ../../src/gcc/varpool.c:300
0x1297c16 varpool_node::get_constructor()
  ../../src/gcc/varpool.c:279
0x694f55 ipa_icf::sem_variable::equals(ipa_icf::sem_item*, hash_map<symtab_node*, ipa_icf::sem_item*, simple_hashmap_traits<default_hash_traits<symtab_node*>, ipa_icf::sem_item*> >&)
  ../../src/gcc/ipa-icf.c:1697
0xe9c4ca ipa_icf::sem_item_optimizer::subdivide_classes_by_equality(bool)
  ../../src/gcc/ipa-icf.c:2732
0x12a95bb ipa_icf::sem_item_optimizer::execute()
  ../../src/gcc/ipa-icf.c:2464
0x12a937b ipa_icf_driver
  ../../src/gcc/ipa-icf.c:3600
0x12a937b ipa_icf::pass_ipa_icf::execute(function*)
  ../../src/gcc/ipa-icf.c:3647
Please submit a full bug report,
with preprocessed source if appropriate.
Please include the complete backtrace with any bug report.
See file:///usr/share/doc/gcc-11/README.Bugs for instructions.
lto-wrapper: fatal error: /usr/bin/c++ returned 1 exit status
compilation terminated.
/usr/bin/ld: error: lto-wrapper failed
collect2: error: ld returned 1 exit status
make[2]: *** [CMakeFiles/reach-4.dir/build.make:104: reach-4] Errore 1
make[1]: *** [CMakeFiles/Makefile2:105: CMakeFiles/reach-4.dir/all] Errore 2
make: *** [Makefile:103: all] Errore 2

Does anybody else get a segmentation fault when compiling the code?

copy assignment of outgoing iterators implicitely deleted

If you change the outgoing loop of function reachable() in reach-6.cc from

    auto outgoing_range = builder.outgoing(node);
    for (auto it = outgoing_range.begin(); ! it.at_end(); ++it) {

    auto outgoing_range = builder.outgoing(node);
    auto it = outgoing_range.begin();
    for (it = outgoing_range.begin(); ! it.at_end(); ++it) {

you get a huge error message saying that
tchecker::ts::builder_ok_t<TS, ALLOCATOR>::iterator_t<TS_ITERATOR>::operator=(const tchecker::ts::builder_ok_t<TS, ALLOCATOR>::iterator_t<TS_ITERATOR>&) is implicitly deleted because the default definition would be ill-formed.

Clang additionally notes that copy assignment operator [...] is implicitly deleted because field '_it' has a deleted copy assignment operator.

I find strange that the copy construction would work, but not the copy assignment.

In my actual case those iterators is wrapped into a class that implement the successor iteration using Spot's interface, but that interface is "restartable": you may iterate over the successors more than once. So I store two TChecker iterators: the current position, and a copy of begin(), so that I can assign it to the position (using the above method) to start another loop on request.

Error reported by sanitizers

Since I want to extend TChecker, I tried to compile with -fsanitize=undefined,address,leak. The compilation works, but at runtime I get some errors like "member access within misaligned address", "constructor call on misaligned address". Is there really a problem here? Did I miss something? Do you know which sanitizers you can enable, or other useful warnings you can use? Many thanks.

typo in tchecker/clockbounds/model.hh

tchecker/clockbounds/model.hh:57:15: error: ‘class tchecker::clockbounds::model_t<tchecker::ta::system_t, tchecker::zg::details::variables_t>’ has no member named ‘_loval_m_map’; did you mean ‘_local_m_map’?
   57 |         model._loval_m_map = nullptr;

Same issue on line 116.

Improve covreach graph construction

Current construction expands nodes by first adding all its child nodes and corresponding edges, and second removing those which are covered. This is done to ensure that edges are built correctly, in particular when a node is covered by one of its successors.

After a discussion with Philipp Schlehuber, it seems that we can cover nodes before we add them to the graph. We shall only take care of the situation where a node n is covered by one of its successors n1. Then, for all the following successors n2 we shall avoid adding the edge n->n2. This can be detected since n is inactive once it has been removed.

Allow some guards on weak event transitions

Currently, no guard is allowed on a transitions labeled by an event that is weakly synchronized. However, guards allowing only bounded integer variables are needed for the translation from UPPAAL models.

The destruct_all() method of the covreach graph may lead to segfault

Since edges are stored in nodes (lists of incoming/outgoing edges), when tchecker::covreach::graph_t::destruct_all() performs _edge_allocator.destruct_all(); it leads to a situation where edges have been destructed, but the list of outgoing/incoming edges of the nodes may still point to memory locations where those edges were stored. As a result, the call to _ts_allocator.destruct_all(); may result in a segmentation fault.

In details tchecker::graph::directed::details::edge_list_t owns a shared pointer to an edge. Each node derives from two edge lists. So when a node is destroyed, the two edge lists delete their head pointers to edges. But these edges have already been destructed in the scenario above.

The clear() method in the directed graph tchecker::graph::directed::graph_t::clear() is misleading as it does not clear anything.

The strategy to free memory for tchecker::covreach::graph_t::destruct_all() should be to iterate over all nodes, and remove all edges from the nodes, before the nodes and edges are destructed.

The memory management strategy for the directed graph should be reconsidered to prevent such bugs.

lexer outputs unknown characters

It seems the lexer is still printing (on stdout) characters it does not understand.

% echo '||||hello;;;;bar!!!!' | ./tchecker explore - 
||||1.1-9: ERROR, syntax error, unexpected identifier, expecting "\n" or system
;;;;!!!!ERROR, nullptr system declaration

2 error(s)

I (re)discovered that the hard way by calling parse_system_declaration(argv[0], log) instead
of parse_system_declaration(argv[1], log)...

Crash on model with clock to clock update

On the following model

system:bug

clock:1:x
clock:1:y

event:tau

process:P
location:P:l0{initial:}
location:P:l1{}
location:P:l2{}
edge:P:l1:l2:tau{do : x = y}

tck-reach crashes (e.g. tck-reach -a reach model.txt) with:

tck-reach: /home/osankur/tools/tchecker/src/clockbounds/solver.cc:168: void tchecker::clockbounds::df_solver_t::add_assignment(tchecker::loc_id_t, tchecker::loc_id_t, tchecker::clock_id_t, tchecker::clock_id_t, tchecker::integer_t): Assertion `x < _clock_number' failed.
Aborted (core dumped)

Fix display of covreach graph

Current graph display traverses the graph using a DFS. However, the graph may not be connected. Hence, display would be incomplete. We should instead traverse the list of nodes, display each node, and all its outgoing edges

Uncatched exception

At the end of the main() function in TChecker, there is a

throw nullptr system declaration

that does not inherit from std::exception, and is thus not catched.

Example raising the issue:

% src/tchecker covreach < /dev/null
1.1: ERROR, syntax error, unexpected end of file, expecting "\n" or system
terminate called after throwing an instance of 'char const*'
zsh: abort      src/tchecker covreach < /dev/null

(thanks Alexandre for signaling the problem)

Duplicate custom targets not supported by cmake's Xcode generator

Hi,

I get the following error message when configuring the build:

CMake Error: This project has enabled the ALLOW_DUPLICATE_CUSTOM_TARGETS global property.  The "Xcode" generator does not support duplicate custom targets.  Consider using a Makefiles generator or fix the project to not use duplicate target names.
CMake Generate step failed.  Build files cannot be regenerated correctly.

Configuration: Mac OS X 10.14.6 and cmake 3.15.3.

Test errors after building

Hey,

I'm trying to build your tool. While building, I get the error:

CMake Error at /usr/local/lib/cmake/Catch2/CatchAddTests.cmake:42 (message):
  Error running test executable
  '/home/hans.vanderlaan/Documents/PolicyVerification/TChecker/build/test/unit-tests/unittest':


    Result: 56
    Output: All available test cases:
    construction of upper bounds
        [db]
    hash values of upper bounds
        [db]
    comparators <,<=,>=,>
        [db]
    sum
        [db]
    add
        [db]
    min et max
        [db]
    is_universal, structural tests
        [dbm]
    is_positive, structural test
        [dbm]
    is_universal_positive, structural test
        [dbm]
    is_empty_0, structural tests
        [dbm]
    is_tight, structural tests
        [dbm]
    universal makes universal zones
        [dbm]
    universal_positive makes universal-positive zones
        [dbm]
    tighten (full)
        [dbm]
    tighten w.r.t. a difference bound
        [dbm]
    constrain
        [dbm]
    DBM equality
        [dbm]
    DBM inclusion
        [dbm]
    reset DBM
        [dbm]
    DBM open_up (delay)
        [dbm]
    DBM intersection
        [dbm]
    Checking tightness when the 0-row is modified
        [dbm]
    Extrapolations from STTT06
        [dbm]
    Extrapolations boundary case on M/U bounds
        [dbm]
    Zone inclusion w.r.t. abstraction aM (1)
        [dbm]
    Zone inclusion w.r.t. abstraction aM (2)
        [dbm]
    Zone inclusion w.r.t. abstraction aLU from LICS12
        [dbm]
    expression with no array variables
        [extract_variables]
    expression with array variables
        [extract_variables]
    statements with no array variable
        [extract_variables]
    statements with array variables
        [extract_variables]
    no throw if no weakly synchronized events
        [guard_weak_sync]
    no throw if weakly synchronized events have no guard
        [guard_weak_sync]
    throw if first weakly synchronized event has a guard
        [guard_weak_sync]
    throw if last weakly synchronized event has a guard
        [guard_weak_sync]
    throw if middle weakly synchronized event has a guard
        [guard_weak_sync]
    throw if some weakly synchronized event has a guard, several transitions
        [guard_weak_sync]
    Offset clock variables from empty access map
        [offset clock variables]
    Offset clock variables from system - no array
        [offset clock variables]
    Offset clock variables from system - array
        [offset clock variables]
    translation clocks <-> offset variables
        [offset_dbm]
    is_positive, structural test for offset DBMs
        [offset_dbm]
    is_universal_positive, structural test for offset DBMs
        [offset_dbm]
    is_synchronized, structural test for offset DBMs
        [offset_dbm]
    universal_positive offset DBMs
        [offset_dbm]
    synchronize offset DBMs
        [offset_dbm]
    reset to reference clocks on offset DBMs
        [offset_dbm]
    asynchronous_open_up on offset DBMs
        [offset_dbm]
    to_dbm on offset DBMs
        [offset_dbm]
    lexical ordering on ranges
        [ordering]
    Empty access map
        [access map]
    Non empty access map
        [access map]
    variable access map computation - empty system
        [access map]
    variable access map computation - 1 process
        [access map]
    variable access map computation - 2 processes, no shared variable
        [access map]
    variable access map computation - 3 processes, array, shared variables
        [access map]

  56 test cases

  

  



make[2]: *** [test/unit-tests/CMakeFiles/unittest.dir/build.make:88: test/unit-tests/unittest] Error 1
make[2]: *** Deleting file 'test/unit-tests/unittest'
make[1]: *** [CMakeFiles/Makefile2:888: test/unit-tests/CMakeFiles/unittest.dir/all] Error 2
make: *** [Makefile:141: all] Error 2

I'm not sure what is happening. How should I read this output? What went wrong?

Kind regards,

Hans

system_t::location(process_name, location_name) is protected

I'm currently working on mapping atomic propositions such as "Bus.Collision" that appear into LTL formulas, to tchecker's location identifiers.

system_t::location("Bus", "Collision")->id() seems to be what I need, unfortunately this method is protected. Is it on purpose or could it be made public?

As far as I can see, another option would be to iterate over the result of system_t::locations() until I find the good pair, but that looks clumsy.

Single free list

Consider using a single free list for all pool allocated objects. This would remove the need of a GC thread. When an object is not used any more, it adds itself to the free list. When a pool runs out of memory, it can inspect the free list to recover the chunks that it has allocated.

Add deallocation methods to allocators and pools

Add predicates/properties

TChecker currently check if some label is reachable. Properties would extend labels by allowing more general properties like "P1.l1 && 1 <= i <= 5 && x-y <= 6". Needs:

parse properties from string (requires to extend expressions to allow labels as well as locations like P1.l1)
compile the resulting expression into bytecode
evaluate the bytecode on a state (evaluation depends on the state, as for instance in "x[2*i] <= a-b")

The graph computed or output by covreach algorithm is not correct

The covreach algorithm on an asynchronous model of Fischer's protocol (fischer_2.txt
) outputs the following graph:

digraph fischer_async_2_10 {
node [shape="box",style="rounded"];
n1 [label="<A,A,l,l> id1=0,id2=0 (0<=x1 & 0<=x2 & x1=x2)"]
n1 -> n2 [color=black]
n1 -> n3 [color=black]
n2 [label="<A,req,l,l> id1=0,id2=0 (0<=x1 & 0<=x2<=10 & 0<=x1-x2)"]
n2 -> n4 [color=black]
n3 [label="<req,A,l,l> id1=0,id2=0 (0<=x1<=10 & 0<=x2 & x1-x2<=0)"]
n3 -> n4 [color=black]
n4 [label="<req,req,l,l> id1=0,id2=0 (0<=x1<=10 & 0<=x2<=10 & 0<=x1-x2<=10)"]
}

command: tchecker covreach -l foo -m zg:elapsed:NOextra -f dot fischer_2.txt

whereas the explore algorithm outputs:

digraph fischer_async_2_10 {
node [shape="box",style="rounded"];
n0 [label="<A,A,l,l> id1=0,id2=0 (0<=x1 & 0<=x2 & x1=x2)"]
n1 [label="<req,A,l,l> id1=0,id2=0 (0<=x1<=10 & 0<=x2 & x1-x2<=0)"]
n0 -> n1
n2 [label="<A,req,l,l> id1=0,id2=0 (0<=x1 & 0<=x2<=10 & 0<=x1-x2)"]
n0 -> n2
n3 [label="<req,req,l,l> id1=0,id2=0 (0<=x1<=10 & 0<=x2<=10 & 0<=x1-x2<=10)"]
n1 -> n3
n4 [label="<req,req,l,l> id1=0,id2=0 (0<=x1<=10 & 0<=x2<=10 & -10<=x1-x2<=0)"]
n2 -> n4
}

command: tchecker explore -s bfs -m zg:elapsed:NOextra -f dot fischer_2.txt

The nodes n2 and n3 in the output produced by covreach algorithm should not have the same successor n4 as demonstrated by the output produced by explore algorithm. They have two distinct successors, and there is no subsumption between these two nodes (n3 and n4 in the output of algorithm explore).

Error: invalid number of clocks or locations

The following model raises an error:

system:small

process:P1
location:P1:l0{initial:}
location:P1:l1

with the following output:

ERROR, invalid number of clocks or locations (overflow)

1 error(s)

The same model, but without location l1 in process P1 raises no error.

typos in utils/gc.hh's documentation

this file mentions the inexistant function stop_and_join() twice

TChecker allows invalid expressions in guards and invariants

TChecker does not detect that expressions like provided: a or invariant: a are invalid when a is an array (for instance declared as int:3:0:10:0:a). This is because the type of expressions returned by the type checker is not verified when the fsm model is built.

NR tests fail

Due to commit faf06bd that fixes a bug in graph output for algorithm covreach, some NR tests fail (as they were built on the buggy output code).

I don't know how to fix the issue since I have not looked at the NR tests part yet. Gerald, could you please handle this?

Incorrect compilation/interpretation of clock assignment

From Philipp Schlehuber:

Je pense il y a un problème avec le reset des horloge à un valeur donné. En faite je pense l'ordre du valeur et de l'entier et l'id de la horloge "à droite" ont été echangé.

Car dans vm/vm.hh
inline tchecker::integer_t interpret_instruction(...){
...
case VM_CLKRESET:
...
auto const value = top_and_poptchecker::integer_t();
auto const right_id = top_and_poptchecker::clock_id_t();
auto const left_id = top_and_poptchecker::clock_id_t();
...
Donc sur le _stack on veut [..., left_id, right_id, value]

But in vm/compilers.cc

virtual void visit(tchecker::typed_int_to_clock_assign_statement_t const & stmt)
{
if (stmt.type() != tchecker::STMT_TYPE_CLKASSIGN_INT)
throw std::invalid_argument("invalid statement");

	    	tchecker::typed_var_expression_t zero_clock(tchecker::EXPR_TYPE_CLKVAR, tchecker::zero_clock_name, tchecker::zero_clock_id, 1);
	    	compile_clock_reset(stmt.clock(), stmt.value(), zero_clock);

}

and

	void compile_clock_reset(tchecker::typed_lvalue_expression_t const & lvalue,
                           tchecker::typed_expression_t const & int_rvalue,
                           tchecker::typed_lvalue_expression_t const & clock_rvalue)
  {
	    	tchecker::details::lvalue_expression_compiler_t<BYTECODE_BACK_INSERTER> clocks_compiler(_bytecode_back_inserter);
	    	tchecker::details::rvalue_expression_compiler_t<BYTECODE_BACK_INSERTER> int_rvalue_compiler(_bytecode_back_inserter);
    
	    	lvalue.visit(clocks_compiler);
	    	int_rvalue.visit(int_rvalue_compiler);
	    	clock_rvalue.visit(clocks_compiler);
    _bytecode_back_inserter = tchecker::VM_CLKRESET;
  }

Donc on met sur le _stack [..., left_id, value, right_id].

Moi j'ai juste changé l'ordre dans vm/vm.hh et ca marche pour l'example ci-dessous, mais je ne suis pas sure s'il faut changer aussi des autres coins dans le code.

system:ad94_fig10

clock:1:x
clock:1:y

event:a
event:b
event:c
event:d

process:P
location:P:l0{initial:}
location:P:l1{}
location:P:l2{}
location:P:l3{labels: green}
edge:P:l0:l1:a{do:y=10}
edge:P:l1:l2:b{provided: y==1}
edge:P:l1:l3:c{provided: x<1}
edge:P:l2:l3:c{provided: x<1}
edge:P:l3:l1:a{provided: y<1 : do:y=10}
edge:P:l3:l3:d{provided: x>1}

cannot compile current HEAD

Just updated:

% git describe 
v0.2-27-g3645075

Compilation shows multiple occurrences of this warning:

/home/adl/git/tchecker/src/../include/tchecker/variables/variables.hh:599:28: warning: comparison of integer expressions of different signedness: ‘int’ and ‘unsigned int’ [-Wsign-compare]
  599 |         for (auto i = 0; i < size; ++i) {
      |                          ~~^~~~~~

Linking fails with the following errors:

[ 93%] Linking CXX executable tchecker
/usr/bin/ld: liblibtchecker.a(program.lex-fixed.cc.o):(.bss+0x0): multiple definition of `pleng'; liblibtchecker.a(system.lex-fixed.cc.o):(.bss+0x0): first defined here
/usr/bin/ld: liblibtchecker.a(program.lex-fixed.cc.o):(.bss+0x8): multiple definition of `pin'; liblibtchecker.a(system.lex-fixed.cc.o):(.bss+0x8): first defined here
/usr/bin/ld: liblibtchecker.a(program.lex-fixed.cc.o):(.bss+0x10): multiple definition of `pout'; liblibtchecker.a(system.lex-fixed.cc.o):(.bss+0x10): first defined here
/usr/bin/ld: liblibtchecker.a(program.lex-fixed.cc.o):(.data+0x0): multiple definition of `plineno'; liblibtchecker.a(system.lex-fixed.cc.o):(.data+0x0): first defined here
/usr/bin/ld: liblibtchecker.a(program.lex-fixed.cc.o):(.bss+0x18): multiple definition of `p_flex_debug'; liblibtchecker.a(system.lex-fixed.cc.o):(.bss+0x18): first defined here
/usr/bin/ld: liblibtchecker.a(program.lex-fixed.cc.o):(.bss+0x20): multiple definition of `ptext'; liblibtchecker.a(system.lex-fixed.cc.o):(.bss+0x20): first defined here
/usr/bin/ld: liblibtchecker.a(program.lex-fixed.cc.o): in function `p_create_buffer(_IO_FILE*, int)':
/home/adl/git/tchecker/build/src/parsing/program_parser/program.lex.cc:1671: multiple definition of `p_create_buffer(_IO_FILE*, int)'; liblibtchecker.a(system.lex-fixed.cc.o):/home/adl/git/tchecker/build/src/parsing/system_parser/system.lex.cc:1770: first defined here
/usr/bin/ld: liblibtchecker.a(program.lex-fixed.cc.o): in function `prealloc(void*, unsigned long)':
/home/adl/git/tchecker/build/src/parsing/program_parser/program.lex.cc:2140: multiple definition of `prealloc(void*, unsigned long)'; liblibtchecker.a(system.lex-fixed.cc.o):/home/adl/git/tchecker/build/src/parsing/system_parser/system.lex.cc:2239: first defined here
/usr/bin/ld: liblibtchecker.a(program.lex-fixed.cc.o): in function `prestart(_IO_FILE*)':
/home/adl/git/tchecker/build/src/parsing/program_parser/program.lex.cc:1609: multiple definition of `prestart(_IO_FILE*)'; liblibtchecker.a(system.lex-fixed.cc.o):/home/adl/git/tchecker/build/src/parsing/system_parser/system.lex.cc:1708: first defined here
/usr/bin/ld: liblibtchecker.a(program.lex-fixed.cc.o): in function `p_switch_to_buffer(yy_buffer_state*)':
/home/adl/git/tchecker/build/src/parsing/program_parser/program.lex.cc:1626: multiple definition of `p_switch_to_buffer(yy_buffer_state*)'; liblibtchecker.a(system.lex-fixed.cc.o):/home/adl/git/tchecker/build/src/parsing/system_parser/system.lex.cc:1725: first defined here
/usr/bin/ld: liblibtchecker.a(program.lex-fixed.cc.o): in function `palloc(unsigned long)':
/home/adl/git/tchecker/build/src/parsing/program_parser/program.lex.cc:2135: multiple definition of `palloc(unsigned long)'; liblibtchecker.a(system.lex-fixed.cc.o):/home/adl/git/tchecker/build/src/parsing/system_parser/system.lex.cc:2234: first defined here
/usr/bin/ld: liblibtchecker.a(program.lex-fixed.cc.o): in function `p_delete_buffer(yy_buffer_state*)':
/home/adl/git/tchecker/build/src/parsing/program_parser/program.lex.cc:1699: multiple definition of `p_delete_buffer(yy_buffer_state*)'; liblibtchecker.a(system.lex-fixed.cc.o):/home/adl/git/tchecker/build/src/parsing/system_parser/system.lex.cc:1798: first defined here
/usr/bin/ld: liblibtchecker.a(program.lex-fixed.cc.o): in function `pfree(void*)':
/home/adl/git/tchecker/build/src/parsing/program_parser/program.lex.cc:2153: multiple definition of `pfree(void*)'; liblibtchecker.a(system.lex-fixed.cc.o):/home/adl/git/tchecker/build/src/parsing/system_parser/system.lex.cc:2252: first defined here
/usr/bin/ld: liblibtchecker.a(program.lex-fixed.cc.o): in function `p_flush_buffer(yy_buffer_state*)':
/home/adl/git/tchecker/build/src/parsing/program_parser/program.lex.cc:1746: multiple definition of `p_flush_buffer(yy_buffer_state*)'; liblibtchecker.a(system.lex-fixed.cc.o):/home/adl/git/tchecker/build/src/parsing/system_parser/system.lex.cc:1845: first defined here
/usr/bin/ld: liblibtchecker.a(program.lex-fixed.cc.o): in function `ppush_buffer_state(yy_buffer_state*)':
/home/adl/git/tchecker/build/src/parsing/program_parser/program.lex.cc:1775: multiple definition of `ppush_buffer_state(yy_buffer_state*)'; liblibtchecker.a(system.lex-fixed.cc.o):/home/adl/git/tchecker/build/src/parsing/system_parser/system.lex.cc:1874: first defined here
/usr/bin/ld: liblibtchecker.a(program.lex-fixed.cc.o): in function `ppop_buffer_state()':
/home/adl/git/tchecker/build/src/parsing/program_parser/program.lex.cc:1805: multiple definition of `ppop_buffer_state()'; liblibtchecker.a(system.lex-fixed.cc.o):/home/adl/git/tchecker/build/src/parsing/system_parser/system.lex.cc:1904: first defined here
/usr/bin/ld: liblibtchecker.a(program.lex-fixed.cc.o): in function `p_scan_buffer(char*, unsigned long)':
/home/adl/git/tchecker/build/src/parsing/program_parser/program.lex.cc:1873: multiple definition of `p_scan_buffer(char*, unsigned long)'; liblibtchecker.a(system.lex-fixed.cc.o):/home/adl/git/tchecker/build/src/parsing/system_parser/system.lex.cc:1972: first defined here
/usr/bin/ld: liblibtchecker.a(program.lex-fixed.cc.o): in function `p_scan_string(char const*)':
/home/adl/git/tchecker/build/src/parsing/program_parser/program.lex.cc:1910: multiple definition of `p_scan_string(char const*)'; liblibtchecker.a(system.lex-fixed.cc.o):/home/adl/git/tchecker/build/src/parsing/system_parser/system.lex.cc:2009: first defined here
/usr/bin/ld: liblibtchecker.a(program.lex-fixed.cc.o): in function `p_scan_bytes(char const*, int)':
/home/adl/git/tchecker/build/src/parsing/program_parser/program.lex.cc:1923: multiple definition of `p_scan_bytes(char const*, int)'; liblibtchecker.a(system.lex-fixed.cc.o):/home/adl/git/tchecker/build/src/parsing/system_parser/system.lex.cc:2022: first defined here
/usr/bin/ld: liblibtchecker.a(program.lex-fixed.cc.o): in function `pget_lineno()':
/home/adl/git/tchecker/build/src/parsing/program_parser/program.lex.cc:1985: multiple definition of `pget_lineno()'; liblibtchecker.a(system.lex-fixed.cc.o):/home/adl/git/tchecker/build/src/parsing/system_parser/system.lex.cc:2084: first defined here
/usr/bin/ld: liblibtchecker.a(program.lex-fixed.cc.o): in function `pget_in()':
/home/adl/git/tchecker/build/src/parsing/program_parser/program.lex.cc:1994: multiple definition of `pget_in()'; liblibtchecker.a(system.lex-fixed.cc.o):/home/adl/git/tchecker/build/src/parsing/system_parser/system.lex.cc:2093: first defined here
/usr/bin/ld: liblibtchecker.a(program.lex-fixed.cc.o): in function `pget_out()':
/home/adl/git/tchecker/build/src/parsing/program_parser/program.lex.cc:2002: multiple definition of `pget_out()'; liblibtchecker.a(system.lex-fixed.cc.o):/home/adl/git/tchecker/build/src/parsing/system_parser/system.lex.cc:2101: first defined here
/usr/bin/ld: liblibtchecker.a(program.lex-fixed.cc.o): in function `pget_leng()':
/home/adl/git/tchecker/build/src/parsing/program_parser/program.lex.cc:2010: multiple definition of `pget_leng()'; liblibtchecker.a(system.lex-fixed.cc.o):/home/adl/git/tchecker/build/src/parsing/system_parser/system.lex.cc:2109: first defined here
/usr/bin/ld: liblibtchecker.a(program.lex-fixed.cc.o): in function `pget_text()':
/home/adl/git/tchecker/build/src/parsing/program_parser/program.lex.cc:2019: multiple definition of `pget_text()'; liblibtchecker.a(system.lex-fixed.cc.o):/home/adl/git/tchecker/build/src/parsing/system_parser/system.lex.cc:2118: first defined here
/usr/bin/ld: liblibtchecker.a(program.lex-fixed.cc.o): in function `pset_lineno(int)':
/home/adl/git/tchecker/build/src/parsing/program_parser/program.lex.cc:2028: multiple definition of `pset_lineno(int)'; liblibtchecker.a(system.lex-fixed.cc.o):/home/adl/git/tchecker/build/src/parsing/system_parser/system.lex.cc:2127: first defined here
/usr/bin/ld: liblibtchecker.a(program.lex-fixed.cc.o): in function `pset_in(_IO_FILE*)':
/home/adl/git/tchecker/build/src/parsing/program_parser/program.lex.cc:2040: multiple definition of `pset_in(_IO_FILE*)'; liblibtchecker.a(system.lex-fixed.cc.o):/home/adl/git/tchecker/build/src/parsing/system_parser/system.lex.cc:2139: first defined here
/usr/bin/ld: liblibtchecker.a(program.lex-fixed.cc.o): in function `pset_out(_IO_FILE*)':
/home/adl/git/tchecker/build/src/parsing/program_parser/program.lex.cc:2045: multiple definition of `pset_out(_IO_FILE*)'; liblibtchecker.a(system.lex-fixed.cc.o):/home/adl/git/tchecker/build/src/parsing/system_parser/system.lex.cc:2144: first defined here
/usr/bin/ld: liblibtchecker.a(program.lex-fixed.cc.o): in function `pget_debug()':
/home/adl/git/tchecker/build/src/parsing/program_parser/program.lex.cc:2050: multiple definition of `pget_debug()'; liblibtchecker.a(system.lex-fixed.cc.o):/home/adl/git/tchecker/build/src/parsing/system_parser/system.lex.cc:2149: first defined here
/usr/bin/ld: liblibtchecker.a(program.lex-fixed.cc.o): in function `pset_debug(int)':
/home/adl/git/tchecker/build/src/parsing/program_parser/program.lex.cc:2055: multiple definition of `pset_debug(int)'; liblibtchecker.a(system.lex-fixed.cc.o):/home/adl/git/tchecker/build/src/parsing/system_parser/system.lex.cc:2154: first defined here
/usr/bin/ld: liblibtchecker.a(program.lex-fixed.cc.o): in function `plex_destroy()':
/home/adl/git/tchecker/build/src/parsing/program_parser/program.lex.cc:2089: multiple definition of `plex_destroy()'; liblibtchecker.a(system.lex-fixed.cc.o):/home/adl/git/tchecker/build/src/parsing/system_parser/system.lex.cc:2188: first defined here
collect2: error: ld returned 1 exit status

I'm using flex 2.6.4, bison 3.4.1, gcc 9.2.1.

Reverting the last changes to the flex --prefix fixes the link issue.

diff --git a/src/parsing/program_parser/CMakeLists.txt b/src/parsing/program_parser/CMakeLists.txt
index ee9bd71..1ed2c74 100644
--- a/src/parsing/program_parser/CMakeLists.txt
+++ b/src/parsing/program_parser/CMakeLists.txt
@@ -10,7 +10,7 @@ ${CMAKE_CURRENT_BINARY_DIR}/program.tab.cc
 DEFINES_FILE   ${CMAKE_CURRENT_BINARY_DIR}/program.tab.hh
 COMPILE_FLAGS  -v)
 
-FLEX_TARGET(program_lexer program.ll ${CMAKE_CURRENT_BINARY_DIR}/program.lex.cc COMPILE_FLAGS -Pp)
+FLEX_TARGET(program_lexer program.ll ${CMAKE_CURRENT_BINARY_DIR}/program.lex.cc COMPILE_FLAGS -Ppp)
 
 ADD_FLEX_BISON_DEPENDENCY(program_lexer program_parser)
 
diff --git a/src/parsing/system_parser/CMakeLists.txt b/src/parsing/system_parser/CMakeLists.txt
index 81cb858..6cb92cd 100644
--- a/src/parsing/system_parser/CMakeLists.txt
+++ b/src/parsing/system_parser/CMakeLists.txt
@@ -10,7 +10,7 @@ ${CMAKE_CURRENT_BINARY_DIR}/system.tab.cc
 DEFINES_FILE  ${CMAKE_CURRENT_BINARY_DIR}/system.tab.hh
 COMPILE_FLAGS -v)
 
-FLEX_TARGET(system_lexer system.ll ${CMAKE_CURRENT_BINARY_DIR}/system.lex.cc COMPILE_FLAGS -Pp)
+FLEX_TARGET(system_lexer system.ll ${CMAKE_CURRENT_BINARY_DIR}/system.lex.cc COMPILE_FLAGS -Psp)
 
 ADD_FLEX_BISON_DEPENDENCY(system_lexer system_parser)

shared library?

To build Python bindings for adl/tcltl I need to build a shared library that either embed TChecker (for this the code of TChecker needs to be compiled with -fPIC even of it is a static archive) or that link with a shared version of TChecker.

I think the first option can be achieved by passing some magic variable to cmake, but that is not necessary convenient for the users. What do you think about changing TChecker to build and install two flavors of the library: a static version and a shared version?

Extremely slow clock bounds computation

The following model is a straight-line automaton with 100 states and 2 clocks. But the clock bounds computation takes about 40s. This seems to increase quickly with the size of the model.

system:bug
clock:1:x
clock:1:y

event:a
process:P
location:P:l0{initial:}
location:P:l1{}
location:P:l2{}
location:P:l3{}
location:P:l4{}
location:P:l5{}
location:P:l6{}
location:P:l7{}
location:P:l8{}
location:P:l9{}
location:P:l10{}
location:P:l11{}
location:P:l12{}
location:P:l13{}
location:P:l14{}
location:P:l15{}
location:P:l16{}
location:P:l17{}
location:P:l18{}
location:P:l19{}
location:P:l20{}
location:P:l21{}
location:P:l22{}
location:P:l23{}
location:P:l24{}
location:P:l25{}
location:P:l26{}
location:P:l27{}
location:P:l28{}
location:P:l29{}
location:P:l30{}
location:P:l31{}
location:P:l32{}
location:P:l33{}
location:P:l34{}
location:P:l35{}
location:P:l36{}
location:P:l37{}
location:P:l38{}
location:P:l39{}
location:P:l40{}
location:P:l41{}
location:P:l42{}
location:P:l43{}
location:P:l44{}
location:P:l45{}
location:P:l46{}
location:P:l47{}
location:P:l48{}
location:P:l49{}
location:P:l50{}
location:P:l51{}
location:P:l52{}
location:P:l53{}
location:P:l54{}
location:P:l55{}
location:P:l56{}
location:P:l57{}
location:P:l58{}
location:P:l59{}
location:P:l60{}
location:P:l61{}
location:P:l62{}
location:P:l63{}
location:P:l64{}
location:P:l65{}
location:P:l66{}
location:P:l67{}
location:P:l68{}
location:P:l69{}
location:P:l70{}
location:P:l71{}
location:P:l72{}
location:P:l73{}
location:P:l74{}
location:P:l75{}
location:P:l76{}
location:P:l77{}
location:P:l78{}
location:P:l79{}
location:P:l80{}
location:P:l81{}
location:P:l82{}
location:P:l83{}
location:P:l84{}
location:P:l85{}
location:P:l86{}
location:P:l87{}
location:P:l88{}
location:P:l89{}
location:P:l90{}
location:P:l91{}
location:P:l92{}
location:P:l93{}
location:P:l94{}
location:P:l95{}
location:P:l96{}
location:P:l97{}
location:P:l98{}
location:P:l99{}
edge:P:l0:l1:a{provided: y>0 && x <1: do : x=0}
edge:P:l1:l2:a{provided: y>0 && x <1: do : x=0}
edge:P:l2:l3:a{provided: y>0 && x <1: do : x=0}
edge:P:l3:l4:a{provided: y>0 && x <1: do : x=0}
edge:P:l4:l5:a{provided: y>0 && x <1: do : x=0}
edge:P:l5:l6:a{provided: y>0 && x <1: do : x=0}
edge:P:l6:l7:a{provided: y>0 && x <1: do : x=0}
edge:P:l7:l8:a{provided: y>0 && x <1: do : x=0}
edge:P:l8:l9:a{provided: y>0 && x <1: do : x=0}
edge:P:l9:l10:a{provided: y>0 && x <1: do : x=0}
edge:P:l10:l11:a{provided: y>0 && x <1: do : x=0}
edge:P:l11:l12:a{provided: y>0 && x <1: do : x=0}
edge:P:l12:l13:a{provided: y>0 && x <1: do : x=0}
edge:P:l13:l14:a{provided: y>0 && x <1: do : x=0}
edge:P:l14:l15:a{provided: y>0 && x <1: do : x=0}
edge:P:l15:l16:a{provided: y>0 && x <1: do : x=0}
edge:P:l16:l17:a{provided: y>0 && x <1: do : x=0}
edge:P:l17:l18:a{provided: y>0 && x <1: do : x=0}
edge:P:l18:l19:a{provided: y>0 && x <1: do : x=0}
edge:P:l19:l20:a{provided: y>0 && x <1: do : x=0}
edge:P:l20:l21:a{provided: y>0 && x <1: do : x=0}
edge:P:l21:l22:a{provided: y>0 && x <1: do : x=0}
edge:P:l22:l23:a{provided: y>0 && x <1: do : x=0}
edge:P:l23:l24:a{provided: y>0 && x <1: do : x=0}
edge:P:l24:l25:a{provided: y>0 && x <1: do : x=0}
edge:P:l25:l26:a{provided: y>0 && x <1: do : x=0}
edge:P:l26:l27:a{provided: y>0 && x <1: do : x=0}
edge:P:l27:l28:a{provided: y>0 && x <1: do : x=0}
edge:P:l28:l29:a{provided: y>0 && x <1: do : x=0}
edge:P:l29:l30:a{provided: y>0 && x <1: do : x=0}
edge:P:l30:l31:a{provided: y>0 && x <1: do : x=0}
edge:P:l31:l32:a{provided: y>0 && x <1: do : x=0}
edge:P:l32:l33:a{provided: y>0 && x <1: do : x=0}
edge:P:l33:l34:a{provided: y>0 && x <1: do : x=0}
edge:P:l34:l35:a{provided: y>0 && x <1: do : x=0}
edge:P:l35:l36:a{provided: y>0 && x <1: do : x=0}
edge:P:l36:l37:a{provided: y>0 && x <1: do : x=0}
edge:P:l37:l38:a{provided: y>0 && x <1: do : x=0}
edge:P:l38:l39:a{provided: y>0 && x <1: do : x=0}
edge:P:l39:l40:a{provided: y>0 && x <1: do : x=0}
edge:P:l40:l41:a{provided: y>0 && x <1: do : x=0}
edge:P:l41:l42:a{provided: y>0 && x <1: do : x=0}
edge:P:l42:l43:a{provided: y>0 && x <1: do : x=0}
edge:P:l43:l44:a{provided: y>0 && x <1: do : x=0}
edge:P:l44:l45:a{provided: y>0 && x <1: do : x=0}
edge:P:l45:l46:a{provided: y>0 && x <1: do : x=0}
edge:P:l46:l47:a{provided: y>0 && x <1: do : x=0}
edge:P:l47:l48:a{provided: y>0 && x <1: do : x=0}
edge:P:l48:l49:a{provided: y>0 && x <1: do : x=0}
edge:P:l49:l50:a{provided: y>0 && x <1: do : x=0}
edge:P:l50:l51:a{provided: y>0 && x <1: do : x=0}
edge:P:l51:l52:a{provided: y>0 && x <1: do : x=0}
edge:P:l52:l53:a{provided: y>0 && x <1: do : x=0}
edge:P:l53:l54:a{provided: y>0 && x <1: do : x=0}
edge:P:l54:l55:a{provided: y>0 && x <1: do : x=0}
edge:P:l55:l56:a{provided: y>0 && x <1: do : x=0}
edge:P:l56:l57:a{provided: y>0 && x <1: do : x=0}
edge:P:l57:l58:a{provided: y>0 && x <1: do : x=0}
edge:P:l58:l59:a{provided: y>0 && x <1: do : x=0}
edge:P:l59:l60:a{provided: y>0 && x <1: do : x=0}
edge:P:l60:l61:a{provided: y>0 && x <1: do : x=0}
edge:P:l61:l62:a{provided: y>0 && x <1: do : x=0}
edge:P:l62:l63:a{provided: y>0 && x <1: do : x=0}
edge:P:l63:l64:a{provided: y>0 && x <1: do : x=0}
edge:P:l64:l65:a{provided: y>0 && x <1: do : x=0}
edge:P:l65:l66:a{provided: y>0 && x <1: do : x=0}
edge:P:l66:l67:a{provided: y>0 && x <1: do : x=0}
edge:P:l67:l68:a{provided: y>0 && x <1: do : x=0}
edge:P:l68:l69:a{provided: y>0 && x <1: do : x=0}
edge:P:l69:l70:a{provided: y>0 && x <1: do : x=0}
edge:P:l70:l71:a{provided: y>0 && x <1: do : x=0}
edge:P:l71:l72:a{provided: y>0 && x <1: do : x=0}
edge:P:l72:l73:a{provided: y>0 && x <1: do : x=0}
edge:P:l73:l74:a{provided: y>0 && x <1: do : x=0}
edge:P:l74:l75:a{provided: y>0 && x <1: do : x=0}
edge:P:l75:l76:a{provided: y>0 && x <1: do : x=0}
edge:P:l76:l77:a{provided: y>0 && x <1: do : x=0}
edge:P:l77:l78:a{provided: y>0 && x <1: do : x=0}
edge:P:l78:l79:a{provided: y>0 && x <1: do : x=0}
edge:P:l79:l80:a{provided: y>0 && x <1: do : x=0}
edge:P:l80:l81:a{provided: y>0 && x <1: do : x=0}
edge:P:l81:l82:a{provided: y>0 && x <1: do : x=0}
edge:P:l82:l83:a{provided: y>0 && x <1: do : x=0}
edge:P:l83:l84:a{provided: y>0 && x <1: do : x=0}
edge:P:l84:l85:a{provided: y>0 && x <1: do : x=0}
edge:P:l85:l86:a{provided: y>0 && x <1: do : x=0}
edge:P:l86:l87:a{provided: y>0 && x <1: do : x=0}
edge:P:l87:l88:a{provided: y>0 && x <1: do : x=0}
edge:P:l88:l89:a{provided: y>0 && x <1: do : x=0}
edge:P:l89:l90:a{provided: y>0 && x <1: do : x=0}
edge:P:l90:l91:a{provided: y>0 && x <1: do : x=0}
edge:P:l91:l92:a{provided: y>0 && x <1: do : x=0}
edge:P:l92:l93:a{provided: y>0 && x <1: do : x=0}
edge:P:l93:l94:a{provided: y>0 && x <1: do : x=0}
edge:P:l94:l95:a{provided: y>0 && x <1: do : x=0}
edge:P:l95:l96:a{provided: y>0 && x <1: do : x=0}
edge:P:l96:l97:a{provided: y>0 && x <1: do : x=0}
edge:P:l97:l98:a{provided: y>0 && x <1: do : x=0}
edge:P:l98:l99:a{provided: y>0 && x <1: do : x=0}

Problem arising when pool_t::destruct_all() is not called

It looks like the destructor of the zg pool destroys _zone_pool before the ta allocator is destroyed

clang-9 warnings

FYI compiling with clang-9 is quite verbose (too long for the 65536-character limit of GitHub's issues). Fortunately, it seems there are many duplicate messages.

Attached is the result of

% mkdir build
% cd build
% CXX=clang++-9 cmake ..
% make >& log.txt

log.txt

No warning when the initial state set is empty

The tck-reach tool does not display any warning when the set of initial states is empty, e.g. when one forgets the initial: attribute, or writes it with a typo. It would be useful to add a warning.
It would also be useful to have warnings about ignored attributes which can help detect typos.

Out of bound assignment causes segmentation fault

Assigning an out-of-bound value to an integer variable causes segmentation fault.
For instance, for the following input:

system:sys
int:1:0:1:1:v0
event:a
process:P
location:P:l0{initial:}
edge:P:l0:l0:a{do:v0=-1}

Running:
tchecker explore -m zg:elapsed:NOextra a.txt

will crash with a segfault.

Destructor of par_expression_t does not clean recursively

I believe the following destructor should not be default but delete this->_expr:
https://github.com/ticktac-project/tchecker/blob/master/include/tchecker/expression/expression.hh#L308

calling gc.stop() twice causes a segfault

I have some control flow that looks like this:

gc.start()
if (condition)
   {
     // ...
     gc.stop()
    }
// ... code that may need the gc or not, depending on condition
gc.stop()

I though that calling gc.stop() twice would be harmless, but it actually segfault.

==2347== Invalid read of size 8
==2347==    at 0x4CB7D54: std::thread::join() (in /usr/lib/x86_64-linux-gnu/libstdc++.so.6.0.27)
==2347==    by 0x1485B2: tchecker::gc_t::stop() (gc.cc:58)
==2347==    by 0x11E9AB: run() (main.cc:232)
==2347==    by 0x11E03F: main (main.cc:255)
==2347==  Address 0x0 is not stack'd, malloc'd or (recently) free'd
==2347== 
==2347== 
==2347== Process terminating with default action of signal 11 (SIGSEGV)
==2347==  Access not within mapped region at address 0x0
==2347==    at 0x4CB7D54: std::thread::join() (in /usr/lib/x86_64-linux-gnu/libstdc++.so.6.0.27)
==2347==    by 0x1485B2: tchecker::gc_t::stop() (gc.cc:58)
==2347==    by 0x11E9AB: run() (main.cc:232)
==2347==    by 0x11E03F: main (main.cc:255)

It's clearly easy for me to work around, but I think it would be nice if gc could check whether it is actually running before trying to stop. I see that calling start() twice will raise an exception, so maybe another option is to do that for stop() as well.

allow to retrieve the model of a ts_t

After I have done

typedef tchecker::zg::ta::elapsed_extraLUplus_local_t zone_graph_t;
tchecker::zg::ta::model_t model(*sysdecl, log);
zone_graph_t::ts_t ts(model);

I'm currently writing a wrapper so that the ts can be seen as a Kripke structure by Spot. So my class hold a reference to ts.

I clearly need ts to explore the graph, but apparently I also need model to dissect the states (let's say for now that I just want to print them). Would it be possible to add a model() method to ts so that I can retrieve the model from ts without having to store an additional reference?

Parser rejects input files that do not end with a new line

The parser should accept input files that do not end with \n.

Fix stats on covreach algorithm

When a new node covers existing nodes (l.127-132 in algorithm/covreach/algorithm.hh):

            for (node_ptr_t & covered_node : covered_nodes) {
              waiting.remove(covered_node);
              cover_node(covered_node, next_node, graph);
              covered_node->make_inactive();
              stats.increment_covered_nonleaf_nodes();
            }

We count all nodes as non leaf nodes (i.e. stats.increment_covered_nonleaf_nodes();), whereas some of the covered nodes may be leaf nodes (from the nodes list).

Output message when reading from standard input

TChecker silently waits when reading from standard input. A message should be displayed to let the user know what she should provide input.

Segmentation Fault with -c aMl and -c aLUl

Hi,

TChecker yields a segfault with options "-c aMl" or "-c aLUl". The following example is sufficient to produce the bug and "-m" option seems to have no influence:

system:S
process:P
location:P:A{initial:}
event:tau
edge:P:A:A:tau{}

Simplify graph display

Output graphs using a fixed format: nodes and edges, with attributes (free list of attributes). Then, implement tools to translate this format into DOT or other formats

Add methods to intersect two DBMs

We need methods:

bool tchecker::dbm::intersect(tchecker::dbm::db_t * dbm1, tchecker::dbm::db_t const * dbm2, tchecker::clock_id_t dim);

bool tchecker::dbm::intersect(tchecker::dbm::db_t * dbm1, tchecker::dbm::db_t const * dbm2, tchecker::dbm::db_t const * dbm3, tchecker::clock_id_t dim);

to check properties involving clock constraints.

parsing errors cause following parsing attempts to fail

I'm currently playing with Python bindings for tcltl. I want users to be able to type the TChecker models in a Jupyter notebook, and have them parsed and instantiated. Of course users will make errors (at least I did), fix them, and attempt to parse the model again.

This scenario is currently failing. It seems that after tchecker::parsing::parse_system_declaration() reports an error on a first model, it will fail to parse a new version of that model without that error.

Here is a C++ test case reproducing this:

#include <iostream>
#include <fstream>

#include "tchecker/parsing/parsing.hh"
#include "tchecker/utils/log.hh"
#include "tchecker/zg/zg_ta.hh"

void parse_and_print(const char* filename)
{
  tchecker::log_t log(&std::cerr);
  tchecker::parsing::system_declaration_t const * sysdecl = nullptr;
  try {
    sysdecl = tchecker::parsing::parse_system_declaration(filename, log);
    if (sysdecl == nullptr)
      throw std::runtime_error("System declaration cannot be built");

    // may throw on compilation failure
    tchecker::zg::ta::model_t model(*sysdecl, log);

    std::cout << *sysdecl << std::endl;
  }
  catch (std::exception const & e) {
    log.error(e.what());
  }
  delete sysdecl;
}


int main(int argc, char* argv[])
{
  std::ofstream file1("file1");
  file1 << R"(system:test
event:e
process:P
int:1:1:3:1:vari
clock:1:x
location:P:l1{initial: }
edge:P:l1:l1:e{})";   // note: missing final new line
  file1.flush();

  parse_and_print("file1"); // comment this, and the second parse works

  file1 << '\n';
  file1.flush();

  parse_and_print("file1");

  return 0;
}

The execution is as follows:

% g++ -std=c++17 -Wall foo.cc  -ltchecker
% ./a.out
7.17: ERROR, syntax error, unexpected end of file, expecting "\n"
ERROR, System compilation failure
ERROR, System declaration cannot be built

I was expecting the second call to parse_and_print() to work. It actually does work if you comment out the first call.

I suspect it has to do with error_count never being reset to 0. However there is more to it, because it seems the only purpose of error_count is to decide when to return nullptr, but in my first call to parse_and_print(), where error_count is apparently set, nullptr is not returned (instead we receive a system without the last line).

Evaluation of integer expressions as Booleans

Hi,

The documentation for expressions points out that an integer expression is false iff it is equal to 0.
If it is correct, in the following example, all values of 'count' should be reachable.
tchecker explore stops at value 2.

int:1:0:10:0:count
process:P
event: a
location:P:l0{initial:}
edge:P:l0:l0:a{provided: ! count : do : count = count+1 }
edge:P:l0:l0:a{provided: count : do : count = count+1 }

In the code of next in fsm.hh, guards, invariants and statements are checked to be different of 1 in which case an error status is returned. These expressions should be tested to be equal to 0, no ?

Problem with weak synchronisations

The following model raises an error that seems to come from weak synchronisation.

system:weak_error

clock:1:x

event:a
event:b

process:P1
location:P1:l0{initial:}
location:P1:l1
edge:P1:l0:l1:a

process:P2
location:P2:l0{initial:}
location:P2:l1
edge:P2:l0:l1:b

sync:P1@a:P2@a?

with the following output:

ERROR, no outgoing edge with that event ID

1 error(s)

Multilines attributes

Hi,

The parser for system descriptions does not allow values of attributes written on several lines.
Would it create an issue if we allow newlines (i.e. allows '\n' in TOK_TEXT in system.ll) ?

Assertion failed: (tchecker::dbm::is_tight(dbm, dim))

Running:

./tchecker explore -m zg:elapsed:extraLUg examples/ad94.txt

triggers an assertion:

Assertion failed: (tchecker::dbm::is_tight(dbm, dim)), function extra_lu, file /Users/herbrete/research/repositories/tchecker/src/dbm/dbm.cc, line 575.
Abort trap: 6

This occurs with extrapolations Ml, Mg and LUg, but not with other extrapolations.

(thanks Philipp Schlehuber!)

Problem with lu_map_capacity

Hi everyone,

when trying to copy create a transition system (elapsed/local_lu) i encountered some problems:

First when trying to do
ts_t ts2 = ts;
There is a compiler error. The compiler tries to use the template constructor (tchecker/zg/details/ts.hh line 52) instead of using the correct one (line 61). This can be fixed by making the template constructor explicit.

Then another problem appears: The capacity of the array in the local_lu_map is not correctly set. That is in the model the (tchecker::zg::ta::model_t) the capacity is correct, once the transition system constructed (ts_t ts(model)), the capacity takes on random(?) values. This causes then segmentation faults when invoking to copy constructor on ts.

An archive with an simply example (src/tchecker/test_cpy.cc) can be downloaded
here
where the problem is detailed in the comments. Simply run it on the examples in "bug_examples" which are just the tchecker files for corsso and csmacd with argument 5.

Have a nice day everyone,
Philipp

Error in resets

Hi everyone,

there is a bug in how the resets are performed if multiple "diagonal" updates are performed.
In the current code they are performed sequentially instead of "at once".

For instance if there are the clocks x,y and z and we have the resets
y':=x and z':=y the result will be
x'=x, y'=x and z'=x as the update y':=x is performed before z':=y and therefore y is already y'.

The error can be reproduced with the attached tchecker file.
I wrote a fix for the problem (see pull-request), but only for normal dbm's, not offset-dbm's.

A+
Philipp

multiple_value_reset.txt

add state comparisons

Just so we don't forget this; in my interface I sometimes need to compare two states (for instance to put them in a std::map). Any total order is ok (e.g., lexicographical) with me.

let garabage collection be robust to allocator destruction

Currently allocators do not "unregister" from the garbage collector. That means the GC must be stopped before any allocator is destroyed, causing issues such as #11. It also makes hard to build Python bindings, were you have little control on the destruction time.

It seems that having the allocators to unregister from the GC (and wait until their collecting function in not running anymore) when they are destroyed could solve these issues.

A compiling bug

When compiling the project by using "make -j" and building the project in Netbeans (gcc), I got the following errors:

/usr/bin/ld: cannot open output file tck-reach: Is a directory
collect2: error: ld returned 1 exit status
/usr/bin/ld: cannot open output file tck-syntax: Is a directory
collect2: error: ld returned 1 exit status
/usr/bin/ld: cannot open output file tck-simulate: Is a directory
collect2: error: ld returned 1 exit status
make[2]: *** [src/CMakeFiles/tck-reach.dir/build.make:130: src/tck-reach] Error 1
make[1]: *** [CMakeFiles/Makefile2:806: src/CMakeFiles/tck-reach.dir/all] Error 2
make[1]: *** Waiting for unfinished jobs....
make[2]: *** [src/CMakeFiles/tck-syntax.dir/build.make:100: src/tck-syntax] Error 1
make[2]: *** [src/CMakeFiles/tck-simulate.dir/build.make:115: src/tck-simulate] Error 1
make[1]: *** [CMakeFiles/Makefile2:779: src/CMakeFiles/tck-syntax.dir/all] Error 2
make[1]: *** [CMakeFiles/Makefile2:752: src/CMakeFiles/tck-simulate.dir/all] Error 2
/usr/bin/ld: cannot open output file tck-liveness: Is a directory
collect2: error: ld returned 1 exit status
make[2]: *** [src/CMakeFiles/tck-liveness.dir/build.make:115: src/tck-liveness] Error 1
make[1]: *** [CMakeFiles/Makefile2:833: src/CMakeFiles/tck-liveness.dir/all] Error 2
make: *** [Makefile:141: all] Error 2

Can you please tell me where I did wrong? Thank you.

Missing column in system declaration output

A system declaration is output as:
system foo
instead of
system:foo