add_test( [==[Empty cache]==] /home/karthik/IITB/MTP/tchecker/test/unit-tests/unittest [==[Empty cache]==])
set_tests_properties( [==[Empty cache]==] PROPERTIES WORKING_DIRECTORY /home/karthik/IITB/MTP/tchecker/test/unit-tests FIXTURES_SETUP BUILD_UNITTEST)
add_test( [==[Cache with 1 element]==] /home/karthik/IITB/MTP/tchecker/test/unit-tests/unittest [==[Cache with 1 element]==])
set_tests_properties( [==[Cache with 1 element]==] PROPERTIES WORKING_DIRECTORY /home/karthik/IITB/MTP/tchecker/test/unit-tests FIXTURES_SETUP BUILD_UNITTEST)
add_test( [==[Cache with many elements]==] /home/karthik/IITB/MTP/tchecker/test/unit-tests/unittest [==[Cache with many elements]==])
set_tests_properties( [==[Cache with many elements]==] PROPERTIES WORKING_DIRECTORY /home/karthik/IITB/MTP/tchecker/test/unit-tests FIXTURES_SETUP BUILD_UNITTEST)
add_test( [==[construction of upper bounds]==] /home/karthik/IITB/MTP/tchecker/test/unit-tests/unittest [==[construction of upper bounds]==])
set_tests_properties( [==[construction of upper bounds]==] PROPERTIES WORKING_DIRECTORY /home/karthik/IITB/MTP/tchecker/test/unit-tests FIXTURES_SETUP BUILD_UNITTEST)
add_test( [==[hash values of upper bounds]==] /home/karthik/IITB/MTP/tchecker/test/unit-tests/unittest [==[hash values of upper bounds]==])
set_tests_properties( [==[hash values of upper bounds]==] PROPERTIES WORKING_DIRECTORY /home/karthik/IITB/MTP/tchecker/test/unit-tests FIXTURES_SETUP BUILD_UNITTEST)
add_test( [==[comparators <,<=,>=,>]==] /home/karthik/IITB/MTP/tchecker/test/unit-tests/unittest [==[comparators <\,<=\,>=\,>]==])
set_tests_properties( [==[comparators <,<=,>=,>]==] PROPERTIES WORKING_DIRECTORY /home/karthik/IITB/MTP/tchecker/test/unit-tests FIXTURES_SETUP BUILD_UNITTEST)
add_test( sum /home/karthik/IITB/MTP/tchecker/test/unit-tests/unittest sum)
set_tests_properties( sum PROPERTIES WORKING_DIRECTORY /home/karthik/IITB/MTP/tchecker/test/unit-tests FIXTURES_SETUP BUILD_UNITTEST)
add_test( add /home/karthik/IITB/MTP/tchecker/test/unit-tests/unittest add)
set_tests_properties( add PROPERTIES WORKING_DIRECTORY /home/karthik/IITB/MTP/tchecker/test/unit-tests FIXTURES_SETUP BUILD_UNITTEST)
add_test( [==[min et max]==] /home/karthik/IITB/MTP/tchecker/test/unit-tests/unittest [==[min et max]==])
set_tests_properties( [==[min et max]==] PROPERTIES WORKING_DIRECTORY /home/karthik/IITB/MTP/tchecker/test/unit-tests FIXTURES_SETUP BUILD_UNITTEST)
add_test( [==[is_universal, structural tests]==] /home/karthik/IITB/MTP/tchecker/test/unit-tests/unittest [==[is_universal\, structural tests]==])
set_tests_properties( [==[is_universal, structural tests]==] PROPERTIES WORKING_DIRECTORY /home/karthik/IITB/MTP/tchecker/test/unit-tests FIXTURES_SETUP BUILD_UNITTEST)
add_test( [==[is_positive, structural test]==] /home/karthik/IITB/MTP/tchecker/test/unit-tests/unittest [==[is_positive\, structural test]==])
set_tests_properties( [==[is_positive, structural test]==] PROPERTIES WORKING_DIRECTORY /home/karthik/IITB/MTP/tchecker/test/unit-tests FIXTURES_SETUP BUILD_UNITTEST)
add_test( [==[is_universal_positive, structural test]==] /home/karthik/IITB/MTP/tchecker/test/unit-tests/unittest [==[is_universal_positive\, structural test]==])
set_tests_properties( [==[is_universal_positive, structural test]==] PROPERTIES WORKING_DIRECTORY /home/karthik/IITB/MTP/tchecker/test/unit-tests FIXTURES_SETUP BUILD_UNITTEST)
add_test( [==[is_empty_0, structural tests]==] /home/karthik/IITB/MTP/tchecker/test/unit-tests/unittest [==[is_empty_0\, structural tests]==])
set_tests_properties( [==[is_empty_0, structural tests]==] PROPERTIES WORKING_DIRECTORY /home/karthik/IITB/MTP/tchecker/test/unit-tests FIXTURES_SETUP BUILD_UNITTEST)
add_test( [==[is_tight, structural tests]==] /home/karthik/IITB/MTP/tchecker/test/unit-tests/unittest [==[is_tight\, structural tests]==])
set_tests_properties( [==[is_tight, structural tests]==] PROPERTIES WORKING_DIRECTORY /home/karthik/IITB/MTP/tchecker/test/unit-tests FIXTURES_SETUP BUILD_UNITTEST)
add_test( [==[universal makes universal zones]==] /home/karthik/IITB/MTP/tchecker/test/unit-tests/unittest [==[universal makes universal zones]==])
set_tests_properties( [==[universal makes universal zones]==] PROPERTIES WORKING_DIRECTORY /home/karthik/IITB/MTP/tchecker/test/unit-tests FIXTURES_SETUP BUILD_UNITTEST)
add_test( [==[universal_positive makes universal-positive zones]==] /home/karthik/IITB/MTP/tchecker/test/unit-tests/unittest [==[universal_positive makes universal-positive zones]==])
set_tests_properties( [==[universal_positive makes universal-positive zones]==] PROPERTIES WORKING_DIRECTORY /home/karthik/IITB/MTP/tchecker/test/unit-tests FIXTURES_SETUP BUILD_UNITTEST)
add_test( [==[tighten (full)]==] /home/karthik/IITB/MTP/tchecker/test/unit-tests/unittest [==[tighten (full)]==])
set_tests_properties( [==[tighten (full)]==] PROPERTIES WORKING_DIRECTORY /home/karthik/IITB/MTP/tchecker/test/unit-tests FIXTURES_SETUP BUILD_UNITTEST)
add_test( [==[tighten w.r.t. a difference bound]==] /home/karthik/IITB/MTP/tchecker/test/unit-tests/unittest [==[tighten w.r.t. a difference bound]==])
set_tests_properties( [==[tighten w.r.t. a difference bound]==] PROPERTIES WORKING_DIRECTORY /home/karthik/IITB/MTP/tchecker/test/unit-tests FIXTURES_SETUP BUILD_UNITTEST)
add_test( constrain /home/karthik/IITB/MTP/tchecker/test/unit-tests/unittest constrain)
set_tests_properties( constrain PROPERTIES WORKING_DIRECTORY /home/karthik/IITB/MTP/tchecker/test/unit-tests FIXTURES_SETUP BUILD_UNITTEST)
add_test( [==[DBM equality]==] /home/karthik/IITB/MTP/tchecker/test/unit-tests/unittest [==[DBM equality]==])
set_tests_properties( [==[DBM equality]==] PROPERTIES WORKING_DIRECTORY /home/karthik/IITB/MTP/tchecker/test/unit-tests FIXTURES_SETUP BUILD_UNITTEST)
add_test( [==[DBM inclusion]==] /home/karthik/IITB/MTP/tchecker/test/unit-tests/unittest [==[DBM inclusion]==])
set_tests_properties( [==[DBM inclusion]==] PROPERTIES WORKING_DIRECTORY /home/karthik/IITB/MTP/tchecker/test/unit-tests FIXTURES_SETUP BUILD_UNITTEST)
add_test( [==[reset DBM]==] /home/karthik/IITB/MTP/tchecker/test/unit-tests/unittest [==[reset DBM]==])
set_tests_properties( [==[reset DBM]==] PROPERTIES WORKING_DIRECTORY /home/karthik/IITB/MTP/tchecker/test/unit-tests FIXTURES_SETUP BUILD_UNITTEST)
add_test( [==[DBM open_up (delay)]==] /home/karthik/IITB/MTP/tchecker/test/unit-tests/unittest [==[DBM open_up (delay)]==])
set_tests_properties( [==[DBM open_up (delay)]==] PROPERTIES WORKING_DIRECTORY /home/karthik/IITB/MTP/tchecker/test/unit-tests FIXTURES_SETUP BUILD_UNITTEST)
add_test( [==[DBM intersection]==] /home/karthik/IITB/MTP/tchecker/test/unit-tests/unittest [==[DBM intersection]==])
set_tests_properties( [==[DBM intersection]==] PROPERTIES WORKING_DIRECTORY /home/karthik/IITB/MTP/tchecker/test/unit-tests FIXTURES_SETUP BUILD_UNITTEST)
add_test( [==[Checking tightness when the 0-row is modified]==] /home/karthik/IITB/MTP/tchecker/test/unit-tests/unittest [==[Checking tightness when the 0-row is modified]==])
set_tests_properties( [==[Checking tightness when the 0-row is modified]==] PROPERTIES WORKING_DIRECTORY /home/karthik/IITB/MTP/tchecker/test/unit-tests FIXTURES_SETUP BUILD_UNITTEST)
add_test( [==[Extrapolations from STTT06]==] /home/karthik/IITB/MTP/tchecker/test/unit-tests/unittest [==[Extrapolations from STTT06]==])
set_tests_properties( [==[Extrapolations from STTT06]==] PROPERTIES WORKING_DIRECTORY /home/karthik/IITB/MTP/tchecker/test/unit-tests FIXTURES_SETUP BUILD_UNITTEST)
add_test( [==[Extrapolations boundary case on M/U bounds]==] /home/karthik/IITB/MTP/tchecker/test/unit-tests/unittest [==[Extrapolations boundary case on M/U bounds]==])
set_tests_properties( [==[Extrapolations boundary case on M/U bounds]==] PROPERTIES WORKING_DIRECTORY /home/karthik/IITB/MTP/tchecker/test/unit-tests FIXTURES_SETUP BUILD_UNITTEST)
add_test( [==[Zone inclusion w.r.t. abstraction aM (1)]==] /home/karthik/IITB/MTP/tchecker/test/unit-tests/unittest [==[Zone inclusion w.r.t. abstraction aM (1)]==])
set_tests_properties( [==[Zone inclusion w.r.t. abstraction aM (1)]==] PROPERTIES WORKING_DIRECTORY /home/karthik/IITB/MTP/tchecker/test/unit-tests FIXTURES_SETUP BUILD_UNITTEST)
add_test( [==[Zone inclusion w.r.t. abstraction aM (2)]==] /home/karthik/IITB/MTP/tchecker/test/unit-tests/unittest [==[Zone inclusion w.r.t. abstraction aM (2)]==])
set_tests_properties( [==[Zone inclusion w.r.t. abstraction aM (2)]==] PROPERTIES WORKING_DIRECTORY /home/karthik/IITB/MTP/tchecker/test/unit-tests FIXTURES_SETUP BUILD_UNITTEST)
add_test( [==[Zone inclusion w.r.t. abstraction aLU from LICS12]==] /home/karthik/IITB/MTP/tchecker/test/unit-tests/unittest [==[Zone inclusion w.r.t. abstraction aLU from LICS12]==])
set_tests_properties( [==[Zone inclusion w.r.t. abstraction aLU from LICS12]==] PROPERTIES WORKING_DIRECTORY /home/karthik/IITB/MTP/tchecker/test/unit-tests FIXTURES_SETUP BUILD_UNITTEST)
add_test( [==[expression with no array variables]==] /home/karthik/IITB/MTP/tchecker/test/unit-tests/unittest [==[expression with no array variables]==])
set_tests_properties( [==[expression with no array variables]==] PROPERTIES WORKING_DIRECTORY /home/karthik/IITB/MTP/tchecker/test/unit-tests FIXTURES_SETUP BUILD_UNITTEST)
add_test( [==[expression with array variables]==] /home/karthik/IITB/MTP/tchecker/test/unit-tests/unittest [==[expression with array variables]==])
set_tests_properties( [==[expression with array variables]==] PROPERTIES WORKING_DIRECTORY /home/karthik/IITB/MTP/tchecker/test/unit-tests FIXTURES_SETUP BUILD_UNITTEST)
add_test( [==[statements with no array variable]==] /home/karthik/IITB/MTP/tchecker/test/unit-tests/unittest [==[statements with no array variable]==])
set_tests_properties( [==[statements with no array variable]==] PROPERTIES WORKING_DIRECTORY /home/karthik/IITB/MTP/tchecker/test/unit-tests FIXTURES_SETUP BUILD_UNITTEST)
add_test( [==[statements with array variables]==] /home/karthik/IITB/MTP/tchecker/test/unit-tests/unittest [==[statements with array variables]==])
set_tests_properties( [==[statements with array variables]==] PROPERTIES WORKING_DIRECTORY /home/karthik/IITB/MTP/tchecker/test/unit-tests FIXTURES_SETUP BUILD_UNITTEST)
add_test( [==[no throw if no weakly synchronized events]==] /home/karthik/IITB/MTP/tchecker/test/unit-tests/unittest [==[no throw if no weakly synchronized events]==])
set_tests_properties( [==[no throw if no weakly synchronized events]==] PROPERTIES WORKING_DIRECTORY /home/karthik/IITB/MTP/tchecker/test/unit-tests FIXTURES_SETUP BUILD_UNITTEST)
add_test( [==[no throw if weakly synchronized events have no guard]==] /home/karthik/IITB/MTP/tchecker/test/unit-tests/unittest [==[no throw if weakly synchronized events have no guard]==])
set_tests_properties( [==[no throw if weakly synchronized events have no guard]==] PROPERTIES WORKING_DIRECTORY /home/karthik/IITB/MTP/tchecker/test/unit-tests FIXTURES_SETUP BUILD_UNITTEST)
add_test( [==[throw if first weakly synchronized event has a guard]==] /home/karthik/IITB/MTP/tchecker/test/unit-tests/unittest [==[throw if first weakly synchronized event has a guard]==])
set_tests_properties( [==[throw if first weakly synchronized event has a guard]==] PROPERTIES WORKING_DIRECTORY /home/karthik/IITB/MTP/tchecker/test/unit-tests FIXTURES_SETUP BUILD_UNITTEST)
add_test( [==[throw if last weakly synchronized event has a guard]==] /home/karthik/IITB/MTP/tchecker/test/unit-tests/unittest [==[throw if last weakly synchronized event has a guard]==])
set_tests_properties( [==[throw if last weakly synchronized event has a guard]==] PROPERTIES WORKING_DIRECTORY /home/karthik/IITB/MTP/tchecker/test/unit-tests FIXTURES_SETUP BUILD_UNITTEST)
add_test( [==[throw if middle weakly synchronized event has a guard]==] /home/karthik/IITB/MTP/tchecker/test/unit-tests/unittest [==[throw if middle weakly synchronized event has a guard]==])
set_tests_properties( [==[throw if middle weakly synchronized event has a guard]==] PROPERTIES WORKING_DIRECTORY /home/karthik/IITB/MTP/tchecker/test/unit-tests FIXTURES_SETUP BUILD_UNITTEST)
add_test( [==[throw if some weakly synchronized event has a guard, several transitions]==] /home/karthik/IITB/MTP/tchecker/test/unit-tests/unittest [==[throw if some weakly synchronized event has a guard\, several transitions]==])
set_tests_properties( [==[throw if some weakly synchronized event has a guard, several transitions]==] PROPERTIES WORKING_DIRECTORY /home/karthik/IITB/MTP/tchecker/test/unit-tests FIXTURES_SETUP BUILD_UNITTEST)
add_test( [==[Offset clock variables from empty access map]==] /home/karthik/IITB/MTP/tchecker/test/unit-tests/unittest [==[Offset clock variables from empty access map]==])
set_tests_properties( [==[Offset clock variables from empty access map]==] PROPERTIES WORKING_DIRECTORY /home/karthik/IITB/MTP/tchecker/test/unit-tests FIXTURES_SETUP BUILD_UNITTEST)
add_test( [==[Offset clock variables from system - no array]==] /home/karthik/IITB/MTP/tchecker/test/unit-tests/unittest [==[Offset clock variables from system - no array]==])
set_tests_properties( [==[Offset clock variables from system - no array]==] PROPERTIES WORKING_DIRECTORY /home/karthik/IITB/MTP/tchecker/test/unit-tests FIXTURES_SETUP BUILD_UNITTEST)
add_test( [==[Offset clock variables from system - array]==] /home/karthik/IITB/MTP/tchecker/test/unit-tests/unittest [==[Offset clock variables from system - array]==])
set_tests_properties( [==[Offset clock variables from system - array]==] PROPERTIES WORKING_DIRECTORY /home/karthik/IITB/MTP/tchecker/test/unit-tests FIXTURES_SETUP BUILD_UNITTEST)
add_test( [==[translation clocks <-> offset variables]==] /home/karthik/IITB/MTP/tchecker/test/unit-tests/unittest [==[translation clocks <-> offset variables]==])
set_tests_properties( [==[translation clocks <-> offset variables]==] PROPERTIES WORKING_DIRECTORY /home/karthik/IITB/MTP/tchecker/test/unit-tests FIXTURES_SETUP BUILD_UNITTEST)
add_test( [==[is_positive, structural test for offset DBMs]==] /home/karthik/IITB/MTP/tchecker/test/unit-tests/unittest [==[is_positive\, structural test for offset DBMs]==])
set_tests_properties( [==[is_positive, structural test for offset DBMs]==] PROPERTIES WORKING_DIRECTORY /home/karthik/IITB/MTP/tchecker/test/unit-tests FIXTURES_SETUP BUILD_UNITTEST)
add_test( [==[is_universal_positive, structural test for offset DBMs]==] /home/karthik/IITB/MTP/tchecker/test/unit-tests/unittest [==[is_universal_positive\, structural test for offset DBMs]==])
set_tests_properties( [==[is_universal_positive, structural test for offset DBMs]==] PROPERTIES WORKING_DIRECTORY /home/karthik/IITB/MTP/tchecker/test/unit-tests FIXTURES_SETUP BUILD_UNITTEST)
add_test( [==[is_synchronized, structural test for offset DBMs]==] /home/karthik/IITB/MTP/tchecker/test/unit-tests/unittest [==[is_synchronized\, structural test for offset DBMs]==])
set_tests_properties( [==[is_synchronized, structural test for offset DBMs]==] PROPERTIES WORKING_DIRECTORY /home/karthik/IITB/MTP/tchecker/test/unit-tests FIXTURES_SETUP BUILD_UNITTEST)
add_test( [==[universal_positive offset DBMs]==] /home/karthik/IITB/MTP/tchecker/test/unit-tests/unittest [==[universal_positive offset DBMs]==])
set_tests_properties( [==[universal_positive offset DBMs]==] PROPERTIES WORKING_DIRECTORY /home/karthik/IITB/MTP/tchecker/test/unit-tests FIXTURES_SETUP BUILD_UNITTEST)
add_test( [==[synchronize offset DBMs]==] /home/karthik/IITB/MTP/tchecker/test/unit-tests/unittest [==[synchronize offset DBMs]==])
set_tests_properties( [==[synchronize offset DBMs]==] PROPERTIES WORKING_DIRECTORY /home/karthik/IITB/MTP/tchecker/test/unit-tests FIXTURES_SETUP BUILD_UNITTEST)
add_test( [==[reset to reference clocks on offset DBMs]==] /home/karthik/IITB/MTP/tchecker/test/unit-tests/unittest [==[reset to reference clocks on offset DBMs]==])
set_tests_properties( [==[reset to reference clocks on offset DBMs]==] PROPERTIES WORKING_DIRECTORY /home/karthik/IITB/MTP/tchecker/test/unit-tests FIXTURES_SETUP BUILD_UNITTEST)
add_test( [==[asynchronous_open_up on offset DBMs]==] /home/karthik/IITB/MTP/tchecker/test/unit-tests/unittest [==[asynchronous_open_up on offset DBMs]==])
set_tests_properties( [==[asynchronous_open_up on offset DBMs]==] PROPERTIES WORKING_DIRECTORY /home/karthik/IITB/MTP/tchecker/test/unit-tests FIXTURES_SETUP BUILD_UNITTEST)
add_test( [==[to_dbm on offset DBMs]==] /home/karthik/IITB/MTP/tchecker/test/unit-tests/unittest [==[to_dbm on offset DBMs]==])
set_tests_properties( [==[to_dbm on offset DBMs]==] PROPERTIES WORKING_DIRECTORY /home/karthik/IITB/MTP/tchecker/test/unit-tests FIXTURES_SETUP BUILD_UNITTEST)
add_test( [==[lexical ordering on ranges]==] /home/karthik/IITB/MTP/tchecker/test/unit-tests/unittest [==[lexical ordering on ranges]==])
set_tests_properties( [==[lexical ordering on ranges]==] PROPERTIES WORKING_DIRECTORY /home/karthik/IITB/MTP/tchecker/test/unit-tests FIXTURES_SETUP BUILD_UNITTEST)
add_test( [==[Empty access map]==] /home/karthik/IITB/MTP/tchecker/test/unit-tests/unittest [==[Empty access map]==])
set_tests_properties( [==[Empty access map]==] PROPERTIES WORKING_DIRECTORY /home/karthik/IITB/MTP/tchecker/test/unit-tests FIXTURES_SETUP BUILD_UNITTEST)
add_test( [==[Non empty access map]==] /home/karthik/IITB/MTP/tchecker/test/unit-tests/unittest [==[Non empty access map]==])
set_tests_properties( [==[Non empty access map]==] PROPERTIES WORKING_DIRECTORY /home/karthik/IITB/MTP/tchecker/test/unit-tests FIXTURES_SETUP BUILD_UNITTEST)
add_test( [==[variable access map computation - empty system]==] /home/karthik/IITB/MTP/tchecker/test/unit-tests/unittest [==[variable access map computation - empty system]==])
set_tests_properties( [==[variable access map computation - empty system]==] PROPERTIES WORKING_DIRECTORY /home/karthik/IITB/MTP/tchecker/test/unit-tests FIXTURES_SETUP BUILD_UNITTEST)
add_test( [==[variable access map computation - 1 process]==] /home/karthik/IITB/MTP/tchecker/test/unit-tests/unittest [==[variable access map computation - 1 process]==])
set_tests_properties( [==[variable access map computation - 1 process]==] PROPERTIES WORKING_DIRECTORY /home/karthik/IITB/MTP/tchecker/test/unit-tests FIXTURES_SETUP BUILD_UNITTEST)
add_test( [==[variable access map computation - 2 processes, no shared variable]==] /home/karthik/IITB/MTP/tchecker/test/unit-tests/unittest [==[variable access map computation - 2 processes\, no shared variable]==])
set_tests_properties( [==[variable access map computation - 2 processes, no shared variable]==] PROPERTIES WORKING_DIRECTORY /home/karthik/IITB/MTP/tchecker/test/unit-tests FIXTURES_SETUP BUILD_UNITTEST)
add_test( [==[variable access map computation - 3 processes, array, shared variables]==] /home/karthik/IITB/MTP/tchecker/test/unit-tests/unittest [==[variable access map computation - 3 processes\, array\, shared variables]==])
set_tests_properties( [==[variable access map computation - 3 processes, array, shared variables]==] PROPERTIES WORKING_DIRECTORY /home/karthik/IITB/MTP/tchecker/test/unit-tests FIXTURES_SETUP BUILD_UNITTEST)
set( unittest_TESTS [==[Empty cache]==] [==[Cache with 1 element]==] [==[Cache with many elements]==] [==[construction of upper bounds]==] [==[hash values of upper bounds]==] [==[comparators <,<=,>=,>]==] sum add [==[min et max]==] [==[is_universal, structural tests]==] [==[is_positive, structural test]==] [==[is_universal_positive, structural test]==] [==[is_empty_0, structural tests]==] [==[is_tight, structural tests]==] [==[universal makes universal zones]==] [==[universal_positive makes universal-positive zones]==] [==[tighten (full)]==] [==[tighten w.r.t. a difference bound]==] constrain [==[DBM equality]==] [==[DBM inclusion]==] [==[reset DBM]==] [==[DBM open_up (delay)]==] [==[DBM intersection]==] [==[Checking tightness when the 0-row is modified]==] [==[Extrapolations from STTT06]==] [==[Extrapolations boundary case on M/U bounds]==] [==[Zone inclusion w.r.t. abstraction aM (1)]==] [==[Zone inclusion w.r.t. abstraction aM (2)]==] [==[Zone inclusion w.r.t. abstraction aLU from LICS12]==] [==[expression with no array variables]==] [==[expression with array variables]==] [==[statements with no array variable]==] [==[statements with array variables]==] [==[no throw if no weakly synchronized events]==] [==[no throw if weakly synchronized events have no guard]==] [==[throw if first weakly synchronized event has a guard]==] [==[throw if last weakly synchronized event has a guard]==] [==[throw if middle weakly synchronized event has a guard]==] [==[throw if some weakly synchronized event has a guard, several transitions]==] [==[Offset clock variables from empty access map]==] [==[Offset clock variables from system - no array]==] [==[Offset clock variables from system - array]==] [==[translation clocks <-> offset variables]==] [==[is_positive, structural test for offset DBMs]==] [==[is_universal_positive, structural test for offset DBMs]==] [==[is_synchronized, structural test for offset DBMs]==] [==[universal_positive offset DBMs]==] [==[synchronize offset DBMs]==] [==[reset to reference clocks on offset DBMs]==] [==[asynchronous_open_up on offset DBMs]==] [==[to_dbm on offset DBMs]==] [==[lexical ordering on ranges]==] [==[Empty access map]==] [==[Non empty access map]==] [==[variable access map computation - empty system]==] [==[variable access map computation - 1 process]==] [==[variable access map computation - 2 processes, no shared variable]==] [==[variable access map computation - 3 processes, array, shared variables]==])
