diff --git a/.github/workflows/build-and-test.yml b/.github/workflows/build-and-test.yml index 2cc7fb03..194ff6cc 100644 --- a/.github/workflows/build-and-test.yml +++ b/.github/workflows/build-and-test.yml @@ -12,7 +12,7 @@ jobs: intsize: ["all:int16:memcheck", "all:int32:memcheck", "all:int64:memcheck"] compiler: ["gcc", "clang"] runs-on: ubuntu-latest - container: alzeha/echtzeitsysteme-tchecker-${{ matrix.compiler }}:v0.1 + container: alzeha/echtzeitsysteme-tchecker-${{ matrix.compiler }}:latest env: CONFNAME: ${{ matrix.intsize }} INSTALL_DIR: "install" diff --git a/CppCheckSuppressions.txt b/CppCheckSuppressions.txt index 146be0ab..c4aa1123 100644 --- a/CppCheckSuppressions.txt +++ b/CppCheckSuppressions.txt @@ -4,16 +4,5 @@ nullPointer:*/tchecker/src/refzg/refzg.cc:[181, 176, 189, 190, 197, 203, 208] uninitdata:*/include/tchecker/utils/shared_objects.hh nullPointer:*/src/refzg/refzg.cc -// TODO: fix the following -rethrowNoCurrentException:*/include/tchecker/variables/variables.hh -assertWithSideEffect:*/include/tchecker/variables/variables.hh -funcArgOrderDifferent:*/src/clockbounds/solver.cc -assertWithSideEffect:*/include/tchecker/waiting/waiting.hh -uninitMemberVar:*/src/algorithms/covreach/stats.cc - -// TODO: decide whether to fix the following -operatorEqVarError:*/include/tchecker/utils/shared_objects.hh -missingMemberCopy:*/include/tchecker/utils/shared_objects.hh - // the following is a known cppcheck bug internalAstError:*/include/tchecker/graph/directed_graph.hh diff --git a/ci-scripts/Dockerfile b/ci-scripts/Dockerfile index b3dba3f1..b36a35c3 100644 --- a/ci-scripts/Dockerfile +++ b/ci-scripts/Dockerfile @@ -4,7 +4,7 @@ ARG CXX RUN apt update && \ apt install -y \ git cmake bison flex doxygen wget \ - valgrind graphviz + valgrind graphviz cppcheck FROM base as gcc-image diff --git a/examples/Lieb_et_al_1.sh b/examples/Lieb_et_al_1.sh new file mode 100755 index 00000000..edf9185d --- /dev/null +++ b/examples/Lieb_et_al_1.sh @@ -0,0 +1,8 @@ +#!/bin/bash + +# This file is a part of the TChecker project. +# +# See files AUTHORS and LICENSE for copyright details. + +cat "$(dirname $0)/strong_timed_bisim_system_tests/Lieb_et_al/A1.txt" + diff --git a/examples/Lieb_et_al_1_diff_invariant.sh b/examples/Lieb_et_al_1_diff_invariant.sh new file mode 100755 index 00000000..459ee51b --- /dev/null +++ b/examples/Lieb_et_al_1_diff_invariant.sh @@ -0,0 +1,8 @@ +#!/bin/bash + +# This file is a part of the TChecker project. +# +# See files AUTHORS and LICENSE for copyright details. + +cat "$(dirname $0)/strong_timed_bisim_system_tests/Lieb_et_al/A1_different_invariant.txt" + diff --git a/examples/Lieb_et_al_1_non_determ_bisim.sh b/examples/Lieb_et_al_1_non_determ_bisim.sh new file mode 100755 index 00000000..67997569 --- /dev/null +++ b/examples/Lieb_et_al_1_non_determ_bisim.sh @@ -0,0 +1,8 @@ +#!/bin/bash + +# This file is a part of the TChecker project. +# +# See files AUTHORS and LICENSE for copyright details. + +cat "$(dirname $0)/strong_timed_bisim_system_tests/Lieb_et_al/A1_non_determ_bisim.txt" + diff --git a/examples/Lieb_et_al_2.sh b/examples/Lieb_et_al_2.sh new file mode 100755 index 00000000..ac9baefc --- /dev/null +++ b/examples/Lieb_et_al_2.sh @@ -0,0 +1,8 @@ +#!/bin/bash + +# This file is a part of the TChecker project. +# +# See files AUTHORS and LICENSE for copyright details. + +cat "$(dirname $0)/strong_timed_bisim_system_tests/Lieb_et_al/A2.txt" + diff --git a/examples/Lieb_et_al_2_determ_split_bisim.sh b/examples/Lieb_et_al_2_determ_split_bisim.sh new file mode 100755 index 00000000..3087fa04 --- /dev/null +++ b/examples/Lieb_et_al_2_determ_split_bisim.sh @@ -0,0 +1,8 @@ +#!/bin/bash + +# This file is a part of the TChecker project. +# +# See files AUTHORS and LICENSE for copyright details. + +cat "$(dirname $0)/strong_timed_bisim_system_tests/Lieb_et_al/A2_determ_split_bisim.txt" + diff --git a/examples/Lieb_et_al_2_determ_split_non_bisim.sh b/examples/Lieb_et_al_2_determ_split_non_bisim.sh new file mode 100755 index 00000000..0cd601cf --- /dev/null +++ b/examples/Lieb_et_al_2_determ_split_non_bisim.sh @@ -0,0 +1,8 @@ +#!/bin/bash + +# This file is a part of the TChecker project. +# +# See files AUTHORS and LICENSE for copyright details. + +cat "$(dirname $0)/strong_timed_bisim_system_tests/Lieb_et_al/A2_determ_split_non_bisim.txt" + diff --git a/examples/Lieb_et_al_2_non_determ_bisim.sh b/examples/Lieb_et_al_2_non_determ_bisim.sh new file mode 100755 index 00000000..575f3f02 --- /dev/null +++ b/examples/Lieb_et_al_2_non_determ_bisim.sh @@ -0,0 +1,8 @@ +#!/bin/bash + +# This file is a part of the TChecker project. +# +# See files AUTHORS and LICENSE for copyright details. + +cat "$(dirname $0)/strong_timed_bisim_system_tests/Lieb_et_al/A2_non_determ_bisim.txt" + diff --git a/examples/Lieb_et_al_3.sh b/examples/Lieb_et_al_3.sh new file mode 100755 index 00000000..9d30097f --- /dev/null +++ b/examples/Lieb_et_al_3.sh @@ -0,0 +1,8 @@ +#!/bin/bash + +# This file is a part of the TChecker project. +# +# See files AUTHORS and LICENSE for copyright details. + +cat "$(dirname $0)/strong_timed_bisim_system_tests/Lieb_et_al/A3.txt" + diff --git a/examples/Lieb_et_al_4.sh b/examples/Lieb_et_al_4.sh new file mode 100755 index 00000000..03c748f4 --- /dev/null +++ b/examples/Lieb_et_al_4.sh @@ -0,0 +1,8 @@ +#!/bin/bash + +# This file is a part of the TChecker project. +# +# See files AUTHORS and LICENSE for copyright details. + +cat "$(dirname $0)/strong_timed_bisim_system_tests/Lieb_et_al/A4.txt" + diff --git a/examples/Lieb_et_al_5.sh b/examples/Lieb_et_al_5.sh new file mode 100755 index 00000000..a0d375b0 --- /dev/null +++ b/examples/Lieb_et_al_5.sh @@ -0,0 +1,8 @@ +#!/bin/bash + +# This file is a part of the TChecker project. +# +# See files AUTHORS and LICENSE for copyright details. + +cat "$(dirname $0)/strong_timed_bisim_system_tests/Lieb_et_al/A5.txt" + diff --git a/examples/count_to_inf.sh b/examples/count_to_inf.sh new file mode 100755 index 00000000..2b2ebdc2 --- /dev/null +++ b/examples/count_to_inf.sh @@ -0,0 +1 @@ +cat "$(dirname $0)/count_to_inf.txt" diff --git a/examples/count_to_inf.txt b/examples/count_to_inf.txt new file mode 100644 index 00000000..34e122ac --- /dev/null +++ b/examples/count_to_inf.txt @@ -0,0 +1,20 @@ +# This file is a part of the TChecker project. +# +# See files AUTHORS and LICENSE for copyright details. + +system:count_to_inf + +clock:1:x +clock:1:y + +event:a +event:b +event:c + +process:P +location:P:A{initial:} +location:P:B{invariant: y<1} +location:P:C{invariant: x<=2} +edge:P:A:B:a{do: x=0;y=0} +edge:P:B:C:b{do: x=0;y=0} +edge:P:C:C:c{provided: x>=2 : do: x=0} diff --git a/examples/easy-ad94-added-transition.sh b/examples/easy-ad94-added-transition.sh new file mode 100755 index 00000000..327f0aae --- /dev/null +++ b/examples/easy-ad94-added-transition.sh @@ -0,0 +1,9 @@ +#!/bin/bash + +# This file is a part of the TChecker project. +# +# See files AUTHORS and LICENSE for copyright details. + +echo "# labels=green" + +cat "$(dirname $0)/strong_timed_bisim_system_tests/easy_ad94/easy_ad94_added_transition.txt" diff --git a/examples/easy-ad94-different-guard.sh b/examples/easy-ad94-different-guard.sh new file mode 100755 index 00000000..5118e321 --- /dev/null +++ b/examples/easy-ad94-different-guard.sh @@ -0,0 +1,9 @@ +#!/bin/bash + +# This file is a part of the TChecker project. +# +# See files AUTHORS and LICENSE for copyright details. + +echo "# labels=green" + +cat "$(dirname $0)/strong_timed_bisim_system_tests/easy_ad94/easy_ad94_different_guard.txt" diff --git a/examples/easy-ad94.sh b/examples/easy-ad94.sh new file mode 100755 index 00000000..004add6b --- /dev/null +++ b/examples/easy-ad94.sh @@ -0,0 +1,9 @@ +#!/bin/bash + +# This file is a part of the TChecker project. +# +# See files AUTHORS and LICENSE for copyright details. + +echo "# labels=green" + +cat "$(dirname $0)/strong_timed_bisim_system_tests/easy_ad94/easy_ad94.txt" diff --git a/examples/strong_timed_bisim_system_tests/Lieb_et_al/A1.txt b/examples/strong_timed_bisim_system_tests/Lieb_et_al/A1.txt new file mode 100644 index 00000000..5bd2fc69 --- /dev/null +++ b/examples/strong_timed_bisim_system_tests/Lieb_et_al/A1.txt @@ -0,0 +1,19 @@ +# This file is a part of the TChecker project. +# +# See files AUTHORS and LICENSE for copyright details. + +system:Lieb_et_al_A1 + +clock:1:x + +event:a +event:b +event:c + +process:P +location:P:A{initial:} +location:P:B{invariant: x<2} +location:P:C{} +edge:P:A:B:a{provided: x<=0} +edge:P:B:C:b{} +edge:P:C:A:c{provided: x>3 : do: x=0} diff --git a/examples/strong_timed_bisim_system_tests/Lieb_et_al/A1_different_invariant.txt b/examples/strong_timed_bisim_system_tests/Lieb_et_al/A1_different_invariant.txt new file mode 100644 index 00000000..f880645e --- /dev/null +++ b/examples/strong_timed_bisim_system_tests/Lieb_et_al/A1_different_invariant.txt @@ -0,0 +1,19 @@ +# This file is a part of the TChecker project. +# +# See files AUTHORS and LICENSE for copyright details. + +system:Lieb_et_al_A1 + +clock:1:x + +event:a +event:b +event:c + +process:P +location:P:A{initial:} +location:P:B{invariant: x<3} +location:P:C{} +edge:P:A:B:a{provided: x<=0} +edge:P:B:C:b{} +edge:P:C:A:c{provided: x>3 : do: x=0} diff --git a/examples/strong_timed_bisim_system_tests/Lieb_et_al/A1_non_determ_bisim.txt b/examples/strong_timed_bisim_system_tests/Lieb_et_al/A1_non_determ_bisim.txt new file mode 100644 index 00000000..e2c021ac --- /dev/null +++ b/examples/strong_timed_bisim_system_tests/Lieb_et_al/A1_non_determ_bisim.txt @@ -0,0 +1,22 @@ +# This file is a part of the TChecker project. +# +# See files AUTHORS and LICENSE for copyright details. + +system:Lieb_et_al_A1 + +clock:1:x + +event:a +event:b +event:c + +process:P +location:P:A{initial:} +location:P:B{invariant: x<2} +location:P:C{} +location:P:CPrime{} +edge:P:A:B:a{provided: x<=0} +edge:P:B:C:b{provided: x<=1} +edge:P:B:CPrime:b{provided:x>1} +edge:P:C:A:c{provided: x>3 : do: x=0} +edge:P:CPrime:A:c{provided: x>3 : do: x=0} diff --git a/examples/strong_timed_bisim_system_tests/Lieb_et_al/A2.txt b/examples/strong_timed_bisim_system_tests/Lieb_et_al/A2.txt new file mode 100644 index 00000000..26c15aaa --- /dev/null +++ b/examples/strong_timed_bisim_system_tests/Lieb_et_al/A2.txt @@ -0,0 +1,19 @@ +# This file is a part of the TChecker project. +# +# See files AUTHORS and LICENSE for copyright details. + +system:Lieb_et_al_A1 + +clock:1:x + +event:a +event:b +event:c + +process:P +location:P:A{initial:} +location:P:B{invariant: x<2} +location:P:C{} +edge:P:A:B:a{do: x=0} +edge:P:B:C:b{} +edge:P:C:A:c{provided: x>3 : do: x=0} diff --git a/examples/strong_timed_bisim_system_tests/Lieb_et_al/A2_determ_split_bisim.txt b/examples/strong_timed_bisim_system_tests/Lieb_et_al/A2_determ_split_bisim.txt new file mode 100644 index 00000000..5b63a54c --- /dev/null +++ b/examples/strong_timed_bisim_system_tests/Lieb_et_al/A2_determ_split_bisim.txt @@ -0,0 +1,24 @@ +# This file is a part of the TChecker project. +# +# See files AUTHORS and LICENSE for copyright details. + +system:Lieb_et_al_A2_determ_split_bisim + +clock:1:x + +event:a +event:b +event:c + +process:P +location:P:A{initial:} +location:P:B{invariant: x<2} +location:P:BPrime{invariant: x<2} +location:P:C{} +location:P:CPrime{} +edge:P:A:B:a{provided: x<2 : do: x=0} +edge:P:A:BPrime:a{provided: x>=2 : do: x=0} +edge:P:B:C:b{} +edge:P:BPrime:CPrime:b{} +edge:P:C:A:c{provided: x>3 : do: x=0} +edge:P:CPrime:A:c{provided: x>3 : do: x=0} diff --git a/examples/strong_timed_bisim_system_tests/Lieb_et_al/A2_determ_split_non_bisim.txt b/examples/strong_timed_bisim_system_tests/Lieb_et_al/A2_determ_split_non_bisim.txt new file mode 100644 index 00000000..c45da91c --- /dev/null +++ b/examples/strong_timed_bisim_system_tests/Lieb_et_al/A2_determ_split_non_bisim.txt @@ -0,0 +1,24 @@ +# This file is a part of the TChecker project. +# +# See files AUTHORS and LICENSE for copyright details. + +system:Lieb_et_al_A2_determ_split_non_bisim + +clock:1:x + +event:a +event:b +event:c + +process:P +location:P:A{initial:} +location:P:B{invariant: x<2} +location:P:BPrime{invariant: x<2} +location:P:C{} +location:P:CPrime{} +edge:P:A:B:a{provided: x<2 : do: x=0} +edge:P:A:BPrime:a{provided: x>2 : do: x=0} +edge:P:B:C:b{} +edge:P:BPrime:CPrime:b{} +edge:P:C:A:c{provided: x>3 : do: x=0} +edge:P:CPrime:A:c{provided: x>3 : do: x=0} diff --git a/examples/strong_timed_bisim_system_tests/Lieb_et_al/A2_non_determ_bisim.txt b/examples/strong_timed_bisim_system_tests/Lieb_et_al/A2_non_determ_bisim.txt new file mode 100644 index 00000000..fee66d3c --- /dev/null +++ b/examples/strong_timed_bisim_system_tests/Lieb_et_al/A2_non_determ_bisim.txt @@ -0,0 +1,24 @@ +# This file is a part of the TChecker project. +# +# See files AUTHORS and LICENSE for copyright details. + +system:Lieb_et_al_A2_non_determ_bisim + +clock:1:x + +event:a +event:b +event:c + +process:P +location:P:A{initial:} +location:P:B{invariant: x<2} +location:P:BPrime{invariant: x<2} +location:P:C{} +location:P:CPrime{} +edge:P:A:B:a{provided: x<2 : do: x=0} +edge:P:A:BPrime:a{provided: x>=1 : do: x=0} +edge:P:B:C:b{} +edge:P:BPrime:CPrime:b{} +edge:P:C:A:c{provided: x>3 : do: x=0} +edge:P:CPrime:A:c{provided: x>3 : do: x=0} diff --git a/examples/strong_timed_bisim_system_tests/Lieb_et_al/A3.txt b/examples/strong_timed_bisim_system_tests/Lieb_et_al/A3.txt new file mode 100644 index 00000000..d0c518a0 --- /dev/null +++ b/examples/strong_timed_bisim_system_tests/Lieb_et_al/A3.txt @@ -0,0 +1,20 @@ +# This file is a part of the TChecker project. +# +# See files AUTHORS and LICENSE for copyright details. + +system:Lieb_et_al_A1 + +clock:1:x +clock:1:y + +event:a +event:b +event:c + +process:P +location:P:A{initial:} +location:P:B{invariant: x<2} +location:P:C{} +edge:P:A:B:a{do: x=0;y=0} +edge:P:B:C:b{} +edge:P:C:A:c{provided: y>3 : do: x=0;y=0} diff --git a/examples/strong_timed_bisim_system_tests/Lieb_et_al/A4.txt b/examples/strong_timed_bisim_system_tests/Lieb_et_al/A4.txt new file mode 100644 index 00000000..14929e25 --- /dev/null +++ b/examples/strong_timed_bisim_system_tests/Lieb_et_al/A4.txt @@ -0,0 +1,20 @@ +# This file is a part of the TChecker project. +# +# See files AUTHORS and LICENSE for copyright details. + +system:Lieb_et_al_A1 + +clock:1:x +clock:1:y + +event:a +event:b +event:c + +process:P +location:P:A{initial:} +location:P:B{invariant: x<2} +location:P:C{} +edge:P:A:B:a{do: x=0} +edge:P:B:C:b{do:y=0} +edge:P:C:A:c{provided: y>3 : do: x=0;y=0} diff --git a/examples/strong_timed_bisim_system_tests/Lieb_et_al/A5.txt b/examples/strong_timed_bisim_system_tests/Lieb_et_al/A5.txt new file mode 100644 index 00000000..dffa5ec5 --- /dev/null +++ b/examples/strong_timed_bisim_system_tests/Lieb_et_al/A5.txt @@ -0,0 +1,27 @@ +# This file is a part of the TChecker project. +# +# See files AUTHORS and LICENSE for copyright details. + +system:Lieb_et_al_A1 + +clock:1:x +clock:1:y + +event:a +event:b +event:c + +process:P +location:P:A{initial:} +location:P:B{invariant: x<2} +location:P:C{} +location:P:BPrime{invariant: x<2} +location:P:CPrime{} + +edge:P:A:B:a{do: x=0} +edge:P:B:C:b{do: y=0} +edge:P:C:A:c{provided: y>3 : do: x=0;y=0} + +edge:P:A:BPrime:a{do: x=0;y=0} +edge:P:BPrime:CPrime:b{} +edge:P:CPrime:A:c{provided: y>3 : do: x=0;y=0} diff --git a/examples/strong_timed_bisim_system_tests/easy_ad94/easy-ad94-different-guard.txt b/examples/strong_timed_bisim_system_tests/easy_ad94/easy-ad94-different-guard.txt new file mode 100644 index 00000000..e96ac26f --- /dev/null +++ b/examples/strong_timed_bisim_system_tests/easy_ad94/easy-ad94-different-guard.txt @@ -0,0 +1,21 @@ +# This file is a part of the TChecker project. +# +# See files AUTHORS and LICENSE for copyright details. + +system:easy_ad94_different_guard_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: x=0; y=0} +edge:P:l1:l2:b{provided: y==2 && x<=2 } diff --git a/examples/strong_timed_bisim_system_tests/easy_ad94/easy_ad94.txt b/examples/strong_timed_bisim_system_tests/easy_ad94/easy_ad94.txt new file mode 100644 index 00000000..bed2440b --- /dev/null +++ b/examples/strong_timed_bisim_system_tests/easy_ad94/easy_ad94.txt @@ -0,0 +1,21 @@ +# This file is a part of the TChecker project. +# +# See files AUTHORS and LICENSE for copyright details. + +system:easy_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: x=0; y=0} +edge:P:l1:l2:b{provided: y==1 && x<=2 } diff --git a/examples/strong_timed_bisim_system_tests/easy_ad94/easy_ad94_added_transition.txt b/examples/strong_timed_bisim_system_tests/easy_ad94/easy_ad94_added_transition.txt new file mode 100644 index 00000000..33b93221 --- /dev/null +++ b/examples/strong_timed_bisim_system_tests/easy_ad94/easy_ad94_added_transition.txt @@ -0,0 +1,22 @@ +# This file is a part of the TChecker project. +# +# See files AUTHORS and LICENSE for copyright details. + +system:easy_ad94_added_transition_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: x=0; y=0} +edge:P:l1:l2:b{provided: y==1 && x<=2 } +edge:P:l1:l2:c{ } diff --git a/examples/strong_timed_bisim_system_tests/easy_ad94/easy_ad94_different_guard.txt b/examples/strong_timed_bisim_system_tests/easy_ad94/easy_ad94_different_guard.txt new file mode 100644 index 00000000..e96ac26f --- /dev/null +++ b/examples/strong_timed_bisim_system_tests/easy_ad94/easy_ad94_different_guard.txt @@ -0,0 +1,21 @@ +# This file is a part of the TChecker project. +# +# See files AUTHORS and LICENSE for copyright details. + +system:easy_ad94_different_guard_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: x=0; y=0} +edge:P:l1:l2:b{provided: y==2 && x<=2 } diff --git a/include/tchecker/dbm/dbm.hh b/include/tchecker/dbm/dbm.hh index 2a042aa6..7f3be836 100644 --- a/include/tchecker/dbm/dbm.hh +++ b/include/tchecker/dbm/dbm.hh @@ -999,6 +999,29 @@ enum clock_position_t { enum tchecker::dbm::clock_position_t clock_position(tchecker::dbm::db_t const * dbm, tchecker::clock_id_t dim, tchecker::clock_id_t x1, tchecker::clock_id_t x2); +/* + \brief Return value of convex-union +*/ +enum union_convex_t { + UNION_IS_CONVEX, /*!< the union of two dbm can be represented as a dbm */ + UNION_IS_NOT_CONVEX /*!< the union of two dbm cannot be represented as a dbm */ +}; + +/*! + \brief tries to union two dbms + \param result : where the result will be stored (must be allocated!) + \param dbm1 : a dbm + \param dbm2 : a dbm to be unioned with dbm1 + \param dim : the dimension (must be the same for all dbm!) + \pre none of the dbm is nullptr (checked by assertion) + dbm1 and dbm1 are consistent and tight (checked by assertion) + dim >= 1 (checked by assertion) + \return UNION_IS_CONVEX if the union of dbm1 and dbm2 can be represented by a dbm. UNION_IS_NOT_CONVEX otherwise + \post if UNION_IS_CONVEX is returned, result contains the union. + \note This function implements the convex-union algorithm from the dissertation "Rokicki, Tomas Gerhard: Representing and modeling digital circuits, Stanford University, 1994" + */ +enum tchecker::dbm::union_convex_t convex_union(tchecker::dbm::db_t *result, tchecker::dbm::db_t const * dbm1, tchecker::dbm::db_t const * dbm2, tchecker::clock_id_t dim); + } // end of namespace dbm } // end of namespace tchecker diff --git a/include/tchecker/dbm/details/db_safe.hh b/include/tchecker/dbm/details/db_safe.hh index e9cc675d..735f0950 100644 --- a/include/tchecker/dbm/details/db_safe.hh +++ b/include/tchecker/dbm/details/db_safe.hh @@ -95,8 +95,13 @@ static_assert(tchecker::dbm::LE_ZERO != tchecker::dbm::LT_INFINITY, ""); */ inline tchecker::dbm::db_t db(enum tchecker::ineq_cmp_t cmp, tchecker::integer_t value) { - if ((value < tchecker::dbm::MIN_VALUE) || (value > tchecker::dbm::MAX_VALUE)) + if (value == INF_VALUE && cmp == tchecker::LT) + { + return tchecker::dbm::LT_INFINITY; + } + if ((value < tchecker::dbm::MIN_VALUE) || (value > tchecker::dbm::MAX_VALUE)) { throw std::invalid_argument("value out of bounds"); + } return db_t{cmp, value}; } @@ -151,6 +156,12 @@ inline int db_cmp(tchecker::dbm::db_t const & db1, tchecker::dbm::db_t const & d return db1.cmp - db2.cmp; } +inline tchecker::dbm::db_t invert(tchecker::dbm::db_t const & to_invert) +{ + return tchecker::dbm::db(to_invert.cmp==tchecker::LE ? tchecker::LT : tchecker::LE, (-1)*to_invert.value); +} + + /*! \brief Less-than operator on difference bounds \param db1 : a difference bound diff --git a/include/tchecker/dbm/details/db_unsafe.hh b/include/tchecker/dbm/details/db_unsafe.hh index 80ef646d..58f09488 100644 --- a/include/tchecker/dbm/details/db_unsafe.hh +++ b/include/tchecker/dbm/details/db_unsafe.hh @@ -99,6 +99,11 @@ inline tchecker::dbm::db_t add(tchecker::dbm::db_t db, tchecker::integer_t value return (db + (value << 1)); } +inline tchecker::dbm::db_t invert(tchecker::dbm::db_t const & to_invert) +{ + return tchecker::dbm::db(to_invert.cmp==tchecker::LE ? tchecker::LT : tchecker::LE, to_invert.value); +} + /*! \note Standard comparison operators <, <=, ==, !=, >= and > on integers carry on difference bounds */ diff --git a/include/tchecker/extrapolation/extrapolation_factory.hh b/include/tchecker/extrapolation/extrapolation_factory.hh index d6209ac7..828ebc4b 100644 --- a/include/tchecker/extrapolation/extrapolation_factory.hh +++ b/include/tchecker/extrapolation/extrapolation_factory.hh @@ -34,7 +34,6 @@ enum extrapolation_type_t { EXTRA_M_LOCAL, /*!< see tchecker::zg::local_extra_m_t */ EXTRA_M_PLUS_GLOBAL, /*!< see tchecker::zg::global_extra_m_plus_t */ EXTRA_M_PLUS_LOCAL, /*!< see tchecker::zg::local_extra_m_plus_t */ - EXTRA_K_NORM /* see tchecker::zg::k_norm */ }; /*! @@ -69,8 +68,8 @@ namespace vcg { /*! \brief Zone extrapolation factory \param extrapolation_type : type of extrapolation - \param orig_system_first : first system of timed processes - \param orig_system_secpmd : second system of timed processes + \param system_first : first system of timed processes + \param system_second : second system of timed processes \param first_not_second : true iff this vcg is the left hand side of the comparison \return a zone extrapolation of type extrapolation_type using clock bounds inferred from the systems, nullptr if clock bounds cannot be inferred from system (see @@ -80,8 +79,8 @@ namespace vcg { */ tchecker::zg::extrapolation_t * extrapolation_factory( enum tchecker::zg::extrapolation_type_t type, - std::shared_ptr const & orig_system_first, - std::shared_ptr const & orig_system_second, + std::shared_ptr system_first, + std::shared_ptr system_second, bool first_not_second); } // end of namespace vcg diff --git a/include/tchecker/extrapolation/k_norm.hh b/include/tchecker/extrapolation/k_norm.hh deleted file mode 100644 index a15d4a03..00000000 --- a/include/tchecker/extrapolation/k_norm.hh +++ /dev/null @@ -1,67 +0,0 @@ -/* - * This file is a part of the TChecker project. - * - * See files AUTHORS and LICENSE for copyright details. - * - */ - -#ifndef TCHECKER_ZG_EXTRAPOLATION_K_NORM_HH -#define TCHECKER_ZG_EXTRAPOLATION_K_NORM_HH - -#include "tchecker/extrapolation/extrapolation.hh" -#include "tchecker/extrapolation/global_lu_extrapolation.hh" - -namespace tchecker { - -namespace zg { - -/*! - \class k_norm - \brief K-Normalization for zone extrapolation - */ -class k_norm final : public tchecker::zg::global_extra_lu_t { -public: - - /*! - \brief Constructor - \param clock_bounds : global LU clock bounds map - \note WARNING: we change the clock bounds, ignoring the const statement - */ - k_norm(std::shared_ptr const & clock_bounds); - - /*! - \brief Destructor - */ - virtual ~k_norm() = default; - - using tchecker::zg::global_extra_lu_t::extrapolate; - -}; - -} // end of namespace zg - -namespace vcg { - -class k_norm_virtual final : public tchecker::zg::global_extra_lu_t { -public: - /*! - \brief Constructor - \param clock_bounds : global LU clock bounds map - \note WARNING: we change the clock bounds, ignoring the const statement - */ - k_norm_virtual(std::shared_ptr const & clock_bounds); - - /*! - \brief Destructor - */ - virtual ~k_norm_virtual() = default; - - using tchecker::zg::global_extra_lu_t::extrapolate; - -}; - -} // end of namespace vcg - -} // end of namespace tchecker - -#endif diff --git a/include/tchecker/strong-timed-bisim/stats.hh b/include/tchecker/strong-timed-bisim/stats.hh index cc7fc806..7592a3f5 100644 --- a/include/tchecker/strong-timed-bisim/stats.hh +++ b/include/tchecker/strong-timed-bisim/stats.hh @@ -8,7 +8,10 @@ #ifndef TCHECKER_ALGORITHMS_COMPARE_STATS_HH #define TCHECKER_ALGORITHMS_COMPARE_STATS_HH +#include + #include "tchecker/algorithms/stats.hh" +#include "tchecker/zg/state.hh" /*! \file stats.hh @@ -35,20 +38,13 @@ public: \brief Accessor \return A reference to the number of visited pair of states */ - unsigned long visited_pair_of_states() const; - - /*! - \brief Accessor - \return Number of visited transitions - */ - unsigned long visited_transitions() const; + long visited_pair_of_states() const; /*! - \brief Accessor - \return The deepest path checked - */ - - unsigned long deepest_path() const; + \brief setter for the number of visited pair of states + \post visited_pair_of_states is set to the given value + */ + void set_visited_pair_of_states(long visited_pair_of_states); /*! \brief Accessor @@ -56,6 +52,12 @@ public: */ bool relationship_fulfilled() const; + /*! + \brief setter for relationship_fulfilled + \post relationship_fulfilled is set to the given value + */ + void set_relationship_fulfilled(bool relationship_fulfilled); + /*! \brief Extract statistics as attributes (key, value) \param m : attributes map @@ -64,9 +66,7 @@ public: void attributes(std::map & m) const; private: - unsigned long _visited_pair_of_states; /*!< Number of visited pairs of states */ - unsigned long _visited_transitions; /*!< Number of visited transitions */ - unsigned long _deepest_path; /*!< Number of visited transitions */ + long _visited_pair_of_states; /*!< Number of visited pairs of states */ bool _relationship_fulfilled; /*< Whether the relationship is fulfilled */ }; diff --git a/include/tchecker/strong-timed-bisim/virtual_clock_algorithm.hh b/include/tchecker/strong-timed-bisim/virtual_clock_algorithm.hh index 4f924422..02f83768 100644 --- a/include/tchecker/strong-timed-bisim/virtual_clock_algorithm.hh +++ b/include/tchecker/strong-timed-bisim/virtual_clock_algorithm.hh @@ -5,8 +5,16 @@ * */ -#ifndef TCHECKER_ALGORITHMS_REACH_ALGORITHM_HH -#define TCHECKER_ALGORITHMS_REACH_ALGORITHM_HH +#ifndef TCHECKER_STRONG_TIMED_BISIM_VIRTUAL_CLOCK_ALGORITHM_HH +#define TCHECKER_STRONG_TIMED_BISIM_VIRTUAL_CLOCK_ALGORITHM_HH + +#define TCHECKER_STRONG_TIMED_BISIM_VIRTUAL_CLOCK_ALGORITHM_HH_SEED 0xDEADBEEF + +#if BOOST_VERSION <= 106600 +#include +#else +#include +#endif #include "tchecker/strong-timed-bisim/stats.hh" #include "tchecker/vcg/vcg.hh" @@ -42,52 +50,62 @@ public: private: + struct custom_hash { + size_t operator()(const std::pair &to_hash) const { + std::size_t h1 = tchecker::zg::hash_value(*(to_hash.first)); + std::size_t h2 = tchecker::zg::hash_value(*(to_hash.second)); + + // https://stackoverflow.com/questions/2590677/how-do-i-combine-hash-values-in-c0x + std::size_t h = (h1 + 0x9e3779b9 + (TCHECKER_STRONG_TIMED_BISIM_VIRTUAL_CLOCK_ALGORITHM_HH_SEED <<6) + (TCHECKER_STRONG_TIMED_BISIM_VIRTUAL_CLOCK_ALGORITHM_HH_SEED>>2)); + h ^= (h2 + 0x9e3779b9 + + (TCHECKER_STRONG_TIMED_BISIM_VIRTUAL_CLOCK_ALGORITHM_HH_SEED <<6) + (TCHECKER_STRONG_TIMED_BISIM_VIRTUAL_CLOCK_ALGORITHM_HH_SEED>>2)); + return h; + } + }; + + struct custom_equal { + bool operator() (const std::pair &p1, const std::pair &p2) const { + return (*(p1.first) == *(p2.first)) && (*(p1.second) == *(p2.second)); + } + }; + + /*! + \brief check-for-virt-bisim function of Lieb et al. + \param symb_state_first : the symbolic state that belongs to the first vcg + \param symbolic_trans_first : the transition with which we reached the first symbolic state + \param symb_state_second : the symbolic state that belongs to the second vcg + \param symbolic_trans_second : the transition with which we reached the second symbolic state + \param last_was_epsilon : whether the last transition was a delay transition + \return a list of virtual constraints that are not bisimilar + */ + std::shared_ptr> + check_for_virt_bisim(tchecker::zg::const_state_sptr_t symb_state_first, tchecker::zg::transition_sptr_t symbolic_trans_first, + tchecker::zg::const_state_sptr_t symb_state_second, tchecker::zg::transition_sptr_t symbolic_trans_second, + std::unordered_set, custom_hash, custom_equal> & visited, + bool last_was_epsilon); + /*! \brief check-for-outgoing-transitions-impl function of Lieb et al. \param symb_state_first : the symbolic state that belongs to the first vcg \param vcg_first : the first vcg \param symb_state_second : the symbolic state that belongs to the second vcg \param vcg_second : the second vcg - \param func : a function that takes two symbolic states and returns a list of virtual constraint + \param A_is_first : whether the outgoing transitions of A or B shall be checked \return a list of virtual constraints that cannot be simulated. \note the result is allocated at the heap and must be freed. */ - std::shared_ptr> - check_for_outgoing_transitions( tchecker::zg::const_state_sptr_t symb_state_first, - std::shared_ptr vcg_first, - tchecker::zg::const_state_sptr_t symb_state_second, - std::shared_ptr vcg_second, - std::shared_ptr> - (*func)(tchecker::zg::state_sptr_t, tchecker::zg::state_sptr_t)); - - /* - \brief calling check_for_outgoing_transitions with first = A - */ - inline std::shared_ptr> - check_for_outgoing_transitions_of_A( tchecker::zg::const_state_sptr_t symb_state_A, - tchecker::zg::const_state_sptr_t symb_state_B, - std::shared_ptr> - (*func)(tchecker::zg::state_sptr_t, tchecker::zg::state_sptr_t)) - { - return check_for_outgoing_transitions(symb_state_A, _A, symb_state_B, _B, func); - } - - /* - \brief calling check_for_outgoing_transitions with first = B - */ - inline std::shared_ptr> - check_for_outgoing_transitions_of_B( tchecker::zg::const_state_sptr_t symb_state_A, - tchecker::zg::const_state_sptr_t symb_state_B, - std::shared_ptr> - (*func)(tchecker::zg::state_sptr_t, tchecker::zg::state_sptr_t)) - { - return check_for_outgoing_transitions(symb_state_B, _B, symb_state_A, _A, func); - } + check_for_outgoing_transitions( tchecker::zg::const_state_sptr_t A_state, + tchecker::zg::const_state_sptr_t B_state, + std::unordered_set, custom_hash, custom_equal> & visited); const std::shared_ptr _A; const std::shared_ptr _B; + long _visited_pair_of_states; + + long _delete_me; + + }; } // end of namespace strong_timed_bisim diff --git a/include/tchecker/utils/zone_container.hh b/include/tchecker/utils/zone_container.hh index cc24c904..e3517cc4 100644 --- a/include/tchecker/utils/zone_container.hh +++ b/include/tchecker/utils/zone_container.hh @@ -9,6 +9,7 @@ #define TCHECKER_ZG_ZONE_CONTAINER_HH #include +#include #include "tchecker/zg/zone.hh" #include "tchecker/vcg/virtual_constraint.hh" @@ -34,13 +35,13 @@ public: \brief Constructor \param dim : dimension */ - zone_container_t(tchecker::clock_id_t dim) : _dim(dim){ } + zone_container_t(tchecker::clock_id_t dim) : _dim(dim), _storage(std::make_shared>>(0)) { } /*! \brief Copy Constructor \param container : the container to copy */ - zone_container_t(zone_container_t &t) : _dim(t.dim()), _storage(0) + zone_container_t(zone_container_t &t) : _dim(t.dim()), _storage(std::make_shared>>(0)) { for(auto iter = t.begin(); iter < t.end(); iter++) { this->append_zone(*(*iter)); @@ -60,23 +61,13 @@ public: std::shared_ptr create_element(T const &zone); - /*! - \brief destructor of zone. Calling the destructor of tchecker::zg::zone_t - \note If T extends tchecker::zg::zone_t by a datastructure, there is a need for - specialisation here! - */ - void destruct_element(std::shared_ptr zone) - { - tchecker::zg::zone_destruct_and_deallocate(&(*zone)); - } - /* \brief check for emptiness of the container \return true if and only if the container is empty */ bool is_empty() { - return 0 == _storage.size(); + return 0 == _storage->size(); } /*! @@ -84,7 +75,7 @@ public: */ void append_zone() { - _storage.emplace_back(create_element()); + _storage->emplace_back(create_element()); } /*! @@ -92,7 +83,8 @@ public: */ void append_zone(T const & zone) { - _storage.emplace_back(create_element(zone)); + assert(_dim == zone.dim()); + _storage->emplace_back(create_element(zone)); } @@ -103,16 +95,55 @@ public: */ void append_zone(std::shared_ptr zone) { - _storage.emplace_back(zone); + assert(_dim == zone->dim()); + _storage->emplace_back(zone); + } + + /*! + \brief adds the elements of other to this + \param other: the container to append + \post other is appended to the container + */ + void append_container(std::shared_ptr> other) + { + assert(other->_dim == this->_dim); + for(auto iter = other->begin(); iter < other->end(); iter++) { + this->append_zone(*iter); + } + } + + /*! + \brief adds the elements of other to this. The elements that can be accessed are the same! + \param other: the container to append + \post other is appended to the container + */ + void append_container(zone_container_t &other) + { + assert(other._dim == this->_dim); + for(auto iter = other.begin(); iter < other.end(); iter++) { + this->append_zone(*iter); + } } /*! \brief removes the last zone and deletes the content */ - void remove_back() + void remove_first() { destruct_element(*(_storage.begin())); - _storage.erase(_storage.begin()); + _storage->erase(_storage.begin()); + } + + /*! + \brief removes all empty zones + */ + void remove_empty() + { + for(auto iter = this->begin(); iter < this->end(); iter++) { + if(iter->empty()) { + _storage->erase(iter); + } + } } /*! @@ -121,7 +152,7 @@ public: */ std::shared_ptr back() { - return _storage.back(); + return _storage->back(); } /*! @@ -131,7 +162,7 @@ public: */ std::shared_ptr operator[](typename std::vector>::size_type i) { - return _storage[i]; + return (*_storage)[i]; } /*! @@ -140,7 +171,7 @@ public: */ typename std::vector>::size_type size() { - return _storage.size(); + return _storage->size(); } /*! @@ -148,7 +179,7 @@ public: */ typename std::vector>::iterator begin() { - return _storage.begin(); + return _storage->begin(); } /*! @@ -156,22 +187,63 @@ public: */ typename std::vector>::iterator end() { - return _storage.end(); + return _storage->end(); } /*! - \brief Destructor + \brief compresses the zone container if possible + \post let zc_prev be the zone container before the call and zc_after the zone container after. The following conditions hold: + - zc_prev._dim = zc_after._dim + - for all zone_prev in zc_prev : for all u in zone_prev : exists zone_after in zc_after : u in zone_after + - for all zone_after in zc_after : for all u in zone_after : exists zone_prev in zc_prev : u in zone_prev */ - ~zone_container_t() + + void compress() { - for(auto iter = begin(); iter < end(); ++iter) { - destruct_element(*iter); - } + + std::shared_ptr>> result = _storage; + + bool reduced; + + do { + auto prev = result->size(); + result = find_union_partner(*result); + reduced = (result->size() < prev); + } while (reduced); + + assert(result->size() <= _storage->size()); + + _storage = result; + } private: + + std::shared_ptr>> find_union_partner(std::vector> const cur) + { + std::shared_ptr>> result = std::make_shared>>(); + + for(auto to_add = cur.begin(); to_add < cur.end(); ++to_add) { + bool found = false; + for(auto in_result = result->begin(); in_result < result->end(); ++in_result) { + tchecker::dbm::db_t cur_union[this->dim() * this->dim()]; + if(tchecker::dbm::union_convex_t::UNION_IS_CONVEX == tchecker::dbm::convex_union(cur_union, (*to_add)->dbm(), (*in_result)->dbm(), this->dim())) { + found = true; + tchecker::dbm::copy((*in_result)->dbm(), cur_union, this->dim()); + break; + } + } + + if(!found) { + result->emplace_back(*to_add); + } + } + + return result; + } + const tchecker::clock_id_t _dim; - std::vector> _storage; + std::shared_ptr>> _storage; }; @@ -188,13 +260,6 @@ std::shared_ptr zone_contain template<> std::shared_ptr zone_container_t::create_element(tchecker::virtual_constraint::virtual_constraint_t const & zone); -/*! - \brief contained-in-all function (see the TR of Lieb et al.) - \param a vector of vector of zones - \return a vector of zones - */ -zone_container_t contained_in_all(std::vector> & zones, tchecker::clock_id_t dim); - } // end of namespace tchecker diff --git a/include/tchecker/vcg/revert_transitions.hh b/include/tchecker/vcg/revert_transitions.hh index 219d2ab4..06422a91 100644 --- a/include/tchecker/vcg/revert_transitions.hh +++ b/include/tchecker/vcg/revert_transitions.hh @@ -11,6 +11,10 @@ #include "tchecker/vcg/virtual_constraint.hh" #include "tchecker/zg/zone.hh" +namespace tchecker { + +namespace vcg { + /*! \brief revert-action-trans function (see the TR of Lieb et al.) \param zone : the original zone @@ -36,4 +40,8 @@ revert_action_trans(const tchecker::zg::zone_t & zone, std::shared_ptr revert_epsilon_trans(const tchecker::zg::zone_t & zone, const tchecker::virtual_constraint::virtual_constraint_t & phi_split); +} // end of namespace vcg + +} // end of namespace tchecker + #endif diff --git a/include/tchecker/vcg/sync.hh b/include/tchecker/vcg/sync.hh index a29df996..ae4e2bba 100644 --- a/include/tchecker/vcg/sync.hh +++ b/include/tchecker/vcg/sync.hh @@ -8,6 +8,7 @@ #ifndef TCHECKER_VCG_SYNC_HH #define TCHECKER_VCG_SYNC_HH +#include "tchecker/dbm/dbm.hh" #include "virtual_constraint.hh" namespace tchecker { @@ -18,7 +19,8 @@ namespace vcg { \brief sync function (see the TR of Lieb et al.) \param dbm1 : a dbm \param dbm2 : a dbm - \param dim : dimension of dbm1 and dbm2 + \param dim1 : dimension of dbm1 + \param dim2 : dimension of dbm2 \param lowest_virt_clk_id : the clk id of chi_0 \param no_of_orig_clocks_1 : the number of orig clocks in the first TA \param orig_reset1 : the resets of the transition of the first TA @@ -32,11 +34,26 @@ namespace vcg { \note the change happens inplace */ -void sync(tchecker::dbm::db_t *dbm1, tchecker::dbm::db_t *dbm2, tchecker::clock_id_t dim, - tchecker::clock_id_t lowest_virt_clk_id, tchecker::clock_id_t no_of_orig_clocks_1, +void sync(tchecker::dbm::db_t *dbm1, tchecker::dbm::db_t *dbm2, + tchecker::clock_id_t dim1, tchecker::clock_id_t dim2, + tchecker::clock_id_t no_of_orig_clocks_1, tchecker::clock_id_t no_of_orig_clocks_2, tchecker::clock_reset_container_t const & orig_reset1, tchecker::clock_reset_container_t const & orig_reset2); +/*! + \brief checks whether the following dbm are synced + \param dbm1 : the DBM of A + \param dbm2 : the DBM of B + \param dim1 : the dim of dbm1 + \param dim2 : the dim of dbm2 + \param no_of_original_clocks_1 : the number of non virt (and non ref) clocks of A + \param no_of_original_clocks_2 : the number of non virt (and non ref) clocks of B + */ + +bool are_dbm_synced(tchecker::dbm::db_t *dbm1, tchecker::dbm::db_t *dbm2, + tchecker::clock_id_t dim1, tchecker::clock_id_t dim2, + tchecker::clock_id_t no_of_orig_clocks_1, tchecker::clock_id_t no_of_orig_clocks_2); + /*! \brief revert-sync function (see the TR of Lieb et al.) \param dbm1 : a dbm @@ -53,10 +70,11 @@ void sync(tchecker::dbm::db_t *dbm1, tchecker::dbm::db_t *dbm2, tchecker::clock_ \note the change happens inplace. this function works if and only if only resets to zero are allowed! */ -std::tuple, std::shared_ptr> -revert_sync(const tchecker::dbm::db_t *dbm1, const tchecker::dbm::db_t *dbm2, tchecker::clock_id_t dim, - const tchecker::virtual_constraint::virtual_constraint_t & phi_e, tchecker::clock_id_t lowest_virt_clk_id, - tchecker::clock_id_t no_of_orig_clocks_1); +std::pair, std::shared_ptr> +revert_sync(const tchecker::dbm::db_t *dbm1, const tchecker::dbm::db_t *dbm2, + tchecker::clock_id_t dim1, tchecker::clock_id_t dim2, + tchecker::clock_id_t no_of_orig_clocks_1, tchecker::clock_id_t no_of_orig_clocks_2, + const tchecker::virtual_constraint::virtual_constraint_t & phi_e); } // end of namespace vcg diff --git a/include/tchecker/vcg/vcg.hh b/include/tchecker/vcg/vcg.hh index ea6e2135..8d52d61d 100644 --- a/include/tchecker/vcg/vcg.hh +++ b/include/tchecker/vcg/vcg.hh @@ -36,10 +36,11 @@ public: \param sharing_type : type of state/transition sharing \param semantics : a zone semantics \param no_of_virtual_clocks : number of virtual clocks - \param extrapolation : a zone extrapolation + \param extrapolation : a zone extrapolation \param block_size : number of objects allocated in a block \param table_size : size of hash tables - \note all states and transitions are pool allocated and deallocated automatically + \note all states and transitions are pool allocated and deallocated automatically. + enable_extrapolation is set to false, since the current bisimulation algorithm does the extrapolation by itself */ vcg_t(std::shared_ptr const & system, enum tchecker::ts::sharing_type_t sharing_type, std::shared_ptr const & semantics, tchecker::clock_id_t no_of_virtual_clocks, @@ -51,6 +52,8 @@ public: */ tchecker::clock_id_t get_no_of_virtual_clocks() const; + inline tchecker::clock_id_t get_no_of_original_clocks() const { return _system->clocks_count(tchecker::variable_kind_t::VK_FLATTENED) - _no_of_virtual_clocks;} + private: tchecker::clock_id_t _no_of_virtual_clocks; diff --git a/include/tchecker/vcg/virtual_constraint.hh b/include/tchecker/vcg/virtual_constraint.hh index 88f2283c..b0e5028b 100644 --- a/include/tchecker/vcg/virtual_constraint.hh +++ b/include/tchecker/vcg/virtual_constraint.hh @@ -52,13 +52,13 @@ public: \brief Accessor \return no of virtual clocks */ - const tchecker::clock_id_t get_no_of_virt_clocks() const; + tchecker::clock_id_t get_no_of_virt_clocks() const; /*! \brief return the virtual constraint as list of clock constraints - \param sum_of_orig_clocks : the sum of the original clocks of both TA + \param no_of_orig_clocks : the number of orig clocks, used as offset */ - clock_constraint_container_t get_vc(tchecker::clock_id_t orig_clocks_offset) const; + clock_constraint_container_t get_vc(tchecker::clock_id_t no_of_orig_clocks, bool system_clocks) const; /*! \brief returns the negated version of this clock constraint @@ -66,20 +66,58 @@ public: * forall u with u model this and for all vc in result u does not model vc * forall u with u does not model this exists a vc in result such that u models vc * (for u in ({\chi_0, ..., \chi_{|C_A| + | C_B| - 1}} \rightarrow T)) + \note the result can easily become very large. Try to avoid this method and use neg_logic_and instead. */ - tchecker::zone_container_t * neg() const; + std::shared_ptr> neg() const; + + /* + \brief returns the (not this and other) + \param result : the pointer in which the result will be stored. Has to be allocated! + \param other : the other vc not this shall be anded with + */ + void neg_logic_and(std::shared_ptr> result, const virtual_constraint_t & other) const; + + /* + \brief returns (this and zone) + \param result : the pointer in which the result will be stored. Has to be allocated! + \param zone : the zone this shall be anded with + \return EMPTY if the resulting DBM is empty, NON_EMPTY otherwise + */ + enum tchecker::dbm::status_t logic_and(std::shared_ptr result, const virtual_constraint_t & other) const; + + /* + \brief returns (this and zone) + \param result : the pointer in which the result will be stored. Has to be allocated! + \param zone : the zone this shall be anded with + \return EMPTY if the resulting DBM is empty, NON_EMPTY otherwise + */ + enum tchecker::dbm::status_t logic_and(std::shared_ptr result, const tchecker::zg::zone_t & zone) const; + + /* + \brief returns (this and zone) + \param result : the ref in which the result will be stored. + \param zone : the zone this shall be anded with + \return EMPTY if the resulting DBM is empty, NON_EMPTY otherwise + */ + enum tchecker::dbm::status_t logic_and(tchecker::zg::zone_t & result, const tchecker::zg::zone_t & zone) const; /* \brief iterates through the container and logically ands each element with this + \param result : the pointer in which the result will be stored. Has to be allocated! \param container : the container to and with - \return a copy of container with each element being logically anded with this. + \return a container with each element of container being logically anded with this. */ - tchecker::zone_container_t logic_and(tchecker::zone_container_t *container); + void logic_and(std::shared_ptr> result, + std::shared_ptr> const container) const; + +private: + + std::shared_ptr> neg_helper(tchecker::dbm::db_t *upper_bounds) const; }; // factories -std::shared_ptr factory(tchecker::clock_id_t dim); +std::shared_ptr factory(tchecker::clock_id_t no_of_virtual_clocks); std::shared_ptr factory(tchecker::virtual_constraint::virtual_constraint_t const & virtual_constraint); @@ -91,6 +129,14 @@ std::shared_ptr factory(tchecker::virtual_constraint::virt */ std::shared_ptr factory(std::shared_ptr zone, tchecker::clock_id_t no_of_virtual_clocks); +/*! + \brief extract the virtual constraint from a zone + \param zone : the zone from which the virtual constraint should be extracted + \param virtual_clocks : the number of virtual clocks + \return the virtual constraint of zone + */ +std::shared_ptr factory(tchecker::zg::zone_t const & zone, tchecker::clock_id_t no_of_virtual_clocks); + /*! \brief extract the virtual constraint from a dbm \param dbm : the dbm from which the virtual constraint should be extracted @@ -100,16 +146,20 @@ std::shared_ptr factory(std::shared_ptr factory(const tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim, tchecker::clock_id_t no_of_virtual_clocks); -// destruction - -void destruct(virtual_constraint_t *to_destruct); - /*! \brief combine operator (see the TR of Lieb et al.) - \param a vector of vector of virtual constraints - \return a vector of virtual constraints + \param a container of virtual constraints + \return a container of virtual constraints + */ +std::shared_ptr> combine(tchecker::zone_container_t & lo_vc, tchecker::clock_id_t no_of_virtual_clocks); + +/*! + \brief contained-in-all function (see the TR of Lieb et al.) + \param a vector of container of zones + \return a container of zones */ -tchecker::zone_container_t *combine(std::vector> & lo_lo_vc, tchecker::clock_id_t dim); +std::shared_ptr> contained_in_all(std::vector>> & zones, tchecker::clock_id_t no_of_virtual_clocks); + } // end of namespace virtual_constraint diff --git a/include/tchecker/zg/semantics.hh b/include/tchecker/zg/semantics.hh index 7d69ead9..373e13d2 100644 --- a/include/tchecker/zg/semantics.hh +++ b/include/tchecker/zg/semantics.hh @@ -101,6 +101,20 @@ public: tchecker::clock_constraint_container_t const & guard, tchecker::clock_reset_container_t const & clkreset, bool tgt_delay_allowed, tchecker::clock_constraint_container_t const & tgt_invariant) = 0; + + /*! + \brief Compute next zone when epsilon transition is used + \param dbm : a DBM + \param dim : dimension of dbm + \param invariant : invariant of current state + \post dbm has been delayed (if allowed), then intersected with src_invariant, + \return tchecker::STATE_OK if the resulting DBM is not empty. Otherwise, + tchecker::STATE_CLOCKS_SRC_INVARIANT_VIOLATED if intersection with src_invariant + result in an empty zone + */ + tchecker::state_status_t delay( tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim, + tchecker::clock_constraint_container_t const & invariant); + }; /*! @@ -340,19 +354,6 @@ public: virtual tchecker::state_status_t final(tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim, bool delay_allowed, tchecker::clock_constraint_container_t const & invariant); - /*! - \brief Compute next zone when epsilon transition is used - \param dbm : a DBM - \param dim : dimension of dbm - \param invariant : invariant of current state - \post dbm has been delayed (if allowed), then intersected with src_invariant, - \return tchecker::STATE_OK if the resulting DBM is not empty. Otherwise, - tchecker::STATE_CLOCKS_SRC_INVARIANT_VIOLATED if intersection with src_invariant - result in an empty zone - */ - tchecker::state_status_t delay( tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim, - tchecker::clock_constraint_container_t const & invariant); - /*! \brief Compute next zone when action transition is used \param dbm : a DBM diff --git a/include/tchecker/zg/state.hh b/include/tchecker/zg/state.hh index a7f3ea10..453216ec 100644 --- a/include/tchecker/zg/state.hh +++ b/include/tchecker/zg/state.hh @@ -101,6 +101,13 @@ public: */ constexpr inline tchecker::zg::zone_t const & zone() const { return *_zone; } + + /*! + \brief Accessor + \return zone in this state + */ + constexpr inline tchecker::zg::zone_t & zone() { return *_zone; } + /*! \brief Accessor \return reference to pointer to the zone in this state diff --git a/include/tchecker/zg/zg.hh b/include/tchecker/zg/zg.hh index 9a8193f5..eb682a11 100644 --- a/include/tchecker/zg/zg.hh +++ b/include/tchecker/zg/zg.hh @@ -169,12 +169,14 @@ public: */ zg_t(std::shared_ptr const & system, enum tchecker::ts::sharing_type_t sharing_type, std::shared_ptr const & semantics, - std::shared_ptr const & extrapolation, std::size_t block_size, std::size_t table_size) + std::shared_ptr const & extrapolation, std::size_t block_size, std::size_t table_size, + bool enable_extrapolation = true) : _system(system), _sharing_type(sharing_type), _semantics(semantics), _extrapolation(extrapolation), _state_allocator(block_size, block_size, _system->processes_count(), block_size, _system->intvars_count(tchecker::VK_FLATTENED), block_size, _system->clocks_count(tchecker::VK_FLATTENED) + 1, table_size), - _transition_allocator(block_size, block_size, _system->processes_count(), table_size) + _transition_allocator(block_size, block_size, _system->processes_count(), table_size), + _enable_extrapolation(enable_extrapolation) { } @@ -402,6 +404,14 @@ public: void split(tchecker::zg::const_state_sptr_t const & s, tchecker::clock_constraint_container_t const & constraints, std::vector & v); + /*! + \brief runs the extrapolation on the given dbm + \param dbm : the dbm to extrapolate + \param dim : the dimension of the dbm + \param vloc : a set of locations + \post the dbm is extrapolated + */ + inline void run_extrapolation(tchecker::dbm::db_t *dbm, tchecker::clock_id_t dim, tchecker::vloc_t const & vloc) const { _extrapolation->extrapolate(dbm, dim, vloc); } // Inspector @@ -472,6 +482,12 @@ public: */ inline tchecker::ta::system_t const & system() const { return *_system; } + /*! + \brief Accessor + \return Underlying semantics + */ + inline std::shared_ptr const & semantics() const { return _semantics; } + /*! \brief Accessor \return sharing type of this synchronized product @@ -482,9 +498,13 @@ public: \brief Accessor \return number of clocks */ - inline tchecker::clock_id_t clocks_count() { return _system->clocks_count(tchecker::VK_FLATTENED); } + inline tchecker::clock_id_t clocks_count() const { return _system->clocks_count(tchecker::VK_FLATTENED); } + + inline tchecker::zg::state_sptr_t create_state() {return _state_allocator.construct();} + inline tchecker::zg::state_sptr_t clone_state(tchecker::zg::const_state_sptr_t const & to_clone) {return _state_allocator.clone(*to_clone);} + inline tchecker::zg::state_sptr_t clone_state(tchecker::zg::state_sptr_t const & to_clone) {return _state_allocator.clone(*to_clone);} -private: +protected: /*! \brief High-Order function to shorten the handling of states and transitions @@ -511,7 +531,7 @@ private: tchecker::zg::state_sptr_t &, tchecker::zg::transition_sptr_t &, helping_hand_t *), - tchecker::zg::const_state_sptr_t const & to_clone, bool clone + tchecker::zg::const_state_sptr_t const & to_clone, bool clone, bool enable_extrapolation = true ); /*! \brief Clone and constrain a state @@ -537,6 +557,7 @@ private: std::shared_ptr _extrapolation; /*!< Zone extrapolation */ tchecker::zg::state_pool_allocator_t _state_allocator; /*!< Pool allocator of states */ tchecker::zg::transition_pool_allocator_t _transition_allocator; /*! Pool allocator of transitions */ + bool _enable_extrapolation; }; /* tools */ @@ -571,13 +592,13 @@ next(tchecker::zg::zg_t &zg, std::shared_ptr factory(std::shared_ptr const & system, enum tchecker::ts::sharing_type_t sharing_type, enum tchecker::zg::semantics_type_t semantics_type, enum tchecker::zg::extrapolation_type_t extrapolation_type, std::size_t block_size, - std::size_t table_size); + std::size_t table_size, bool enable_extrapolation = true); std::shared_ptr factory(std::shared_ptr const & system, enum tchecker::ts::sharing_type_t sharing_type, enum tchecker::zg::semantics_type_t semantics_type, enum tchecker::zg::extrapolation_type_t extrapolation_type, tchecker::clockbounds::clockbounds_t const & clock_bounds, std::size_t block_size, - std::size_t table_size); + std::size_t table_size, bool enable_extrapolation = true); } // end of namespace zg diff --git a/src/dbm/dbm.cc b/src/dbm/dbm.cc index 9cf4618e..97ca3ae9 100644 --- a/src/dbm/dbm.cc +++ b/src/dbm/dbm.cc @@ -185,8 +185,9 @@ enum tchecker::dbm::status_t tighten(tchecker::dbm::db_t * dbm, tchecker::clock_ for (tchecker::clock_id_t i = 0; i < dim; ++i) { if ((i == k) || (DBM(i, k) == tchecker::dbm::LT_INFINITY)) // optimization continue; - for (tchecker::clock_id_t j = 0; j < dim; ++j) + for (tchecker::clock_id_t j = 0; j < dim; ++j) { DBM(i, j) = tchecker::dbm::min(tchecker::dbm::sum(DBM(i, k), DBM(k, j)), DBM(i, j)); + } if (DBM(i, i) < tchecker::dbm::LE_ZERO) { DBM(0, 0) = tchecker::dbm::LT_ZERO; return tchecker::dbm::EMPTY; @@ -524,12 +525,61 @@ enum tchecker::dbm::status_t intersection(tchecker::dbm::db_t * dbm, tchecker::d return tchecker::dbm::tighten(dbm, dim); } +// used for assertion only +bool split_is_subset_of_R_orig(const tchecker::dbm::db_t * orig_zone, + tchecker::clock_id_t dim, tchecker::dbm::db_t * zone_split, + tchecker::clock_reset_container_t reset) +{ + + tchecker::dbm::db_t r_orig[dim*dim]; + tchecker::dbm::copy(r_orig, orig_zone, dim); + + // resets to zero allowed, only + for(const tchecker::clock_reset_t & r : reset) { + reset_to_value(r_orig, dim, r.left_id() + 1, 0); + } + + assert(tchecker::dbm::is_tight(r_orig, dim)); + assert(tchecker::dbm::is_consistent(r_orig, dim)); + + if(!tchecker::dbm::is_le(zone_split, r_orig, dim)) { + std::cout << __FILE__ << ": " << __LINE__ << ": orig_zone:" << std::endl; + tchecker::dbm::output_matrix(std::cout, orig_zone, dim); + + std::cout << __FILE__ << ": " << __LINE__ << ": zone_split:" << std::endl; + tchecker::dbm::output_matrix(std::cout, orig_zone, dim); + + + std::cout << __FILE__ << ": " << __LINE__ << ": resets:" << std::endl; + + for(const tchecker::clock_reset_t & r : reset) { + std::cout << r << std::endl; + } + + std::cout << __FILE__ << ": " << __LINE__ << ": R(orig_zone):" << std::endl; + tchecker::dbm::output_matrix(std::cout, r_orig, dim); + + return false; + } + + return true; + +} + tchecker::dbm::db_t * revert_multiple_reset(const tchecker::dbm::db_t * orig_zone, tchecker::clock_id_t dim, tchecker::dbm::db_t * zone_split, tchecker::clock_reset_container_t reset) { - // TODO: add assertions + assert(dim >= 1); + assert(orig_zone != nullptr); + assert(zone_split != nullptr); + assert(tchecker::dbm::is_consistent(orig_zone, dim)); + assert(tchecker::dbm::is_consistent(zone_split, dim)); + assert(tchecker::dbm::is_tight(orig_zone, dim)); + assert(tchecker::dbm::is_tight(zone_split, dim)); + + assert(split_is_subset_of_R_orig(orig_zone, dim, zone_split, reset)); if(reset.empty()) { // place the dbm to return at the heap s.t. it is not destroyed during the returns @@ -1264,6 +1314,61 @@ enum tchecker::dbm::clock_position_t clock_position(tchecker::dbm::db_t const * return tchecker::dbm::CLK_SYNCHRONIZABLE; } +enum tchecker::dbm::union_convex_t convex_union(tchecker::dbm::db_t *result, tchecker::dbm::db_t const * dbm1, tchecker::dbm::db_t const * dbm2, tchecker::clock_id_t dim) +{ + assert(result != nullptr); + assert(dbm1 != nullptr); + assert(dbm2 != nullptr); + + assert(dim >= 1); + + assert(tchecker::dbm::is_consistent(dbm1, dim)); + assert(tchecker::dbm::is_tight(dbm1, dim)); + + assert(tchecker::dbm::is_consistent(dbm2, dim)); + assert(tchecker::dbm::is_tight(dbm2, dim)); + + tchecker::dbm::copy(result, dbm1, dim); + + std::vector> dbm1_tight; + std::vector> dbm2_tight; + + for(tchecker::clock_id_t i = 0; i < dim; ++i) { + for(tchecker::clock_id_t j = 0; j < dim; ++j) { + if(DBM1(i, j) < DBM2(i, j) ) { + result[i*dim + j] = DBM2(i, j); + dbm1_tight.emplace_back(std::make_tuple(std::move(i), std::move(j), tchecker::dbm::db_t(DBM1(i, j)))); + } else if (DBM2(i, j) < DBM1(i, j)) { + dbm2_tight.emplace_back(std::make_tuple(std::move(i), std::move(j), tchecker::dbm::db_t(DBM2(i, j)))); + } + } + } + + if(dbm2_tight.empty()) { + return tchecker::dbm::union_convex_t::UNION_IS_CONVEX; + } + + if (dbm1_tight.empty()) { + tchecker::dbm::copy(result, dbm2, dim); + return tchecker::dbm::union_convex_t::UNION_IS_CONVEX; + } + + for(auto iter = dbm1_tight.begin(); iter < dbm1_tight.end(); iter++) { + tchecker::dbm::db_t diff_dbm[dim*dim]; + tchecker::dbm::copy(diff_dbm, result, dim); + diff_dbm[std::get<1>(*iter) * dim + std::get<0>(*iter)] = tchecker::dbm::invert(std::get<2>(*iter)); + tchecker::dbm::tighten(diff_dbm, dim); + for(auto iter2 = dbm2_tight.begin(); iter2 < dbm2_tight.end(); iter2++) { + if(diff_dbm[std::get<0>(*iter2) * dim + std::get<1>(*iter2)] > std::get<2>(*iter2)) { + return tchecker::dbm::union_convex_t::UNION_IS_NOT_CONVEX; + } + } + } + + return tchecker::dbm::union_convex_t::UNION_IS_CONVEX; + +} + } // end of namespace dbm } // end of namespace tchecker diff --git a/src/extrapolation/CMakeLists.txt b/src/extrapolation/CMakeLists.txt index 742822ba..7f40862b 100644 --- a/src/extrapolation/CMakeLists.txt +++ b/src/extrapolation/CMakeLists.txt @@ -7,14 +7,12 @@ ${CMAKE_CURRENT_SOURCE_DIR}/extrapolation.cc ${CMAKE_CURRENT_SOURCE_DIR}/extrapolation_factory.cc ${CMAKE_CURRENT_SOURCE_DIR}/global_lu_extrapolation.cc ${CMAKE_CURRENT_SOURCE_DIR}/global_m_extrapolation.cc -${CMAKE_CURRENT_SOURCE_DIR}/k_norm.cc ${CMAKE_CURRENT_SOURCE_DIR}/local_lu_extrapolation.cc ${CMAKE_CURRENT_SOURCE_DIR}/local_m_extrapolation.cc ${TCHECKER_INCLUDE_DIR}/tchecker/extrapolation/extrapolation.hh ${TCHECKER_INCLUDE_DIR}/tchecker/extrapolation/extrapolation_factory.hh ${TCHECKER_INCLUDE_DIR}/tchecker/extrapolation/global_lu_extrapolation.hh ${TCHECKER_INCLUDE_DIR}/tchecker/extrapolation/global_m_extrapolation.hh -${TCHECKER_INCLUDE_DIR}/tchecker/extrapolation/k_norm.hh ${TCHECKER_INCLUDE_DIR}/tchecker/extrapolation/local_lu_extrapolation.hh ${TCHECKER_INCLUDE_DIR}/tchecker/extrapolation/local_m_extrapolation.hh PARENT_SCOPE) diff --git a/src/extrapolation/extrapolation_factory.cc b/src/extrapolation/extrapolation_factory.cc index 0e46407d..ea0fb46b 100644 --- a/src/extrapolation/extrapolation_factory.cc +++ b/src/extrapolation/extrapolation_factory.cc @@ -16,7 +16,6 @@ #include "tchecker/extrapolation/extrapolation.hh" #include "tchecker/extrapolation/global_lu_extrapolation.hh" #include "tchecker/extrapolation/global_m_extrapolation.hh" -#include "tchecker/extrapolation/k_norm.hh" #include "tchecker/extrapolation/local_lu_extrapolation.hh" #include "tchecker/extrapolation/local_m_extrapolation.hh" @@ -62,8 +61,6 @@ tchecker::zg::extrapolation_t * extrapolation_factory(enum extrapolation_type_t return new tchecker::zg::global_extra_m_plus_t{clock_bounds.global_m_map()}; case tchecker::zg::EXTRA_M_PLUS_LOCAL: return new tchecker::zg::local_extra_m_plus_t{clock_bounds.local_m_map()}; - case tchecker::zg::EXTRA_K_NORM: - return new tchecker::zg::k_norm{clock_bounds.global_lu_map()}; default: throw std::invalid_argument("Unknown zone extrapolation"); } @@ -75,70 +72,51 @@ namespace vcg { tchecker::zg::extrapolation_t * extrapolation_factory( enum tchecker::zg::extrapolation_type_t type, - std::shared_ptr const & orig_system_first, - std::shared_ptr const & orig_system_second, + std::shared_ptr system_first, + std::shared_ptr system_second, bool first_not_second) { - if(tchecker::zg::EXTRA_K_NORM != type) - throw std::invalid_argument("vcg currently supports k normalization only."); - std::vector> bounds; - bounds.push_back(std::vector()); - bounds.push_back(std::vector()); - - for(std::size_t i = 0; i < 2; ++i) { - std::unique_ptr clock_bounds{ - tchecker::clockbounds::compute_clockbounds(0 == i ? *orig_system_first : *orig_system_second)}; - - if (clock_bounds.get() == nullptr) - return nullptr; - - std::shared_ptr lu_map = clock_bounds->global_lu_map(); + if(tchecker::zg::EXTRA_M_GLOBAL != type) { // vcg currently support k norm (m_global) only + throw std::invalid_argument("Unknown zone extrapolation"); + } - // we set the upper and lower clock bound to the same value to receive k-norm. - tchecker::clockbounds::map_t *U = const_cast(&(lu_map->U())); - tchecker::clockbounds::map_t *L = const_cast(& (lu_map->L())); + std::unique_ptr clock_bounds_first{tchecker::clockbounds::compute_clockbounds(*system_first)}; + if (clock_bounds_first.get() == nullptr) + return nullptr; - tchecker::clockbounds::update(*U, *L); + std::unique_ptr clock_bounds_second{tchecker::clockbounds::compute_clockbounds(*system_second)}; + if (clock_bounds_second.get() == nullptr) + return nullptr; - for(tchecker::clock_id_t j = 0; j < clock_bounds->clock_number(); ++j) { - bounds[i].push_back(U[0][j]); - } - } - tchecker::clock_id_t no_of_virtual_clocks = orig_system_first->clocks_count(VK_FLATTENED) + orig_system_second->clocks_count(VK_FLATTENED); - tchecker::clock_id_t no_of_original_clocks = first_not_second ? orig_system_first->clocks_count(VK_FLATTENED) : orig_system_second->clocks_count(VK_FLATTENED); - tchecker::clock_id_t no_of_clocks = no_of_original_clocks + no_of_virtual_clocks; + std::shared_ptr M_first = clock_bounds_first->global_m_map(); + std::shared_ptr M_second = clock_bounds_second->global_m_map(); - std::shared_ptr resulting_clock_bounds = std::make_shared(no_of_clocks); - /* set the bounds */ + tchecker::clock_id_t no_orig_clocks = (first_not_second) ? clock_bounds_first->clocks_number() : clock_bounds_second->clocks_number(); - // original - for(tchecker::clock_id_t i = 0; i < no_of_original_clocks; ++i) { + tchecker::clockbounds::global_m_map_t m_map_with_virt_clks{no_orig_clocks + clock_bounds_first->clocks_number() + clock_bounds_second->clocks_number()}; - tchecker::clockbounds::bound_t bound = first_not_second ? bounds[0][i] : bounds[1][i]; + tchecker::clockbounds::clear(m_map_with_virt_clks.M()); - tchecker::clockbounds::update(resulting_clock_bounds->L(), i, bound); - tchecker::clockbounds::update(resulting_clock_bounds->U(), i, bound); + for(clock_id_t i = 0; i < no_orig_clocks; ++i) { + tchecker::clockbounds::update(m_map_with_virt_clks.M(), i, (first_not_second) ? M_first->M()[i] : M_second->M()[i]); } + for(clock_id_t i = 0; i < clock_bounds_first->clocks_number(); ++i) { + tchecker::clockbounds::update(m_map_with_virt_clks.M(), i + no_orig_clocks, M_first->M()[i]); + } - // first virtual - for(tchecker::clock_id_t i = no_of_original_clocks; i < no_of_original_clocks + orig_system_first->clocks_count(VK_FLATTENED); ++i) { - tchecker::clockbounds::update(resulting_clock_bounds->L(), i, bounds[0][i - no_of_original_clocks]); - tchecker::clockbounds::update(resulting_clock_bounds->U(), i, bounds[0][i - no_of_original_clocks]); + for(clock_id_t i = 0; i < clock_bounds_second->clocks_number(); ++i) { + tchecker::clockbounds::update(m_map_with_virt_clks.M(), i + no_orig_clocks + clock_bounds_first->clocks_number(), M_second->M()[i]); } - // second virtual - tchecker::clock_id_t offset_second_virtual = no_of_original_clocks + orig_system_first->clocks_count(VK_FLATTENED); + //std::cout << __FILE__ << ": " << __LINE__ << ": " << m_map_with_virt_clks << std::endl; - for(tchecker::clock_id_t i = offset_second_virtual; i < no_of_clocks; ++i) { - tchecker::clockbounds::update(resulting_clock_bounds->L(), i, bounds[1][i - offset_second_virtual]); - tchecker::clockbounds::update(resulting_clock_bounds->U(), i, bounds[1][i - offset_second_virtual]); - } + std::shared_ptr final_map = std::make_shared(m_map_with_virt_clks); - return new tchecker::vcg::k_norm_virtual{resulting_clock_bounds}; + return new tchecker::zg::global_extra_m_t{final_map}; } diff --git a/src/extrapolation/k_norm.cc b/src/extrapolation/k_norm.cc deleted file mode 100644 index 4d346c79..00000000 --- a/src/extrapolation/k_norm.cc +++ /dev/null @@ -1,39 +0,0 @@ -/* - * This file is a part of the TChecker project. - * - * See files AUTHORS and LICENSE for copyright details. - * - */ - -#include "tchecker/extrapolation/k_norm.hh" - -namespace tchecker { - -namespace zg { - -k_norm::k_norm( - std::shared_ptr const & clock_bounds) - :tchecker::zg::global_extra_lu_t(clock_bounds) -{ - // k-norm is equivalent to global_extra_lu_t, if we always choose the maximum value of U(i) and L(i) for all checks. - tchecker::clockbounds::map_t *U = const_cast(&(_clock_bounds->U())); - tchecker::clockbounds::map_t *L = const_cast(& (_clock_bounds->L())); - - - tchecker::clockbounds::update(*U, *L); - tchecker::clockbounds::update(*L, *U); -} - -} // end of namespace zg - -namespace vcg { - -k_norm_virtual::k_norm_virtual( - std::shared_ptr const & clock_bounds) - :tchecker::zg::global_extra_lu_t(clock_bounds) -{ -} - -} // end of namespace vcg - -} // end of namespace tchecker diff --git a/src/strong-timed-bisim/stats.cc b/src/strong-timed-bisim/stats.cc index 5fefdcd0..92ab3536 100644 --- a/src/strong-timed-bisim/stats.cc +++ b/src/strong-timed-bisim/stats.cc @@ -13,15 +13,26 @@ namespace tchecker { namespace strong_timed_bisim { -stats_t::stats_t() : _visited_pair_of_states(0), _visited_transitions(0), _deepest_path(0), _relationship_fulfilled(true) {} +stats_t::stats_t() : _visited_pair_of_states(0), _relationship_fulfilled(true) {} -unsigned long stats_t::visited_pair_of_states() const { return _visited_pair_of_states; } +long stats_t::visited_pair_of_states() const +{ + return _visited_pair_of_states; +} -unsigned long stats_t::visited_transitions() const { return _visited_transitions; } +void stats_t::set_visited_pair_of_states(long visited_pair_of_states) +{ + _visited_pair_of_states = visited_pair_of_states; +} -unsigned long stats_t::deepest_path() const { return _deepest_path; } +bool stats_t::relationship_fulfilled() const { + return _relationship_fulfilled; +} -bool stats_t::relationship_fulfilled() const { return _relationship_fulfilled; } +void stats_t::set_relationship_fulfilled(bool relationship_fulfilled) +{ + _relationship_fulfilled = relationship_fulfilled; +} void stats_t::attributes(std::map & m) const { tchecker::algorithms::stats_t::attributes(m); @@ -29,18 +40,10 @@ void stats_t::attributes(std::map & m) const { std::stringstream sstream; sstream << _visited_pair_of_states; - m["VISITED_PAIR_OF_STATES_STATES"] = sstream.str(); - - sstream.str(""); - sstream << _visited_transitions; - m["VISITED_TRANSITIONS"] = sstream.str(); - - sstream.str(""); - sstream << _deepest_path; - m["DEEPEST_PATH"] = sstream.str(); + m["VISITED_PAIR_OF_STATES"] = sstream.str(); sstream.str(""); - sstream << std::boolalpha << _relationship_fulfilled; + sstream << (_relationship_fulfilled ? "true" : "false"); m["RELATIONSHIP_FULFILLED"] = sstream.str(); } diff --git a/src/strong-timed-bisim/virtual_clock_algorithm.cc b/src/strong-timed-bisim/virtual_clock_algorithm.cc index 0c1cdea4..46f54a1e 100644 --- a/src/strong-timed-bisim/virtual_clock_algorithm.cc +++ b/src/strong-timed-bisim/virtual_clock_algorithm.cc @@ -7,23 +7,28 @@ #include "tchecker/strong-timed-bisim/virtual_clock_algorithm.hh" #include "tchecker/vcg/virtual_constraint.hh" +#include "tchecker/vcg/revert_transitions.hh" +#include "tchecker/vcg/sync.hh" +#include "tchecker/dbm/dbm.hh" namespace tchecker { namespace strong_timed_bisim { -Lieb_et_al::Lieb_et_al(std::shared_ptr input_first, std::shared_ptr input_second) : _A(input_first), _B(input_first) {} +Lieb_et_al::Lieb_et_al(std::shared_ptr input_first, std::shared_ptr input_second) + : _A(input_first), _B(input_second), _visited_pair_of_states(0), _delete_me(0) +{ + assert(_A->get_no_of_virtual_clocks() == _B->get_no_of_virtual_clocks()); +} tchecker::strong_timed_bisim::stats_t Lieb_et_al::run() { - std::cout << "run algorithm" << std::endl; +// std::cout << __FILE__ << ": " << __LINE__ << ": no of orig clocks is " << _A->get_no_of_original_clocks() << " and " << _B->get_no_of_original_clocks() << std::endl; +// std::cout << __FILE__ << ": " << __LINE__ << ": no of virt clocks is " << _A->get_no_of_virtual_clocks() << " and " << _B->get_no_of_virtual_clocks() << std::endl; - stats_t stats; -#if 0 - stats.set_start_time(); + tchecker::strong_timed_bisim::stats_t stats; - // sst is a tuple (tchecker::state_status_t, state_t, transition_t) - // state_status_t : see basictypes.hh + stats.set_start_time(); std::vector sst_first; std::vector sst_second; @@ -34,74 +39,432 @@ tchecker::strong_timed_bisim::stats_t Lieb_et_al::run() { if(STATE_OK != std::get<0>(sst_first[0]) || STATE_OK != std::get<0>(sst_second[0])) throw std::runtime_error("problems with initial state"); - std::size_t dim = std::get<1>(sst_first[0])->zone().dim(); - auto dbm = std::get<1>(sst_first[0])->zone().dbm(); + tchecker::zg::const_state_sptr_t const_first{std::get<1>(sst_first[0])}; + tchecker::zg::const_state_sptr_t const_second{std::get<1>(sst_second[0])}; - for(std::size_t i = 0; i < dim; ++i) { - for(std::size_t j = 0; j < dim; ++j) { - std::size_t index = i*dim + j; - std::cout << "(" << dbm[index].cmp << ", " << dbm[index].value << ") "; - } - std::cout << std::endl; - } +// std::cout << __FILE__ << ": " << __LINE__ << ": start algorithm" << std::endl; + + std::unordered_set, custom_hash, custom_equal> empty; + + std::shared_ptr> result + = this->check_for_virt_bisim(const_first, std::get<2>(sst_first[0]), const_second, std::get<2>(sst_second[0]), empty, false); + + stats.set_end_time(); - tchecker::virtual_constraint::virtual_constraint_t *vc = tchecker::virtual_constraint::factory(&(std::get<1>(sst_first[0])->zone()), this->_A->get_no_of_virtual_clocks()); + stats.set_visited_pair_of_states(_visited_pair_of_states); + stats.set_relationship_fulfilled(result->is_empty()); - const clock_constraint_container_t & virt_cons = vc->get_vc(this->_A->clocks_count() - this->_A->get_no_of_virtual_clocks()); + return stats; - for(auto iter = virt_cons.begin(); iter < virt_cons.end(); iter++) { - std::cout << *iter << std::endl; +} + +// used for assertion only +bool check_for_virt_bisim_preconditions_check(tchecker::zg::const_state_sptr_t symb_state, tchecker::zg::transition_sptr_t symb_trans) +{ + + assert(tchecker::dbm::is_consistent(symb_state->zone().dbm(), symb_state->zone().dim())); + assert(tchecker::dbm::is_tight(symb_state->zone().dbm(), symb_state->zone().dim())); + + // we check whether the resets of the zones are matching the resets of the transitions. WARNING: This works for reset to zero only! + for(auto iter = symb_trans->reset_container().begin(); iter < symb_trans->reset_container().end(); iter++) { + + if(!iter->reset_to_zero()) { + std::cerr << __FILE__ << ": " << __LINE__ << ": the reset " << *iter << " is not a reset to zero" << std::endl; + return false; + } + + tchecker::clock_constraint_t orig_min_ref{iter->left_id(), tchecker::REFCLOCK_ID, tchecker::LE, 0}; + tchecker::clock_constraint_t ref_min_orig{tchecker::REFCLOCK_ID, iter->left_id(), tchecker::LE, 0}; + + if(!tchecker::dbm::satisfies(symb_state->zone().dbm(), symb_state->zone().dim(), orig_min_ref)) { + std::cerr << __FILE__ << ": " << __LINE__ << ": the reset " << orig_min_ref << " is not fulfilled by" << std::endl; + std::cerr << __FILE__ << ": " << __LINE__ << ": vloc: "<< symb_state->vloc() << std::endl; + tchecker::dbm::output_matrix(std::cerr, symb_state->zone().dbm(), symb_state->zone().dim()); + return false; + } + + if(!tchecker::dbm::satisfies(symb_state->zone().dbm(), symb_state->zone().dim(), ref_min_orig)) { + std::cerr << __FILE__ << ": " << __LINE__ << ": the reset " << ref_min_orig << " is not fulfilled by" << std::endl; + std::cerr << __FILE__ << ": " << __LINE__ << ": vloc: "<< symb_state->vloc() << std::endl; + tchecker::dbm::output_matrix(std::cerr, symb_state->zone().dbm(), symb_state->zone().dim()); + return false; + } } -/* - for(std::size_t i = 0; i <= input_first->get_no_of_virtual_clocks(); ++i) { - for(std::size_t j = 0; j < input_first->get_no_of_virtual_clocks(); ++j) { - std::size_t index = i*input_first->get_no_of_virtual_clocks() + i + j; - std::cout << "(" << (vc->get_dbm())[index].cmp << ", " << (vc->get_dbm())[index].value << ") "; - } - std::cout << std::endl; + return true; +} + +// used for assertion only +bool all_vc_are_sub_vc_of_phi_a_or_phi_b(tchecker::zone_container_t & lo_vc, + tchecker::zg::const_state_sptr_t first, tchecker::zg::const_state_sptr_t second, tchecker::clock_id_t no_of_virt_clocks) +{ + std::shared_ptr phi_A = tchecker::virtual_constraint::factory(first->zone(), no_of_virt_clocks); + std::shared_ptr phi_B = tchecker::virtual_constraint::factory(second->zone(), no_of_virt_clocks); + bool result = true; + + for(auto iter = lo_vc.begin(); iter < lo_vc.end(); iter++) { + + assert(tchecker::dbm::is_tight((*iter)->dbm(), (*iter)->dim())); + assert(tchecker::dbm::is_consistent((*iter)->dbm(), (*iter)->dim())); + + result &= ((*iter)->dim() == no_of_virt_clocks + 1); + result &= (tchecker::dbm::is_le((*iter)->dbm(), phi_A->dbm(), phi_A->dim()) || tchecker::dbm::is_le((*iter)->dbm(), phi_B->dbm(), phi_B->dim())); + + if(!result) { + std::cout << __FILE__ << ": " << __LINE__ << ": problems with the return of check_for_virt_bisim" << std::endl << "phi_A is " << std::endl; + tchecker::dbm::output_matrix(std::cout, phi_A->dbm(), phi_A->dim()); + + std::cout << __FILE__ << ": " << __LINE__ << ": phi_B is " << std::endl; + tchecker::dbm::output_matrix(std::cout, phi_B->dbm(), phi_B->dim()); + + std::cout << __FILE__ << ": " << __LINE__ << ": returned vc is " << std::endl; + tchecker::dbm::output_matrix(std::cout, (*iter)->dbm(), (*iter)->dim()); + return result; + } } -*/ - delete vc; + return result; +} - stats.set_end_time(); -#endif - return stats; +// used for assertion only +bool is_phi_subset_of_a_zone(const tchecker::dbm::db_t *dbm, tchecker::clock_id_t dim, tchecker::clock_id_t no_of_virt_clocks, + const tchecker::virtual_constraint::virtual_constraint_t & phi_e) +{ + std::shared_ptr phi = tchecker::virtual_constraint::factory(dbm, dim, no_of_virt_clocks); + return tchecker::dbm::is_le(phi_e.dbm(), phi->dbm(), phi_e.dim()); } std::shared_ptr> -Lieb_et_al::check_for_outgoing_transitions( tchecker::zg::const_state_sptr_t symb_state_first, - std::shared_ptr vcg_first, - tchecker::zg::const_state_sptr_t symb_state_second, - std::shared_ptr vcg_second, - std::shared_ptr> - (*func)(tchecker::zg::state_sptr_t, tchecker::zg::state_sptr_t)) +Lieb_et_al::check_for_virt_bisim(tchecker::zg::const_state_sptr_t symb_state_first, tchecker::zg::transition_sptr_t symb_trans_first, + tchecker::zg::const_state_sptr_t symb_state_second, tchecker::zg::transition_sptr_t symb_trans_second, + std::unordered_set, custom_hash, custom_equal> & visited, + bool last_was_epsilon) { - std::vector v_first; - vcg_first->next(symb_state_first, v_first); + if(!last_was_epsilon) { + assert(check_for_virt_bisim_preconditions_check(symb_state_first, symb_trans_first)); + assert(check_for_virt_bisim_preconditions_check(symb_state_second, symb_trans_second)); + } + + _visited_pair_of_states++; + + //std::cout << __FILE__ << ": " << __LINE__ << ": _visited_pair_of_states: " << _visited_pair_of_states << std::endl; + //std::cout << __FILE__ << ": " << __LINE__ << ": check-for-virt-bisim" << std::endl; + //std::cout << __FILE__ << ": " << __LINE__ << ": " << symb_state_first->vloc() << std::endl; + //tchecker::dbm::output_matrix(std::cout, symb_state_first->zone().dbm(), symb_state_first->zone().dim()); + + //std::cout << __FILE__ << ": " << __LINE__ << ": " << symb_state_second->vloc() << std::endl; + //tchecker::dbm::output_matrix(std::cout, symb_state_second->zone().dbm(), symb_state_second->zone().dim()); std::shared_ptr> result - = std::make_shared>(vcg_first->get_no_of_virtual_clocks()); + = std::make_shared>(_A->get_no_of_virtual_clocks() + 1); + + std::shared_ptr phi_A = tchecker::virtual_constraint::factory(symb_state_first->zone(), _A->get_no_of_virtual_clocks()); + std::shared_ptr phi_B = tchecker::virtual_constraint::factory(symb_state_second->zone(), _A->get_no_of_virtual_clocks()); + + tchecker::zg::state_sptr_t A_synced = _A->clone_state(symb_state_first); + tchecker::zg::state_sptr_t B_synced = _B->clone_state(symb_state_second); + + // Before we sync them, we have to ensure virtual equivalence + if( + tchecker::dbm::status_t::EMPTY == phi_B->logic_and(A_synced->zone(), symb_state_first->zone()) || + tchecker::dbm::status_t::EMPTY == phi_A->logic_and(B_synced->zone(), symb_state_second->zone()) + ) + { + // this is a difference to the original function, done for efficiency reasons. + result->append_zone(phi_A); + result->append_zone(phi_B); + assert(all_vc_are_sub_vc_of_phi_a_or_phi_b(*result, symb_state_first, symb_state_second, _A->get_no_of_virtual_clocks())); + _delete_me++; + //std::cout << __FILE__ << ": " << __LINE__ << ": _delete_me: " << _delete_me << std::endl; + result->compress(); + return result; + } + + //std::cout << __FILE__ << ": " << __LINE__ << ": " << "virt_equiv A:" << std::endl; + //tchecker::dbm::output_matrix(std::cout, A_synced->zone().dbm(), A_synced->zone().dim()); + //std::cout << __FILE__ << ": " << __LINE__ << ": " << "virt_equiv B:" << std::endl; + //tchecker::dbm::output_matrix(std::cout, B_synced->zone().dbm(), B_synced->zone().dim()); + + std::shared_ptr> to_append_A + = std::make_shared>(_A->get_no_of_virtual_clocks() + 1); + std::shared_ptr> to_append_B + = std::make_shared>(_B->get_no_of_virtual_clocks() + 1); + + phi_B->neg_logic_and(to_append_A, *phi_A); + phi_A->neg_logic_and(to_append_B, *phi_B); + + result->append_container(to_append_A); + result->append_container(to_append_B); + + assert(all_vc_are_sub_vc_of_phi_a_or_phi_b(*result, symb_state_first, symb_state_second, _A->get_no_of_virtual_clocks())); - for (auto && [status_first, s_first, t_first] : v_first) { + // now we can sync them. As we know: the targets of delay transitions are already synced! + if(!last_was_epsilon) { + tchecker::vcg::sync( A_synced->zone_ptr()->dbm(), B_synced->zone_ptr()->dbm(), + A_synced->zone_ptr()->dim(), B_synced->zone_ptr()->dim(), + _A->get_no_of_original_clocks(), _B->get_no_of_original_clocks(), + symb_trans_first->reset_container(), symb_trans_second->reset_container()); - std::shared_ptr> lo_result; + //std::cout << __FILE__ << ": " << __LINE__ << ": " << "synced A:" << std::endl; + //tchecker::dbm::output_matrix(std::cout, A_synced->zone().dbm(), A_synced->zone().dim()); + //std::cout << __FILE__ << ": " << __LINE__ << ": " << "synced B:" << std::endl; + //tchecker::dbm::output_matrix(std::cout, B_synced->zone().dbm(), B_synced->zone().dim()); + } + + assert(tchecker::vcg::are_dbm_synced(A_synced->zone_ptr()->dbm(), B_synced->zone_ptr()->dbm(), + A_synced->zone_ptr()->dim(), B_synced->zone_ptr()->dim(), + _A->get_no_of_original_clocks(), _B->get_no_of_original_clocks())); + + // normalizing, checking whether we have already seen this pair. + tchecker::zg::state_sptr_t A_normed = _A->clone_state(A_synced); + tchecker::zg::state_sptr_t B_normed = _B->clone_state(B_synced); + + _A->run_extrapolation(A_normed->zone().dbm(), A_normed->zone().dim(), *(A_normed->vloc_ptr())); + _B->run_extrapolation(B_normed->zone().dbm(), B_normed->zone().dim(), *(B_normed->vloc_ptr())); + + std::pair normalized_pair{A_normed, B_normed}; + + if(visited.count(normalized_pair)) { + assert(all_vc_are_sub_vc_of_phi_a_or_phi_b(*result, symb_state_first, symb_state_second, _A->get_no_of_virtual_clocks())); + _delete_me++; + //std::cout << __FILE__ << ": " << __LINE__ << ": _delete_me: " << _delete_me << std::endl; + result->compress(); + return result; + } + + // If we haven't seen this pair, yet, add it to visited + visited.insert(normalized_pair); + + std::shared_ptr> lo_not_simulatable + = std::make_shared>(_A->get_no_of_virtual_clocks() + 1); - std::vector v_second; - vcg_second->next(symb_state_second, v_second); + if(!last_was_epsilon) { + // we check the outgoing epsilon transition + tchecker::zg::state_sptr_t A_epsilon = _A->clone_state(A_normed); + tchecker::zg::state_sptr_t B_epsilon = _B->clone_state(B_normed); + + _A->semantics()->delay(A_epsilon->zone_ptr()->dbm(), A_epsilon->zone_ptr()->dim(), symb_trans_first->tgt_invariant_container()); + _B->semantics()->delay(B_epsilon->zone_ptr()->dbm(), B_epsilon->zone_ptr()->dim(), symb_trans_second->tgt_invariant_container()); + + tchecker::zg::const_state_sptr_t const_A_epsilon{A_epsilon}; + tchecker::zg::const_state_sptr_t const_B_epsilon{B_epsilon}; + + std::shared_ptr> result_epsilon + = check_for_virt_bisim(const_A_epsilon, symb_trans_first, const_B_epsilon, symb_trans_second, visited, true); + + // now, we calculate the problematic virtual constraints by using the revert-epsilon function and adding it to lo_not_simulatable + + for(auto iter = result_epsilon->begin(); iter < result_epsilon->end(); iter++) { + lo_not_simulatable->append_zone(tchecker::vcg::revert_epsilon_trans(A_normed->zone(), **iter)); + } + + } + else { - for (auto && [status_second, s_second, t_second] : v_first) { + tchecker::zg::const_state_sptr_t const_A_normed{A_normed}; + tchecker::zg::const_state_sptr_t const_B_normed{B_normed}; - if(t_first->vedge().event_equal(vcg_first->system(), t_second->vedge(), vcg_second->system())) { - std::shared_ptr> inter = func(s_first, s_second); + // now that we have checked the epsilon transition, we check the outgoing action transitions + lo_not_simulatable->append_container(check_for_outgoing_transitions(const_A_normed, const_B_normed, visited)); + } + + lo_not_simulatable->compress(); + + // now we have to revert the extrapolation + + std::shared_ptr> reverted_extrapolation + = std::make_shared>(_A->get_no_of_virtual_clocks() + 1); + + std::shared_ptr phi_synced = tchecker::virtual_constraint::factory(A_synced->zone(), _A->get_no_of_virtual_clocks()); // vc of A_synced and B_synced are the same + + for(auto iter = lo_not_simulatable->begin(); iter < lo_not_simulatable->end(); iter++) { + std::shared_ptr to_Add = tchecker::virtual_constraint::factory(_A->get_no_of_virtual_clocks()); + if(tchecker::dbm::NON_EMPTY == tchecker::dbm::intersection(to_Add->dbm(), (*iter)->dbm(), phi_synced->dbm(), _A->get_no_of_virtual_clocks() + 1)) { + reverted_extrapolation->append_zone(to_Add); + } + } + + reverted_extrapolation->compress(); + + // finally, we revert the sync + + std::shared_ptr another_phi_A = tchecker::virtual_constraint::factory(symb_state_first->zone(), _A->get_no_of_virtual_clocks()); + std::shared_ptr another_phi_B = tchecker::virtual_constraint::factory(symb_state_second->zone(), _B->get_no_of_virtual_clocks()); + + tchecker::zg::state_sptr_t A_clone = _A->clone_state(symb_state_first); + tchecker::zg::state_sptr_t B_clone = _B->clone_state(symb_state_second); + + another_phi_A->logic_and(B_clone->zone(), symb_state_second->zone()); + another_phi_B->logic_and(A_clone->zone(), symb_state_first->zone()); + + tchecker::zone_container_t inter{_A->get_no_of_virtual_clocks() + 1}; + + for(auto iter = reverted_extrapolation->begin(); iter < reverted_extrapolation->end(); iter++) { + std::pair, std::shared_ptr> sync_reverted + = tchecker::vcg::revert_sync(A_clone->zone_ptr()->dbm(), B_clone->zone_ptr()->dbm(), A_clone->zone_ptr()->dim(), B_clone->zone_ptr()->dim(), + _A->get_no_of_original_clocks(), _B->get_no_of_original_clocks(), + **iter); + inter.append_zone(sync_reverted.first); + inter.append_zone(sync_reverted.second); + + assert(is_phi_subset_of_a_zone(symb_state_first->zone().dbm(), symb_state_first->zone().dim(), _A->get_no_of_virtual_clocks(), *(sync_reverted.first))); + assert(is_phi_subset_of_a_zone(symb_state_second->zone().dbm(), symb_state_second->zone().dim(), _B->get_no_of_virtual_clocks(), *(sync_reverted.second))); + } + + inter.compress(); + + assert(all_vc_are_sub_vc_of_phi_a_or_phi_b(inter, symb_state_first, symb_state_second, _A->get_no_of_virtual_clocks())); + + result->append_container(tchecker::virtual_constraint::combine(inter, _A->get_no_of_virtual_clocks())); + + assert(all_vc_are_sub_vc_of_phi_a_or_phi_b(*result, symb_state_first, symb_state_second, _A->get_no_of_virtual_clocks())); + + _delete_me++; + //std::cout << __FILE__ << ": " << __LINE__ << ": _delete_me: " << _delete_me << std::endl; + + result->compress(); + + return result; +} + + +std::shared_ptr> +Lieb_et_al::check_for_outgoing_transitions( tchecker::zg::const_state_sptr_t A_state, + tchecker::zg::const_state_sptr_t B_state, + std::unordered_set, custom_hash, custom_equal> & visited) +{ + + std::shared_ptr> result + = std::make_shared>(_A->get_no_of_virtual_clocks() + 1); + + std::vector v_first, v_second; + _A->next(A_state, v_first); + _B->next(B_state, v_second); + + // vector of pointer to zone_container to store the return values regarding an outgoing transition + typedef std::vector>> return_values; + + // vector with an entry for each outgoing transition. For each outgoing trans, a vector of zone container is stored + typedef std::vector lo_return_values; + + lo_return_values A_return_values; + + lo_return_values B_return_values; + + + std::tuple *, lo_return_values *, tchecker::zg::const_state_sptr_t *> A_v_ret_val_pair + = std::make_tuple *, lo_return_values *, tchecker::zg::const_state_sptr_t *>(&v_first, &A_return_values, &A_state); + + std::tuple *, lo_return_values *, tchecker::zg::const_state_sptr_t *> B_v_ret_val_pair + = std::make_tuple *, lo_return_values *, tchecker::zg::const_state_sptr_t *>(&v_second, &B_return_values, &B_state); + + auto together = {&A_v_ret_val_pair, &B_v_ret_val_pair}; + + // init the return values of each outgoing transition. + // for A and B + for(auto iter : together) { + auto ret_val = std::get<1>(*iter); + // and for each outgoing transition + for(auto && [status, s, t] : *(std::get<0>(*iter))) { + // create a zone container + tchecker::zone_container_t tmp{_A->get_no_of_virtual_clocks() + 1}; + // that contains the target vc only + tmp.append_zone(tchecker::virtual_constraint::factory(s->zone(), _A->get_no_of_virtual_clocks())); + // add it to the vector of returned results + return_values init_returned_values; + init_returned_values.emplace_back(std::make_shared>(tmp)); + // and place it at the return values vector + ret_val->emplace_back(init_returned_values); + } + } + + assert(A_return_values.size() == v_first.size()); + assert(B_return_values.size() == v_second.size()); + + for (long unsigned int i = 0; i < v_first.size(); ++i) { + + auto && [status_first, s_first, t_first] = v_first[i]; + tchecker::zg::const_state_sptr_t const_s_first{s_first}; + + for(long unsigned int j = 0; j < v_second.size(); ++j) { + auto && [status_second, s_second, t_second] = v_second[j]; + // the action has to be the same + if(!t_first->vedge().event_equal(_A->system(), t_second->vedge(), _B->system())) { + continue; + } + + tchecker::zg::const_state_sptr_t const_s_second{s_second}; + std::unordered_set, custom_hash, custom_equal> copy(visited); + + std::shared_ptr> inter + = this->check_for_virt_bisim(const_s_first, t_first, const_s_second, t_second, copy, false); + + auto A_s_ret_val_idx = std::make_tuple >*, + lo_return_values *, + long unsigned int *>(&s_first, &A_return_values, &i); + + + auto B_s_ret_val_idx = std::make_tuple >*, + lo_return_values *, + long unsigned int *>(&s_second, &B_return_values, &j); + + auto s_ret_val_idx_together = {&A_s_ret_val_idx, &B_s_ret_val_idx}; + + for(auto iter : s_ret_val_idx_together) { + auto s_cur = *(std::get<0>(*iter)); + auto ret_val_cur = std::get<1>(*iter); + auto index_cur = std::get<2>(*iter); + tchecker::zone_container_t to_add{_A->get_no_of_virtual_clocks() + 1}; for(auto iter = inter->begin(); iter < inter->end(); iter++) { - // TODO + std::shared_ptr tmp = tchecker::zg::factory(s_cur->zone().dim()); + if(tchecker::dbm::status_t::NON_EMPTY == (*iter)->logic_and(tmp, s_cur->zone())) { + to_add.append_zone(tchecker::virtual_constraint::factory(tmp, _A->get_no_of_virtual_clocks())); + } } + to_add.compress(); + (*ret_val_cur)[*index_cur].emplace_back(std::make_shared>(to_add)); } + } + } + + //std::cout << __FILE__ << ": " << __LINE__ << ": start revert_action_trans" << std::endl; + for(auto iter : together) { + auto v_cur = std::get<0>(*iter); + auto ret_val = std::get<1>(*iter); + for (long unsigned int i = 0; i < v_cur->size(); ++i) { + auto && [status_cur, s_cur, t_cur] = (*v_cur)[i]; + std::shared_ptr> in_all = + tchecker::virtual_constraint::contained_in_all( std::ref((*ret_val)[i]), _A->get_no_of_virtual_clocks()); + + for(auto iter_in_all = in_all->begin(); iter_in_all < in_all->end(); iter_in_all++) { + if(!((*iter_in_all)->is_empty())) { + assert(is_phi_subset_of_a_zone(s_cur->zone().dbm(), s_cur->zone().dim(), (*iter_in_all)->get_no_of_virt_clocks(), **iter_in_all)); + result->append_zone(tchecker::vcg::revert_action_trans((*(std::get<2>(*iter)))->zone(), t_cur->guard_container(), t_cur->reset_container(), t_cur->tgt_invariant_container(), **iter_in_all)); + } + } } + } + + //std::cout << __FILE__ << ": " << __LINE__ << ": end revert_action_trans" << std::endl; + + assert( + std::all_of(result->begin(), result->end(), + [A_state, B_state](std::shared_ptr vc) + { + return (is_phi_subset_of_a_zone(A_state->zone().dbm(), A_state->zone().dim(), vc->get_no_of_virt_clocks(), *vc)) || + (is_phi_subset_of_a_zone(B_state->zone().dbm(), B_state->zone().dim(), vc->get_no_of_virt_clocks(), *vc)); + } + ) + ); + + result->compress(); + + //std::cout << __FILE__ << ": " << __LINE__ << ": return from check-outgoing-trans" << std::endl; + + return result; + } } // end of namespace strong_timed_bisim diff --git a/src/tck-compare/tck-compare.cc b/src/tck-compare/tck-compare.cc index b9d2436b..606a7d72 100644 --- a/src/tck-compare/tck-compare.cc +++ b/src/tck-compare/tck-compare.cc @@ -123,9 +123,9 @@ int parse_command_line(int argc, char * argv[]) of errors \post all errors have been reported to std::cerr */ -tchecker::parsing::system_declaration_t * load_system_declaration(std::string const & filename) +std::shared_ptr load_system_declaration(std::string const & filename) { - tchecker::parsing::system_declaration_t * sysdecl = nullptr; + std::shared_ptr sysdecl = nullptr; try { sysdecl = tchecker::parsing::parse_system_declaration(filename); if (sysdecl == nullptr) @@ -147,12 +147,8 @@ tchecker::parsing::system_declaration_t * load_system_declaration(std::string co void strong_timed_bisim(std::shared_ptr const & sysdecl_first, std::shared_ptr const & sysdecl_second) { - std::cout << "tck-compare.cc: run" << std::endl; - auto stats = tchecker::tck_compare::vcg_timed_bisim::run(sysdecl_first, sysdecl_second, os, block_size, table_size); - std::cerr << "tck-compare.cc : print stats" << std::endl; - // stats std::map m; stats.attributes(m); diff --git a/src/tck-compare/vcg-timed-bisim.cc b/src/tck-compare/vcg-timed-bisim.cc index 41bb624c..155ea782 100644 --- a/src/tck-compare/vcg-timed-bisim.cc +++ b/src/tck-compare/vcg-timed-bisim.cc @@ -73,8 +73,6 @@ run(std::shared_ptr const & sysdecl_fir std::vector> systems; - std::cout << "vcg-timed-bisim.cc : run" << std::endl; - for(size_t i = 0; i < 2; ++i) { std::shared_ptr cur_system{new tchecker::ta::system_t{ (i == 0) ? *sysdecl_first : *sysdecl_second}}; std::shared_ptr system_syncprod = std::make_shared(cur_system->as_syncprod_system()); @@ -90,99 +88,16 @@ run(std::shared_ptr const & sysdecl_fir for(size_t i = 0; i < 2; ++i) { std::shared_ptr extended_system{new tchecker::strong_timed_bisim::system_virtual_clocks_t{*(systems[i]), no_of_virt_clocks, 0 == i}}; std::shared_ptr vcg{tchecker::vcg::factory(extended_system, 0 == i, systems[0], systems[1], tchecker::ts::SHARING, tchecker::zg::DISTINGUISHED_SEMANTICS, - tchecker::zg::EXTRA_K_NORM, block_size, table_size)}; + tchecker::zg::EXTRA_M_GLOBAL, block_size, table_size)}; vcgs.push_back(vcg); } - std::cout << "vcg-timed-bisim.cc : created vcgs" << std::endl; +// std::cout << __FILE__ << ": " << __LINE__ << ": created vcgs" << std::endl; auto algorithm = new tchecker::strong_timed_bisim::Lieb_et_al(vcgs[0], vcgs[1]); return algorithm->run(); - - /* DELETE ME! - - std::cout << "no. of processes: " << system_first->processes_count() << std::endl; - std::cout << "no. of processes of product: " << product_first->processes_count() << std::endl; - - auto r = system_first->attributes().range(); - auto begin = r.begin(), end = r.end(); - - std::cout << "loop system attributes" << std::endl; - - for(auto it = begin; it != end; ++it) { - std::cout << "found attribute: " << (*it).key() << ":" << (*it).value() << std::endl; - } - - auto p = product_first->attributes().range(); - auto pbegin = p.begin(), pend = p.end(); - - std::cout << "loop product attributes" << std::endl; - - for(auto it = pbegin; it != pend; ++it) { - std::cout << "found attribute: " << (*it).key() << ":" << (*it).value() << std::endl; - } - - auto r_l = system_first->locations(); - auto begin_l = r_l.begin(), end_l = r_l.end(); - - std::cout << "loop system locations" << std::endl; - - for(auto it = begin_l; it != end_l; ++it) { - std::cout << "found location: " << (*it)->name() << std::endl; - } - - auto p_l = product_first->locations(); - auto begin_p_l = p_l.begin(), end_p_l = p_l.end(); - - std::cout << "loop product locations" << std::endl; - - for(auto it = begin_p_l; it != end_p_l; ++it) { - std::cout << "found location: " << (*it)->name() << std::endl; - } - - std::cout << "initial system locations" << std::endl; - - for(std::size_t i = 0; i < system_first->processes_count(); ++i) { - auto r_init = system_first->initial_locations(i); - auto begin_init = r_init.begin(), end_init = r_init.end(); - - for(auto it = begin_init; it != end_init; ++it) { - std::cout << "found initial location for process " << i << "(" << system_first->process_name(i) << "): " << (*it)->name() << std::endl; - } - } - - std::cout << "initial product locations" << std::endl; - - auto p_init = product_first->initial_locations(0); - auto begin_init = p_init.begin(), end_init = p_init.end(); - - for(auto it = begin_init; it != end_init; ++it) { - std::cout << "found initial location for process " << 0 << "(" << product_first->process_name(0) << "): " << (*it)->name() << std::endl; - } - - auto r_c = system_first->clock_variables().identifiers(); - auto begin_c = r_c.begin(), end_c = r_c.end(); - - std::cout << "loop system clocks" << std::endl; - - for(auto it = begin_c; it != end_c; ++it) { - std::cout << "found clock: " << it << ": " << system_first->clock_name(it) << std::endl; - } - - auto p_c = product_first->clock_variables().identifiers(); - auto begin_p_c = p_c.begin(), end_p_c = p_c.end(); - - std::cout << "loop product clocks" << std::endl; - - for(auto it = begin_p_c; it != end_p_c; ++it) { - std::cout << "found clock: " << it << ": " << product_first->clock_name(it) << std::endl; - } - - - /* UNTIL ME! */ - } } // end of namespace vcg_timed_bisim diff --git a/src/utils/zone_container.cc b/src/utils/zone_container.cc index 8de343a8..0f0bb541 100644 --- a/src/utils/zone_container.cc +++ b/src/utils/zone_container.cc @@ -9,39 +9,6 @@ namespace tchecker { -zone_container_t contained_in_all(std::vector> & zones, tchecker::clock_id_t dim) -{ - - if (zones.empty()) { - zone_container_t result(dim); - return result; - } - - if (1 == zones.size()) { - return zones[0]; - } - - zone_container_t cur = zones.back(); - zones.pop_back(); - - zone_container_t inter = contained_in_all(zones, dim); - - zone_container_t result{dim}; - - for(auto iter_cur = cur.begin(); iter_cur < cur.end(); iter_cur++) { - for(auto iter_inter = inter.begin(); iter_inter < inter.end(); iter_inter++) { - std::shared_ptr tmp = tchecker::zg::factory(dim); - if(tchecker::dbm::NON_EMPTY == tchecker::dbm::intersection(tmp->dbm(), (**iter_cur).dbm(), (**iter_inter).dbm(), (**iter_cur).dim())) { - result.append_zone(tmp); - } - else { - tchecker::zg::zone_t::destruct(&(*tmp)); - } - } - } - return result; -} - // specializations template<> std::shared_ptr zone_container_t::create_element() @@ -58,7 +25,7 @@ std::shared_ptr zone_container_t::cr template<> std::shared_ptr zone_container_t::create_element() { - return tchecker::virtual_constraint::factory(_dim); + return tchecker::virtual_constraint::factory(_dim - 1); } template<> diff --git a/src/vcg/revert_transitions.cc b/src/vcg/revert_transitions.cc index aec1d7b6..bc6bbc7e 100644 --- a/src/vcg/revert_transitions.cc +++ b/src/vcg/revert_transitions.cc @@ -7,6 +7,53 @@ #include "tchecker/vcg/revert_transitions.hh" + +namespace tchecker { + +namespace vcg { + +bool check_whether_phi_is_subset_of_target( + const tchecker::zg::zone_t & zone, + const tchecker::clock_constraint_container_t & guard, + const tchecker::clock_reset_container_t & reset, + const tchecker::clock_constraint_container_t & tgt_invariant, + const tchecker::virtual_constraint::virtual_constraint_t & phi_split) +{ + tchecker::dbm::db_t target_dbm[zone.dim()*zone.dim()]; + zone.to_dbm(target_dbm); + + tchecker::dbm::constrain(target_dbm, zone.dim(), guard); + + if(!tchecker::dbm::is_tight(target_dbm, zone.dim())) { + std::cerr << __FILE__ << ": " << __LINE__ << ": target_dbm is not tight" << std::endl; + return false; + } + + if(!tchecker::dbm::is_consistent(target_dbm, zone.dim())) { + std::cerr << __FILE__ << ": " << __LINE__ << ": target_dbm is not consistent" << std::endl; + return false; + } + + tchecker::dbm::reset(target_dbm, zone.dim(), reset); + tchecker::dbm::constrain(target_dbm, zone.dim(), tgt_invariant); + + if(!tchecker::dbm::is_tight(target_dbm, zone.dim())) { + std::cerr << __FILE__ << ": " << __LINE__ << ": target_dbm is not tight" << std::endl; + return false; + } + + if(!tchecker::dbm::is_consistent(target_dbm, zone.dim())) { + std::cerr << __FILE__ << ": " << __LINE__ << ": target_dbm is not consistent" << std::endl; + return false; + } + + std::shared_ptr target_vc + = tchecker::virtual_constraint::factory(target_dbm, zone.dim(), phi_split.get_no_of_virt_clocks()); + + return tchecker::dbm::is_le(phi_split.dbm(), target_vc->dbm(), target_vc->dim()); + +} + std::shared_ptr revert_action_trans(const tchecker::zg::zone_t & zone, const tchecker::clock_constraint_container_t & guard, @@ -14,39 +61,59 @@ revert_action_trans(const tchecker::zg::zone_t & zone, const tchecker::clock_constraint_container_t & tgt_invariant, const tchecker::virtual_constraint::virtual_constraint_t & phi_split) { + assert(!zone.is_empty()); + assert(!phi_split.is_empty()); - tchecker::clock_reset_container_t reset_copy; + assert(tchecker::dbm::is_tight(zone.dbm(), zone.dim())); + assert(tchecker::dbm::is_consistent(zone.dbm(), zone.dim())); - reset_copy.reserve(reset.size()); + assert(tchecker::dbm::is_tight(phi_split.dbm(), phi_split.dim())); + assert(tchecker::dbm::is_consistent(phi_split.dbm(), phi_split.dim())); - std::copy(reset.begin(), reset.end(), reset_copy.begin()); - - tchecker::dbm::db_t zone_clone[zone.dim()*zone.dim()]; - zone.to_dbm(zone_clone); + assert(check_whether_phi_is_subset_of_target(zone, guard, reset, tgt_invariant, phi_split)); + // copy the reset container since revert_multiple_reset will change it + tchecker::clock_reset_container_t reset_copy(reset); + // According to the implementation of revert-action-trans, described in Lieb et al., we first have to calculate R(zone && g). tchecker::dbm::db_t d_land_g[zone.dim()*zone.dim()]; zone.to_dbm(d_land_g); - tchecker::dbm::constrain(d_land_g, zone.dim(), guard); + assert(tchecker::dbm::is_tight(d_land_g, zone.dim())); + assert(tchecker::dbm::is_consistent(d_land_g, zone.dim())); + tchecker::dbm::constrain(d_land_g, zone.dim(), guard); tchecker::dbm::db_t r_d_land_g_land_phi[zone.dim()*zone.dim()]; tchecker::dbm::copy(r_d_land_g_land_phi, d_land_g, zone.dim()); tchecker::dbm::reset(r_d_land_g_land_phi, zone.dim(), reset); - tchecker::dbm::constrain(r_d_land_g_land_phi, zone.dim(), phi_split.get_vc(zone.dim() - phi_split.dim())); + + assert(tchecker::dbm::is_tight(r_d_land_g_land_phi, zone.dim())); + assert(tchecker::dbm::is_consistent(r_d_land_g_land_phi, zone.dim())); + + // now we have calculated R(zone && g) and we have to land this with the given virtual constrain + tchecker::dbm::constrain(r_d_land_g_land_phi, zone.dim(), phi_split.get_vc(zone.dim() - phi_split.dim(), true)); + + assert(tchecker::dbm::is_tight(r_d_land_g_land_phi, zone.dim())); + assert(tchecker::dbm::is_consistent(r_d_land_g_land_phi, zone.dim())); tchecker::dbm::db_t *reverted = tchecker::dbm::revert_multiple_reset(d_land_g, zone.dim(), r_d_land_g_land_phi, reset_copy); std::shared_ptr virt_mult_reset = tchecker::virtual_constraint::factory(reverted, zone.dim(), phi_split.get_no_of_virt_clocks()); - tchecker::dbm::constrain(zone_clone, zone.dim(), virt_mult_reset->get_vc(zone.dim() - phi_split.dim())); + + tchecker::dbm::db_t zone_clone[zone.dim()*zone.dim()]; + zone.to_dbm(zone_clone); + + tchecker::dbm::constrain(zone_clone, zone.dim(), virt_mult_reset->get_vc(zone.dim() - phi_split.dim(), true)); std::shared_ptr result = tchecker::virtual_constraint::factory(zone_clone, zone.dim(), phi_split.get_no_of_virt_clocks()); + //std::cout << __FILE__ << ": " << __LINE__ << ": return from revert_action_trans" << std::endl; + return result; } @@ -60,14 +127,15 @@ revert_epsilon_trans(const tchecker::zg::zone_t & zone, const tchecker::virtual_ std::shared_ptr zone_copy = tchecker::zg::factory(zone); - tchecker::dbm::constrain(zone_copy->dbm(), zone_copy->dim(), phi_copy->get_vc(zone_copy->dim() - phi_copy->dim())); + tchecker::dbm::constrain(zone_copy->dbm(), zone_copy->dim(), phi_copy->get_vc(zone_copy->dim() - phi_copy->dim(), true)); std::shared_ptr result = tchecker::virtual_constraint::factory(zone_copy, phi_split.get_no_of_virt_clocks()); - tchecker::zg::zone_destruct_and_deallocate(&(*phi_copy)); - tchecker::zg::zone_destruct_and_deallocate(&(*phi_copy)); - return result; } +} // end of namespace vcg + +} // end of namespace tchecker + diff --git a/src/vcg/sync.cc b/src/vcg/sync.cc index eeb8fa4b..cbdf5727 100644 --- a/src/vcg/sync.cc +++ b/src/vcg/sync.cc @@ -6,18 +6,103 @@ */ #include "tchecker/vcg/sync.hh" -#include "tchecker/dbm/dbm.hh" +namespace tchecker { -void sync(tchecker::dbm::db_t *dbm1, tchecker::dbm::db_t *dbm2, tchecker::clock_id_t dim, - tchecker::clock_id_t lowest_virt_clk_id, tchecker::clock_id_t no_of_orig_clocks_1, +namespace vcg { + +bool is_virtually_equivalent(tchecker::dbm::db_t *dbm1, tchecker::dbm::db_t *dbm2, + tchecker::clock_id_t dim1, tchecker::clock_id_t dim2, + tchecker::clock_id_t no_of_orig_clocks_1, tchecker::clock_id_t no_of_orig_clocks_2) +{ + std::shared_ptr vc1 + = tchecker::virtual_constraint::factory(dbm1, dim1, dim1 - no_of_orig_clocks_1 - 1); + + std::shared_ptr vc2 + = tchecker::virtual_constraint::factory(dbm2, dim2, dim2 - no_of_orig_clocks_2 - 1); + + return (*vc1 == *vc2); +} + + +bool are_dbm_synced(tchecker::dbm::db_t *dbm1, tchecker::dbm::db_t *dbm2, + tchecker::clock_id_t dim1, tchecker::clock_id_t dim2, + tchecker::clock_id_t no_of_orig_clocks_1, tchecker::clock_id_t no_of_orig_clocks_2) +{ + + assert(dbm1 != nullptr); + assert(dbm2 != nullptr); + + assert(dim1 >= 1); + assert(dim2 >= 1); + + assert(tchecker::dbm::is_consistent(dbm1, dim1)); + assert(tchecker::dbm::is_consistent(dbm2, dim2)); + assert(tchecker::dbm::is_tight(dbm1, dim1)); + assert(tchecker::dbm::is_tight(dbm2, dim2)); + + assert(no_of_orig_clocks_1 >= 1); + assert(no_of_orig_clocks_2 >= 1); + + assert(dim1 == no_of_orig_clocks_1 + no_of_orig_clocks_1 + no_of_orig_clocks_2 + 1); + assert(dim2 == no_of_orig_clocks_1 + no_of_orig_clocks_2 + no_of_orig_clocks_2 + 1); + + bool result = is_virtually_equivalent(dbm1, dbm2, dim1, dim2, no_of_orig_clocks_1, no_of_orig_clocks_2); + + if(!result) { + std::cout << __FILE__ << ": " << __LINE__ << ": the dbm are not virtually equivalent." << std::endl; + tchecker::dbm::output_matrix(std::cout, dbm1, dim1); + tchecker::dbm::output_matrix(std::cout, dbm2, dim2); + return result; + } + + for(tchecker::clock_id_t i = 1; i <= no_of_orig_clocks_1; ++i) { + tchecker::dbm::db_t * orig_min_virt = tchecker::dbm::access(dbm1, dim1, i, i + no_of_orig_clocks_1); + tchecker::dbm::db_t * virt_min_orig = tchecker::dbm::access(dbm1, dim1, i + no_of_orig_clocks_1, i); + + result &= (*orig_min_virt == *virt_min_orig); + result &= (orig_min_virt->cmp == tchecker::LE); + result &= (orig_min_virt->value == 0); + if(!result) { + std::cout << __FILE__ << ": " << __LINE__ << ": " << i << " virtual and original clock of first dbm are not equivalent" << std::endl; + tchecker::dbm::output_matrix(std::cout, dbm1, dim1); + return result; + } + } + + for(tchecker::clock_id_t i = 1; i <= no_of_orig_clocks_2; ++i) { + tchecker::dbm::db_t * orig_min_virt = tchecker::dbm::access(dbm2, dim2, i, i + no_of_orig_clocks_1 + no_of_orig_clocks_2); + tchecker::dbm::db_t * virt_min_orig = tchecker::dbm::access(dbm2, dim2, i + no_of_orig_clocks_1 + no_of_orig_clocks_2, i); + + result &= (*orig_min_virt == *virt_min_orig); + result &= (orig_min_virt->cmp == tchecker::LE); + result &=(orig_min_virt->value == 0); + if(!result) { + std::cout << __FILE__ << ": " << __LINE__ << ": " << i << " virtual and original clock of second dbm are not equivalent" << std::endl; + tchecker::dbm::output_matrix(std::cout, dbm2, dim2); + return result; + } + } + + return result; +} + +bool is_phi_subset_of_a_zone(const tchecker::dbm::db_t *dbm, tchecker::clock_id_t dim, tchecker::clock_id_t no_of_orig_clocks, + const tchecker::virtual_constraint::virtual_constraint_t & phi_e) +{ + std::shared_ptr phi = tchecker::virtual_constraint::factory(dbm, dim, dim - no_of_orig_clocks - 1); + + return tchecker::dbm::is_le(phi_e.dbm(), phi->dbm(), phi_e.dim()); +} + +void sync(tchecker::dbm::db_t *dbm1, tchecker::dbm::db_t *dbm2, + tchecker::clock_id_t dim1, tchecker::clock_id_t dim2, + tchecker::clock_id_t no_of_orig_clocks_1, tchecker::clock_id_t no_of_orig_clocks_2, tchecker::clock_reset_container_t const & orig_reset1, tchecker::clock_reset_container_t const & orig_reset2) { - // TODO: add assertions - - tchecker::clock_reset_container_t virt_resets; + assert(is_virtually_equivalent(dbm1, dbm2, dim1, dim2, no_of_orig_clocks_1, no_of_orig_clocks_2)); for(const tchecker::clock_reset_t & r : orig_reset1) { @@ -25,77 +110,115 @@ void sync(tchecker::dbm::db_t *dbm1, tchecker::dbm::db_t *dbm2, tchecker::clock_ throw std::runtime_error("when checking for timed bisim, only resets to value zero are allowed"); } - reset_to_value(dbm1, dim, r.left_id() + 1 + lowest_virt_clk_id, 0); - reset_to_value(dbm2, dim, r.left_id() + 1 + lowest_virt_clk_id, 0); + reset_to_value(dbm1, dim1, r.left_id() + 1 + no_of_orig_clocks_1, 0); + reset_to_value(dbm2, dim2, r.left_id() + 1 + no_of_orig_clocks_2, 0); } - tchecker::clock_id_t border = lowest_virt_clk_id + no_of_orig_clocks_1; - for(const tchecker::clock_reset_t & r : orig_reset2) { if(r.right_id() != tchecker::REFCLOCK_ID || r.value() != 0) { throw std::runtime_error("when checking for timed bisim, only resets to value zero are allowed"); } - reset_to_value(dbm1, dim, r.left_id() + 1 + border, 0); - reset_to_value(dbm2, dim, r.left_id() + 1 + border, 0); + reset_to_value(dbm1, dim1, r.left_id() + 1 + no_of_orig_clocks_1 + no_of_orig_clocks_1, 0); + reset_to_value(dbm2, dim2, r.left_id() + 1 + no_of_orig_clocks_2 + no_of_orig_clocks_1, 0); } - virt_resets.clear(); - + assert(are_dbm_synced(dbm1, dbm2, dim1, dim2, no_of_orig_clocks_1, no_of_orig_clocks_2)); } -std::tuple, std::shared_ptr> -revert_sync(const tchecker::dbm::db_t *dbm1, const tchecker::dbm::db_t *dbm2, tchecker::clock_id_t dim, - const tchecker::virtual_constraint::virtual_constraint_t & phi_e, tchecker::clock_id_t lowest_virt_clk_id, - tchecker::clock_id_t no_of_orig_clocks_1) + + +std::pair, std::shared_ptr> +revert_sync(const tchecker::dbm::db_t *dbm1, const tchecker::dbm::db_t *dbm2, + tchecker::clock_id_t dim1, tchecker::clock_id_t dim2, + tchecker::clock_id_t no_of_orig_clocks_1, tchecker::clock_id_t no_of_orig_clocks_2, + const tchecker::virtual_constraint::virtual_constraint_t & phi_e) { - // TODO add assertions + assert(is_virtually_equivalent(const_cast(dbm1), const_cast(dbm2), dim1, dim2, no_of_orig_clocks_1, no_of_orig_clocks_2)); + + // due to the fact that the number of original clocks might differ, we need to build two reset sets + tchecker::clock_reset_container_t orig_reset_set_A; + tchecker::clock_reset_container_t orig_reset_set_B; + + tchecker::clock_reset_container_t virt_reset_set_A; + tchecker::clock_reset_container_t virt_reset_set_B; + + for(tchecker::clock_id_t i = 0; i < no_of_orig_clocks_1; ++i) { + if(tchecker::dbm::LE_ZERO == *tchecker::dbm::access(dbm1, dim1, i+1, 0) && tchecker::dbm::LE_ZERO == *tchecker::dbm::access(dbm1, dim1, 0, i+1)) { + + tchecker::clock_reset_t orig_tmp{i, tchecker::REFCLOCK_ID, 0}; - tchecker::dbm::db_t zero_value = tchecker::dbm::db(tchecker::LT, 0); - tchecker::clock_reset_container_t reset_set; + tchecker::clock_reset_t virt_tmp_A{i + no_of_orig_clocks_1, tchecker::REFCLOCK_ID, 0}; + tchecker::clock_reset_t virt_tmp_B{i + no_of_orig_clocks_2, tchecker::REFCLOCK_ID, 0}; - for(tchecker::clock_id_t i = 1; i < (dim - lowest_virt_clk_id); ++i) { - if(zero_value == *tchecker::dbm::access(dbm1, dim, i, 0) && zero_value == *tchecker::dbm::access(dbm1, dim, 0, i)) { - tchecker::clock_reset_t tmp{i + lowest_virt_clk_id - 1, tchecker::REFCLOCK_ID, 0}; - reset_set.emplace_back(tmp); + orig_reset_set_A.emplace_back(orig_tmp); + + virt_reset_set_A.emplace_back(virt_tmp_A); + virt_reset_set_B.emplace_back(virt_tmp_B); } } - for(tchecker::clock_id_t i = 1; i < (dim - lowest_virt_clk_id); ++i) { - if(zero_value == *tchecker::dbm::access(dbm2, dim, i, 0) && zero_value == *tchecker::dbm::access(dbm2, dim, 0, i)) { - tchecker::clock_reset_t tmp{i + lowest_virt_clk_id + no_of_orig_clocks_1 - 1, tchecker::REFCLOCK_ID, 0}; - reset_set.emplace_back(tmp); + for(tchecker::clock_id_t i = 0; i < no_of_orig_clocks_2; ++i) { + if(tchecker::dbm::LE_ZERO == *tchecker::dbm::access(dbm2, dim2, i+1, 0) && tchecker::dbm::LE_ZERO == *tchecker::dbm::access(dbm2, dim2, 0, i+1)) { + + tchecker::clock_reset_t orig_tmp{i, tchecker::REFCLOCK_ID, 0}; + + tchecker::clock_reset_t virt_tmp_A{i + no_of_orig_clocks_1 + no_of_orig_clocks_1, tchecker::REFCLOCK_ID, 0}; + tchecker::clock_reset_t virt_tmp_B{i + no_of_orig_clocks_1 + no_of_orig_clocks_2, tchecker::REFCLOCK_ID, 0}; + + orig_reset_set_B.emplace_back(orig_tmp); + + virt_reset_set_A.emplace_back(virt_tmp_A); + virt_reset_set_B.emplace_back(virt_tmp_B); } } - tchecker::dbm::db_t dbm1_clone[dim*dim]; - tchecker::dbm::copy(dbm1_clone, dbm1, dim); + tchecker::dbm::db_t dbm1_synced[dim1*dim1]; + tchecker::dbm::copy(dbm1_synced, dbm1, dim1); + tchecker::dbm::db_t dbm2_synced[dim2*dim2]; + tchecker::dbm::copy(dbm2_synced, dbm2, dim2); + + sync(dbm1_synced, dbm2_synced, dim1, dim2, no_of_orig_clocks_1, no_of_orig_clocks_2, orig_reset_set_A, orig_reset_set_B); - tchecker::dbm::constrain(dbm1_clone, dim, phi_e.get_vc(lowest_virt_clk_id - 1)); + assert(is_phi_subset_of_a_zone(dbm1_synced, dim1, no_of_orig_clocks_1, phi_e) || is_phi_subset_of_a_zone(dbm2_synced, dim2, no_of_orig_clocks_2, phi_e)); - tchecker::dbm::db_t dbm2_clone[dim*dim]; - tchecker::dbm::copy(dbm2_clone, dbm2, dim); + if(tchecker::dbm::status_t::EMPTY == tchecker::dbm::constrain(dbm1_synced, dim1, phi_e.get_vc(no_of_orig_clocks_1, true))) { + throw std::runtime_error("problems in _A while reverting the sync"); // should NEVER occur + } - tchecker::dbm::constrain(dbm2_clone, dim, phi_e.get_vc(lowest_virt_clk_id - 1)); + if(tchecker::dbm::status_t::EMPTY == tchecker::dbm::constrain(dbm2_synced, dim2, phi_e.get_vc(no_of_orig_clocks_2, true))) { + throw std::runtime_error("problems in _B while reverting the sync"); // should NEVER occur + } - tchecker::dbm::db_t * multiple_reset = revert_multiple_reset(dbm1, dim, dbm1_clone, reset_set); + tchecker::dbm::db_t * multiple_reset = revert_multiple_reset(dbm1, dim1, dbm1_synced, virt_reset_set_A); std::shared_ptr first - = tchecker::virtual_constraint::factory(multiple_reset, dim, dim - lowest_virt_clk_id); + = tchecker::virtual_constraint::factory(multiple_reset, dim1, no_of_orig_clocks_1 + no_of_orig_clocks_2); free(multiple_reset); - multiple_reset = revert_multiple_reset(dbm2, dim, dbm2_clone, reset_set); + multiple_reset = revert_multiple_reset(dbm2, dim2, dbm2_synced, virt_reset_set_B); std::shared_ptr second - = tchecker::virtual_constraint::factory(multiple_reset, dim, dim - lowest_virt_clk_id); + = tchecker::virtual_constraint::factory(multiple_reset, dim2, no_of_orig_clocks_1 + no_of_orig_clocks_2); free(multiple_reset); - reset_set.clear(); + orig_reset_set_A.clear(); + orig_reset_set_B.clear(); + - return std::make_tuple(first, second); + virt_reset_set_A.clear(); + virt_reset_set_B.clear(); + + assert(is_phi_subset_of_a_zone(dbm1, dim1, no_of_orig_clocks_1, *first)); + assert(is_phi_subset_of_a_zone(dbm2, dim2, no_of_orig_clocks_2, *second)); + + return std::make_pair(first, second); } +} // end of namespace vcg + +} // end of namespace tchecker diff --git a/src/vcg/vcg.cc b/src/vcg/vcg.cc index 666a47cd..b4e5765e 100644 --- a/src/vcg/vcg.cc +++ b/src/vcg/vcg.cc @@ -14,7 +14,7 @@ namespace vcg { vcg_t::vcg_t(std::shared_ptr const & system, enum tchecker::ts::sharing_type_t sharing_type, std::shared_ptr const & semantics, tchecker::clock_id_t no_of_virtual_clocks, std::shared_ptr const & extrapolation, std::size_t block_size, std::size_t table_size) - : tchecker::zg::zg_t(system, sharing_type, semantics, extrapolation, block_size, table_size), + : tchecker::zg::zg_t(system, sharing_type, semantics, extrapolation, block_size, table_size, false), _no_of_virtual_clocks(no_of_virtual_clocks) { } diff --git a/src/vcg/virtual_constraint.cc b/src/vcg/virtual_constraint.cc index f163951f..c73bbd8e 100644 --- a/src/vcg/virtual_constraint.cc +++ b/src/vcg/virtual_constraint.cc @@ -11,116 +11,172 @@ namespace tchecker { namespace virtual_constraint { -const tchecker::clock_id_t virtual_constraint_t::get_no_of_virt_clocks() const +tchecker::clock_id_t virtual_constraint_t::get_no_of_virt_clocks() const { return this->dim() - 1; } -// WARNING: above might not be tight after this call -void insert_values(std::shared_ptr to_change, tchecker::clock_id_t i, tchecker::clock_id_t j) +// WARNING: The vitrual constraints placed at result are NOT tight! +void add_neg_single(tchecker::zone_container_t *result, const virtual_constraint_t & cur, tchecker::clock_id_t i, tchecker::clock_id_t j, tchecker::dbm::db_t *max_value) { - tchecker::dbm::db_t * j_minus_i = tchecker::dbm::access(to_change->dbm(), to_change->dim(), j, i); - tchecker::dbm::db_t * i_minus_j = tchecker::dbm::access(to_change->dbm(), to_change->dim(), i, j); + // the first line is a special case since the value of 0 - c cannot become larger than zero. + tchecker::dbm::db_t upper_bound = ((0 == i) && (tchecker::dbm::LE_ZERO < *max_value)) ? tchecker::dbm::LE_ZERO : *max_value; + + // if the upper constraint is larger than the upper bound, the inverse is empty anyway. + if(*tchecker::dbm::access(cur.dbm(), cur.dim(), i, j) < upper_bound) { + + tchecker::dbm::db_t copy{tchecker::dbm::invert(*tchecker::dbm::access(cur.dbm(), cur.dim(), i, j))}; + std::shared_ptr to_insert = tchecker::virtual_constraint::factory(cur); + + // we remove what is allowed by cur, by setting the entry j - i to the inverse of cur[i][j], and add what is not allowed, by setting i - j to LT_INFINITY + + tchecker::dbm::db_t * j_minus_i = tchecker::dbm::access(to_insert->dbm(), to_insert->dim(), j, i); + tchecker::dbm::db_t * i_minus_j = tchecker::dbm::access(to_insert->dbm(), to_insert->dim(), i, j); - tchecker::dbm::db_t db_above{ - (tchecker::LE == tchecker::dbm::comparator(*i_minus_j)) ? tchecker::LT : tchecker::LE, - tchecker::dbm::value(*i_minus_j)}; + *j_minus_i = copy; + *i_minus_j = upper_bound; - *j_minus_i = db_above; - *i_minus_j = tchecker::dbm::LT_INFINITY; + result->append_zone(to_insert); + } } -// WARNING: The vitrual constraints placed at result are NOT tight! -void add_neg(tchecker::zone_container_t *result, const virtual_constraint_t *cur, tchecker::clock_id_t i, tchecker::clock_id_t j) +void +add_neg(tchecker::zone_container_t *result, const virtual_constraint_t & cur, + tchecker::clock_id_t i, tchecker::clock_id_t j, + tchecker::dbm::db_t *max_i_minus_j, tchecker::dbm::db_t *max_j_minus_i) { - // we first insert all clock valuations for which chi_i - chi_j is to high - std::shared_ptr above = tchecker::virtual_constraint::factory(*cur); - insert_values(above, i, j); - result->append_zone(above); - // now we insert all clocks for which chi_i - chi_j is to low - std::shared_ptr below = tchecker::virtual_constraint::factory(*cur); - insert_values(below, j, i); - result->append_zone(below); + // we first add the neg breaking the upper bound of i-j + add_neg_single(result, cur, i, j, max_i_minus_j); + // we afterwards add the neg breaking the upper bound of j - i + add_neg_single(result, cur, j, i, max_j_minus_i); } -tchecker::zone_container_t * virtual_constraint_t::neg() const +std::shared_ptr> virtual_constraint_t::neg_helper(tchecker::dbm::db_t *upper_bounds) const { tchecker::zone_container_t inter{this->dim()}; for(tchecker::clock_id_t i = 0; i < this->dim(); ++i) { for(tchecker::clock_id_t j = i+1; j < this->dim(); ++j) { - tchecker::clock_id_t size_before = inter.size(); + tchecker::zone_container_t helper{this->dim()}; + helper.append_container(inter); // this way, only the pointers are copied. - add_neg(&inter, this, i, j); + tchecker::dbm::db_t * i_minus_j = tchecker::dbm::access(upper_bounds, this->dim(), i, j); + tchecker::dbm::db_t * j_minus_i = tchecker::dbm::access(upper_bounds, this->dim(), j, i); + + add_neg(&inter, *this, i, j, i_minus_j, j_minus_i); // do the same for all already added virtual constraints. - for(tchecker::clock_id_t iter = 0; iter < size_before; ++iter) { - add_neg(&inter, &(*(inter[iter])), i, j); + for(auto iter = helper.begin(); iter < helper.end(); iter++) { + add_neg(&inter, **iter, i, j, i_minus_j, j_minus_i); } } } - tchecker::zone_container_t * result = new tchecker::zone_container_t(this->dim()); + std::shared_ptr> result = std::make_shared>(this->dim()); for(auto iter = inter.begin(); iter < inter.end(); iter++) { - if(tchecker::dbm::NON_EMPTY == tchecker::dbm::tighten((*iter)->dbm(), (*iter)->dim())) { + if(tchecker::dbm::NON_EMPTY ==tchecker::dbm::tighten((*iter)->dbm(), (*iter)->dim()) && + tchecker::dbm::NON_EMPTY == tchecker::dbm::intersection((*iter)->dbm(), (*iter)->dbm(), upper_bounds, (*iter)->dim())) { result->append_zone(*iter); - } else { - tchecker::virtual_constraint::destruct(&(**iter)); } } return result; } -clock_constraint_container_t virtual_constraint_t::get_vc(tchecker::clock_id_t orig_clocks_offset) const +std::shared_ptr> virtual_constraint_t::neg() const { + tchecker::dbm::db_t univ[this->dim()*this->dim()]; + tchecker::dbm::universal(univ, this->dim()); + return neg_helper(univ); +} + +clock_constraint_container_t virtual_constraint_t::get_vc(tchecker::clock_id_t no_of_orig_clocks, bool system_clocks) const +{ + + tchecker::clock_id_t ref_clk = system_clocks ? tchecker::REFCLOCK_ID : 0; clock_constraint_container_t result; - for(tchecker::clock_id_t i = 1; i < get_no_of_virt_clocks(); ++i) { - tchecker::clock_id_t cur = i + orig_clocks_offset; - result.emplace_back(0, cur, tchecker::dbm::access(this->dbm(), this->dim(), 0, i)->cmp, tchecker::dbm::access(this->dbm(), this->dim(), 0, i)->value); - result.emplace_back(cur, 0, tchecker::dbm::access(this->dbm(), this->dim(), i, 0)->cmp, tchecker::dbm::access(this->dbm(), this->dim(), i, 0)->value); + for(tchecker::clock_id_t i = 1; i <= get_no_of_virt_clocks(); ++i) { + tchecker::clock_id_t cur = i + no_of_orig_clocks; + + if(system_clocks) { + cur--; + } + + result.emplace_back(ref_clk, cur, tchecker::dbm::access(this->dbm(), this->dim(), 0, i)->cmp, tchecker::dbm::access(this->dbm(), this->dim(), 0, i)->value); + result.emplace_back(cur, ref_clk, tchecker::dbm::access(this->dbm(), this->dim(), i, 0)->cmp, tchecker::dbm::access(this->dbm(), this->dim(), i, 0)->value); + + for(tchecker::clock_id_t j = i+1; j <= get_no_of_virt_clocks(); ++j) { + tchecker::clock_id_t second_cur = j + no_of_orig_clocks; + + if(system_clocks) { + second_cur--; + } - for(tchecker::clock_id_t j = i+1; j < get_no_of_virt_clocks(); ++j) { - tchecker::clock_id_t second_cur = j + orig_clocks_offset; result.emplace_back(second_cur, cur, tchecker::dbm::access(this->dbm(), this->dim(), j, i)->cmp, tchecker::dbm::access(this->dbm(), this->dim(), j, i)->value); result.emplace_back(cur, second_cur, tchecker::dbm::access(this->dbm(), this->dim(), i, j)->cmp, tchecker::dbm::access(this->dbm(), this->dim(), i, j)->value); } } + return result; } -tchecker::zone_container_t virtual_constraint_t::logic_and(tchecker::zone_container_t *container) +void virtual_constraint_t::neg_logic_and(std::shared_ptr> result, const virtual_constraint_t & other) const { + assert(result->is_empty()); + assert(result->dim() == other.dim()); + assert(this->dim() == other.dim()); + + result->append_container(this->neg_helper(const_cast(other.dbm()))); +} + +enum tchecker::dbm::status_t virtual_constraint_t::logic_and(std::shared_ptr result, const virtual_constraint_t & other) const { - tchecker::zone_container_t result{this->dim()}; - for(auto iter = container->begin(); iter < container->end(); iter++ ) { + assert(result->dim() == other.dim()); + assert(this->dim() == result->dim()); + return tchecker::dbm::intersection(result->dbm(), other.dbm(), this->dbm(), this->dim()); +} - std::shared_ptr to_append = factory(this->dim()); +enum tchecker::dbm::status_t virtual_constraint_t::logic_and(std::shared_ptr result, const tchecker::zg::zone_t & zone) const +{ + return this->logic_and(*result, zone); +} + +enum tchecker::dbm::status_t virtual_constraint_t::logic_and(tchecker::zg::zone_t & result, const tchecker::zg::zone_t & zone) const +{ + assert(result.dim() == zone.dim()); + tchecker::dbm::copy(result.dbm(), zone.dbm(), zone.dim()); + return tchecker::dbm::constrain(result.dbm(), result.dim(), this->get_vc(result.dim() - this->dim(), true)); +} + +void virtual_constraint_t::logic_and(std::shared_ptr> result, + std::shared_ptr> const container) const +{ + assert(result->is_empty()); + assert(result->dim() == container->dim()); + assert(this->dim() == container->dim()); + + for(auto iter = container->begin(); iter < container->end(); iter++ ) { + std::shared_ptr to_append = factory(this->get_no_of_virt_clocks()); if(tchecker::dbm::EMPTY != tchecker::dbm::intersection(to_append->dbm(), (*iter)->dbm(), this->dbm(), this->dim())) { - result.append_zone(to_append); + result->append_zone(to_append); } } - - return result; } -std::shared_ptr factory(tchecker::clock_id_t dim) +std::shared_ptr factory(tchecker::clock_id_t number_of_virtual_clocks) { return static_pointer_cast( - tchecker::zg::factory(dim)); + tchecker::zg::factory(number_of_virtual_clocks + 1)); } std::shared_ptr factory(tchecker::virtual_constraint::virtual_constraint_t const & virtual_constraint) { - tchecker::zg::zone_t const & reinterpreted_zone = reinterpret_cast(virtual_constraint); - return static_pointer_cast( - tchecker::zg::factory(reinterpreted_zone) - ); + return factory(virtual_constraint.dbm(), virtual_constraint.dim(), virtual_constraint.get_no_of_virt_clocks()); } @@ -129,10 +185,15 @@ std::shared_ptr factory(std::shared_ptrdbm(), zone->dim(), no_of_virtual_clocks); } +std::shared_ptr factory(tchecker::zg::zone_t const & zone, tchecker::clock_id_t no_of_virtual_clocks) +{ + return factory(zone.dbm(), zone.dim(), no_of_virtual_clocks); +} + std::shared_ptr factory(const tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim, tchecker::clock_id_t no_of_virtual_clocks) { - std::shared_ptr result = factory(no_of_virtual_clocks + 1); + std::shared_ptr result = factory(no_of_virtual_clocks); std::vector indices; indices.emplace_back(0); @@ -142,78 +203,123 @@ std::shared_ptr factory(const tchecker::dbm::db_t * dbm, t indices.emplace_back(i); } - for(std::size_t i = 0; i < indices.size(); ++i) + for(tchecker::clock_id_t i = 0; i < indices.size(); ++i) { - for(std::size_t j = 0; j < indices.size(); ++j) + for(tchecker::clock_id_t j = 0; j < indices.size(); ++j) { - tchecker::dbm::constrain( - result->dbm(), result->dim(), i, j, dbm[indices[i]*dim + indices[j]].cmp, dbm[indices[i]*dim + indices[j]].value - ); + tchecker::dbm::db_t * i_minus_j = tchecker::dbm::access(result->dbm(), result->dim(), i, j); + *i_minus_j = *(tchecker::dbm::access(dbm, dim, indices[i], indices[j])); } } return result; } -void destruct(virtual_constraint_t *to_destruct) +std::shared_ptr> combine(tchecker::zone_container_t & lo_vc, tchecker::clock_id_t no_of_virtual_clocks) { - tchecker::zg::zone_destruct_and_deallocate(to_destruct); -} - -tchecker::zone_container_t * combine_lhs_land_not_rhs(std::shared_ptr lhs, std::shared_ptr rhs, tchecker::clock_id_t dim) -{ - tchecker::zone_container_t *result = new tchecker::zone_container_t(dim); - tchecker::zone_container_t *neg = rhs->neg(); + tchecker::zone_container_t lo_of_non_empty_vc{no_of_virtual_clocks + 1}; - for(auto iter = neg->begin(); iter < neg->end(); iter++) { - std::shared_ptr to_append = factory(dim); - if(tchecker::dbm::EMPTY != tchecker::dbm::intersection(to_append->dbm(), (*iter)->dbm(), lhs->dbm(), dim)) { - result->append_zone(*to_append); // to_append is copied here + for(auto phi = lo_vc.begin(); phi < lo_vc.end(); phi++) { + if(!(*phi)->is_empty()) { + lo_of_non_empty_vc.append_zone(*phi); } - destruct(&(*to_append)); } - return result; -} + std::shared_ptr> result = std::make_shared>(no_of_virtual_clocks + 1); -tchecker::zone_container_t * combine_helper(std::shared_ptr lhs, tchecker::zone_container_t * lo_vc, tchecker::clock_id_t dim) -{ - tchecker::zone_container_t *result = new tchecker::zone_container_t(dim); - result->append_zone(*lhs); - for(auto iter = lo_vc->begin(); iter < lo_vc->end(); iter++) { - tchecker::zone_container_t *inter = result; - result = new tchecker::zone_container_t(dim); + for(auto iter = lo_of_non_empty_vc.begin(); iter < lo_of_non_empty_vc.end(); iter++) { + + std::shared_ptr> inter = std::make_shared>(no_of_virtual_clocks + 1); + std::shared_ptr> helper; + inter->append_zone(*iter); + + for(auto phi_r = result->begin(); phi_r < result->end(); phi_r++) { + helper = std::make_shared>(no_of_virtual_clocks + 1); + for(auto phi_inter = inter->begin(); phi_inter < inter->end(); phi_inter++) { + std::shared_ptr> to_append + = std::make_shared>(no_of_virtual_clocks + 1); + + (*phi_r)->neg_logic_and(to_append, **phi_inter); + + helper->append_container(to_append); + } + inter = helper; + } - for(auto inter_iter = inter->begin(); inter_iter < inter->end(); inter_iter++) { - tchecker::zone_container_t *lhs_land_not_rhs = combine_lhs_land_not_rhs(*inter_iter, *iter, dim); - for(auto land_iter = lhs_land_not_rhs->begin(); land_iter < lhs_land_not_rhs->end(); land_iter++) { - result->append_zone(*land_iter); + for(auto phi = inter->begin(); phi < inter->end(); phi++) { + if(!(*phi)->is_empty()) { + assert(tchecker::dbm::is_le((*phi)->dbm(), (*iter)->dbm(), (*iter)->dim())); + result->append_zone(**phi); } } - delete inter; + } return result; +} +bool all_elements_are_stronger_than(std::shared_ptr> weaker, + std::shared_ptr> stronger, tchecker::clock_id_t no_of_virtual_clocks) { + bool result = true; + for(auto iter = stronger->begin(); iter < stronger->end(); iter++) { + result &= ((*iter)->dim() == (no_of_virtual_clocks + 1)); + bool inter = false; + for(auto second_iter = weaker->begin(); second_iter < weaker->end(); second_iter++) { + inter |= tchecker::dbm::is_le((*iter)->dbm(), (*second_iter)->dbm(), no_of_virtual_clocks + 1); + } + result &= inter; + } + return result; } -tchecker::zone_container_t * combine(std::vector> & lo_lo_vc, tchecker::clock_id_t dim) +std::shared_ptr> contained_in_all(std::vector>> & zones, tchecker::clock_id_t no_of_virtual_clocks) { - if(lo_lo_vc.empty()) { - return new tchecker::zone_container_t(dim); + + assert( + std::all_of(zones.begin(), zones.end(), + [no_of_virtual_clocks](std::shared_ptr> & lo_zones){return no_of_virtual_clocks + 1 == lo_zones->dim();} // cppcheck-suppress [assertWithSideEffect] + ) + ); + + if (zones.empty()) { + return std::make_shared>(no_of_virtual_clocks + 1); + } + + if (1 == zones.size()) { + return (zones[0]); } - tchecker::zone_container_t cur = lo_lo_vc.back(); - lo_lo_vc.pop_back(); + std::shared_ptr> cur = zones.back(); + zones.pop_back(); + + std::shared_ptr> inter = contained_in_all(zones, no_of_virtual_clocks); - tchecker::zone_container_t *result = combine(lo_lo_vc, dim); + std::shared_ptr> result = std::make_shared>(no_of_virtual_clocks + 1); - for(auto cur_iter = cur.begin(); cur_iter < cur.end(); cur_iter++) { - tchecker::zone_container_t *inter = combine_helper(*cur_iter, result, dim); - delete result; - result = inter; + for(auto iter_cur = cur->begin(); iter_cur < cur->end(); iter_cur++) { + for(auto iter_inter = inter->begin(); iter_inter < inter->end(); iter_inter++) { + std::shared_ptr tmp = factory(no_of_virtual_clocks); + if(tchecker::dbm::NON_EMPTY == tchecker::dbm::intersection(tmp->dbm(), (**iter_cur).dbm(), (**iter_inter).dbm(), (**iter_cur).dim())) { + result->append_zone(tmp); + } + } } + + assert( + std::all_of(result->begin(), result->end(), + [](std::shared_ptr res){return tchecker::dbm::is_consistent(res->dbm(), res->dim());} // cppcheck-suppress assertWithSideEffect + ) + ); + + assert( + std::all_of(result->begin(), result->end(), + [](std::shared_ptr res){return tchecker::dbm::is_tight(res->dbm(), res->dim());} // cppcheck-suppress assertWithSideEffect + ) + ); + + assert(all_elements_are_stronger_than(cur, result, no_of_virtual_clocks)); + return result; } diff --git a/src/zg/semantics.cc b/src/zg/semantics.cc index 05bb59c7..a8ca1e77 100644 --- a/src/zg/semantics.cc +++ b/src/zg/semantics.cc @@ -42,9 +42,15 @@ tchecker::state_status_t next_helper(tchecker::dbm::db_t * dbm, tchecker::clock_ tchecker::clock_reset_container_t const & clkreset, bool tgt_delay_allowed, tchecker::clock_constraint_container_t const & tgt_invariant) { + assert(tchecker::dbm::is_tight(dbm, dim)); + assert(tchecker::dbm::is_consistent(dbm, dim)); + if (tchecker::dbm::constrain(dbm, dim, src_invariant) == tchecker::dbm::EMPTY) return tchecker::STATE_CLOCKS_SRC_INVARIANT_VIOLATED; + assert(tchecker::dbm::is_tight(dbm, dim)); + assert(tchecker::dbm::is_consistent(dbm, dim)); + if (src_delay_allowed) { tchecker::dbm::open_up(dbm, dim); @@ -55,11 +61,21 @@ tchecker::state_status_t next_helper(tchecker::dbm::db_t * dbm, tchecker::clock_ if (tchecker::dbm::constrain(dbm, dim, guard) == tchecker::dbm::EMPTY) return tchecker::STATE_CLOCKS_GUARD_VIOLATED; + + assert(tchecker::dbm::is_tight(dbm, dim)); + assert(tchecker::dbm::is_consistent(dbm, dim)); + tchecker::dbm::reset(dbm, dim, clkreset); + assert(tchecker::dbm::is_tight(dbm, dim)); + assert(tchecker::dbm::is_consistent(dbm, dim)); + if (tchecker::dbm::constrain(dbm, dim, tgt_invariant) == tchecker::dbm::EMPTY) return tchecker::STATE_CLOCKS_TGT_INVARIANT_VIOLATED; + assert(tchecker::dbm::is_tight(dbm, dim)); + assert(tchecker::dbm::is_consistent(dbm, dim)); + return tchecker::STATE_OK; } @@ -98,6 +114,23 @@ tchecker::state_status_t prev_helper(tchecker::dbm::db_t * dbm, tchecker::clock_ return tchecker::STATE_OK; } +/* semantics_t */ + +tchecker::state_status_t semantics_t::delay( tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim, + tchecker::clock_constraint_container_t const & invariant) +{ + if (tchecker::dbm::constrain(dbm, dim, invariant) == tchecker::dbm::EMPTY) + return tchecker::STATE_CLOCKS_SRC_INVARIANT_VIOLATED; + + tchecker::dbm::open_up(dbm, dim); + + if (tchecker::dbm::constrain(dbm, dim, invariant) == tchecker::dbm::EMPTY) + return tchecker::STATE_CLOCKS_SRC_INVARIANT_VIOLATED; // should never occur + + return tchecker::STATE_OK; +} + + /* standard_semantics_t */ tchecker::state_status_t standard_semantics_t::initial(tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim, bool delay_allowed, @@ -225,27 +258,13 @@ tchecker::state_status_t elapsed_semantics_t::prev(tchecker::dbm::db_t * dbm, tc tchecker::state_status_t distinguished_semantics_t::initial( tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim, bool delay_allowed, tchecker::clock_constraint_container_t const & invariant) { - return initial_helper(dbm, dim, delay_allowed, invariant); + return initial_helper(dbm, dim, false, invariant); } tchecker::state_status_t distinguished_semantics_t::final( tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim, bool delay_allowed, tchecker::clock_constraint_container_t const & invariant) { - return final_helper(dbm, dim, delay_allowed, invariant); -} - -tchecker::state_status_t distinguished_semantics_t::delay( tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim, - tchecker::clock_constraint_container_t const & invariant) -{ - if (tchecker::dbm::constrain(dbm, dim, invariant) == tchecker::dbm::EMPTY) - return tchecker::STATE_CLOCKS_SRC_INVARIANT_VIOLATED; - - tchecker::dbm::open_up(dbm, dim); - - if (tchecker::dbm::constrain(dbm, dim, invariant) == tchecker::dbm::EMPTY) - return tchecker::STATE_CLOCKS_SRC_INVARIANT_VIOLATED; // should never occur - - return tchecker::STATE_OK; + return final_helper(dbm, dim, false, invariant); } tchecker::state_status_t distinguished_semantics_t::next( tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim, bool src_delay_allowed, diff --git a/src/zg/zg.cc b/src/zg/zg.cc index 6fd2f12d..378ba604 100644 --- a/src/zg/zg.cc +++ b/src/zg/zg.cc @@ -63,7 +63,7 @@ void zg_t::next(tchecker::zg::const_state_sptr_t const & s, outgoing_edges_value t->reset_container(), tgt_delay, t->tgt_invariant_container()); }; - sst_handler(out_edge, v, mask, ta_func, se_func, s, true); + sst_handler(out_edge, v, mask, ta_func, se_func, s, true, _enable_extrapolation); } void zg_t::next(tchecker::zg::const_state_sptr_t const & s, std::vector & v, @@ -248,11 +248,11 @@ void zg_t::sst_handler( edge_t edge, std::vector & v, tchecker::state_sta tchecker::zg::state_sptr_t &, tchecker::zg::transition_sptr_t &, helping_hand_t *), - tchecker::zg::const_state_sptr_t const & to_clone, bool clone + tchecker::zg::const_state_sptr_t const & to_clone, bool clone, bool enable_extrapolation ) { tchecker::zg::state_sptr_t s; - if(clone) { // for some crazy reason, I cannot check for null here and, therefore, we need clone + if(clone) { // for some crazy reasons, I cannot check for null here and, therefore, we need clone s = _state_allocator.clone(*to_clone); } else { @@ -271,7 +271,7 @@ void zg_t::sst_handler( edge_t edge, std::vector & v, tchecker::state_sta status = se_func(*_system, *_semantics, dbm, dim, s, t, &helper); - if(tchecker::STATE_OK == status) { + if(tchecker::STATE_OK == status && enable_extrapolation) { _extrapolation->extrapolate(dbm, dim, *(s->vloc_ptr())); } } @@ -344,28 +344,28 @@ next(tchecker::zg::zg_t &zg, std::shared_ptr factory(std::shared_ptr const & system, enum tchecker::ts::sharing_type_t sharing_type, enum tchecker::zg::semantics_type_t semantics_type, enum tchecker::zg::extrapolation_type_t extrapolation_type, std::size_t block_size, - std::size_t table_size) + std::size_t table_size, bool enable_extrapolation) { std::shared_ptr extrapolation{ tchecker::zg::extrapolation_factory(extrapolation_type, *system)}; if (extrapolation.get() == nullptr) return nullptr; std::shared_ptr semantics{tchecker::zg::semantics_factory(semantics_type)}; - return std::make_shared(system, sharing_type, semantics, extrapolation, block_size, table_size); + return std::make_shared(system, sharing_type, semantics, extrapolation, block_size, table_size, enable_extrapolation); } std::shared_ptr factory(std::shared_ptr const & system, enum tchecker::ts::sharing_type_t sharing_type, enum tchecker::zg::semantics_type_t semantics_type, enum tchecker::zg::extrapolation_type_t extrapolation_type, tchecker::clockbounds::clockbounds_t const & clock_bounds, std::size_t block_size, - std::size_t table_size) + std::size_t table_size, bool enable_extrapolation) { std::shared_ptr extrapolation{ tchecker::zg::extrapolation_factory(extrapolation_type, clock_bounds)}; if (extrapolation.get() == nullptr) return nullptr; std::shared_ptr semantics{tchecker::zg::semantics_factory(semantics_type)}; - return std::make_shared(system, sharing_type, semantics, extrapolation, block_size, table_size); + return std::make_shared(system, sharing_type, semantics, extrapolation, block_size, table_size, enable_extrapolation); } } // end of namespace zg diff --git a/test/tck-compare/CMakeLists.txt b/test/tck-compare/CMakeLists.txt index 032e7994..17ad3bfe 100644 --- a/test/tck-compare/CMakeLists.txt +++ b/test/tck-compare/CMakeLists.txt @@ -38,7 +38,21 @@ set(DOT_MAX_SIZE 20000) # only append to the tail of this list! set(INPUTS missing_initial.sh: + easy-ad94.sh: + easy-ad94-added-transition.sh: + easy-ad94-different-guard.sh: ad94.sh: + Lieb_et_al_1.sh: + Lieb_et_al_1_diff_invariant.sh: + Lieb_et_al_2.sh: + Lieb_et_al_3.sh: + Lieb_et_al_4.sh: + Lieb_et_al_5.sh: + count_to_inf.sh: + Lieb_et_al_1_non_determ_bisim.sh: + Lieb_et_al_2_non_determ_bisim.sh: + Lieb_et_al_2_determ_split_bisim.sh: + Lieb_et_al_2_determ_split_non_bisim.sh: corsso.sh:2:2:10:1:2 critical-region-async.sh:2:10 csmacd.sh:3 @@ -64,15 +78,90 @@ file(RELATIVE_PATH here ${CMAKE_BINARY_DIR} ${CMAKE_CURRENT_BINARY_DIR}) message(STATUS "Generating '${here}' tests. This may take a long time.") tck_register_testcases("tck-compare-" CHECK_TESTCASES_ savelist TCK_COMPARE_INPUT_FILES ${INPUTS}) -# TODO: Insert real Testcases here. You can find the name of all the available files in TCK_COMPARE_INPUT_FILES or add some to INPUTS - list(GET TCK_COMPARE_INPUT_FILES 0 no_initial) -list(GET TCK_COMPARE_INPUT_FILES 1 ad) - +list(GET TCK_COMPARE_INPUT_FILES 1 easy-ad) +list(GET TCK_COMPARE_INPUT_FILES 2 easy-ad-added-transition) +list(GET TCK_COMPARE_INPUT_FILES 3 easy-ad-different-guard) +list(GET TCK_COMPARE_INPUT_FILES 4 ad) +list(GET TCK_COMPARE_INPUT_FILES 5 Lieb1) +list(GET TCK_COMPARE_INPUT_FILES 6 Lieb1_diff_inv) +list(GET TCK_COMPARE_INPUT_FILES 7 Lieb2) +list(GET TCK_COMPARE_INPUT_FILES 8 Lieb3) +list(GET TCK_COMPARE_INPUT_FILES 9 Lieb4) +list(GET TCK_COMPARE_INPUT_FILES 10 Lieb5) +list(GET TCK_COMPARE_INPUT_FILES 11 count_to_inf) +list(GET TCK_COMPARE_INPUT_FILES 12 Lieb1_non_determ_bisim) +list(GET TCK_COMPARE_INPUT_FILES 13 Lieb_et_al_2_non_determ_bisim) +list(GET TCK_COMPARE_INPUT_FILES 14 Lieb_et_al_2_determ_split_bisim) +list(GET TCK_COMPARE_INPUT_FILES 15 Lieb_et_al_2_determ_split_non_bisim) + +# check whether the no_initial_check works create_testcase(no_initial_first ${no_initial} ${ad} strong-timed-bisim) create_testcase(no_initial_second ${ad} ${no_initial} strong-timed-bisim) +# testcases using easy-ad94 + +create_testcase(easy-ad94-self ${easy-ad} ${easy-ad} strong-timed-bisim) +create_testcase(easy-ad94-self-added-transition ${easy-ad-added-transition} ${easy-ad-added-transition} strong-timed-bisim) +create_testcase(easy-ad94-self-different-guard ${easy-ad-different-guard} ${easy-ad-different-guard} strong-timed-bisim) + +create_testcase(easy-ad94-easy-ad94-added-transition ${easy-ad} ${easy-ad-added-transition} strong-timed-bisim) +create_testcase(easy-ad94-added-transition-easy-ad94 ${easy-ad-added-transition} ${easy-ad} strong-timed-bisim) + +create_testcase(easy-ad94-different-guard-easy-ad94 ${easy-ad-different-guard} ${easy-ad} strong-timed-bisim) + +create_testcase(easy-ad94-different-guard-easy-ad94-added-transition ${easy-ad-different-guard} ${easy-ad-added-transition} strong-timed-bisim) + +# testcases using the examples of Lieb et al. + +# Lieb1 +create_testcase(Lieb-et-al-1-self ${Lieb1} ${Lieb1} strong-timed-bisim) + +create_testcase(Lieb-et-al-1-Lieb-et-al-1-diff-inv ${Lieb1} ${Lieb1_diff_inv} strong-timed-bisim) +create_testcase(Lieb-et-al-1-Lieb-et-al-1-non-determ-bisim ${Lieb1} ${Lieb1_non_determ_bisim} strong-timed-bisim) + +create_testcase(Lieb-et-al-1-Lieb-et-al-2 ${Lieb1} ${Lieb2} strong-timed-bisim) +create_testcase(Lieb-et-al-1-Lieb-et-al-3 ${Lieb1} ${Lieb3} strong-timed-bisim) +create_testcase(Lieb-et-al-1-Lieb-et-al-4 ${Lieb1} ${Lieb4} strong-timed-bisim) +create_testcase(Lieb-et-al-1-Lieb-et-al-5 ${Lieb1} ${Lieb5} strong-timed-bisim) +# Lieb2 +create_testcase(Lieb-et-al-2-self ${Lieb2} ${Lieb2} strong-timed-bisim) +create_testcase(Lieb-et-al-2-Lieb-et-al-2-non-determ-bisim ${Lieb2} ${Lieb_et_al_2_non_determ_bisim} strong-timed-bisim) +create_testcase(Lieb-et-al-2-Lieb-et-al-2-determ-split-bisim ${Lieb2} ${Lieb_et_al_2_determ_split_bisim} strong-timed-bisim) +create_testcase(Lieb-et-al-2-Lieb-et-al-2-determ-split-non-bisim ${Lieb2} ${Lieb_et_al_2_determ_split_non_bisim} strong-timed-bisim) + +create_testcase(Lieb-et-al-2-Lieb-et-al-3 ${Lieb2} ${Lieb3} strong-timed-bisim) +create_testcase(Lieb-et-al-2-Lieb-et-al-4 ${Lieb2} ${Lieb4} strong-timed-bisim) +create_testcase(Lieb-et-al-2-Lieb-et-al-5 ${Lieb2} ${Lieb5} strong-timed-bisim) + +#Lieb 3 +create_testcase(Lieb-et-al-3-self ${Lieb3} ${Lieb3} strong-timed-bisim) + +create_testcase(Lieb-et-al-3-Lieb-et-al-4 ${Lieb3} ${Lieb4} strong-timed-bisim) +create_testcase(Lieb-et-al-3-Lieb-et-al-5 ${Lieb3} ${Lieb5} strong-timed-bisim) + +#Lieb 4 +create_testcase(Lieb-et-al-4-self ${Lieb4} ${Lieb4} strong-timed-bisim) + +create_testcase(Lieb-et-al-4-Lieb-et-al-5 ${Lieb4} ${Lieb5} strong-timed-bisim) + +#Lieb 5 +create_testcase(Lieb-et-al-5-self ${Lieb5} ${Lieb5} strong-timed-bisim) + +# some self test take to long +#foreach(cur ${TCK_COMPARE_INPUT_FILES}) +# +# string(FIND ${cur} "/" last_slash REVERSE) +# math(EXPR last_slash "${last_slash}+1") +# string(SUBSTRING ${cur} ${last_slash} -1 test_name) +# string(REPLACE ".out" "-self" test_name ${test_name}) +# +# if(NOT ${no_initial} STREQUAL ${cur}) +# create_testcase(${test_name} ${cur} ${cur} strong-timed-bisim) +# endif() +# +#endforeach() tck_add_savelist(save-compare ${savelist}) diff --git a/test/tck-compare/Lieb-et-al-1-Lieb-et-al-1-diff-inv.out-expected b/test/tck-compare/Lieb-et-al-1-Lieb-et-al-1-diff-inv.out-expected new file mode 100644 index 00000000..a8111856 --- /dev/null +++ b/test/tck-compare/Lieb-et-al-1-Lieb-et-al-1-diff-inv.out-expected @@ -0,0 +1,4 @@ +MEMORY_MAX_RSS xxxx +RELATIONSHIP_FULFILLED false +RUNNING_TIME_SECONDS xxxx +VISITED_PAIR_OF_STATES 7 diff --git a/test/tck-compare/no_initial_first.out-expected b/test/tck-compare/Lieb-et-al-1-Lieb-et-al-1-non-determ-bisim.out-expected similarity index 52% rename from test/tck-compare/no_initial_first.out-expected rename to test/tck-compare/Lieb-et-al-1-Lieb-et-al-1-non-determ-bisim.out-expected index f755e384..31efe2e6 100644 --- a/test/tck-compare/no_initial_first.out-expected +++ b/test/tck-compare/Lieb-et-al-1-Lieb-et-al-1-non-determ-bisim.out-expected @@ -1,6 +1,4 @@ -DEEPEST_PATH 0 MEMORY_MAX_RSS xxxx RELATIONSHIP_FULFILLED true RUNNING_TIME_SECONDS xxxx -VISITED_PAIR_OF_STATES_STATES 0 -VISITED_TRANSITIONS 0 +VISITED_PAIR_OF_STATES 10 diff --git a/test/tck-compare/Lieb-et-al-1-Lieb-et-al-2.out-expected b/test/tck-compare/Lieb-et-al-1-Lieb-et-al-2.out-expected new file mode 100644 index 00000000..a8111856 --- /dev/null +++ b/test/tck-compare/Lieb-et-al-1-Lieb-et-al-2.out-expected @@ -0,0 +1,4 @@ +MEMORY_MAX_RSS xxxx +RELATIONSHIP_FULFILLED false +RUNNING_TIME_SECONDS xxxx +VISITED_PAIR_OF_STATES 7 diff --git a/test/tck-compare/Lieb-et-al-1-Lieb-et-al-3.out-expected b/test/tck-compare/Lieb-et-al-1-Lieb-et-al-3.out-expected new file mode 100644 index 00000000..a8111856 --- /dev/null +++ b/test/tck-compare/Lieb-et-al-1-Lieb-et-al-3.out-expected @@ -0,0 +1,4 @@ +MEMORY_MAX_RSS xxxx +RELATIONSHIP_FULFILLED false +RUNNING_TIME_SECONDS xxxx +VISITED_PAIR_OF_STATES 7 diff --git a/test/tck-compare/Lieb-et-al-1-Lieb-et-al-4.out-expected b/test/tck-compare/Lieb-et-al-1-Lieb-et-al-4.out-expected new file mode 100644 index 00000000..a8111856 --- /dev/null +++ b/test/tck-compare/Lieb-et-al-1-Lieb-et-al-4.out-expected @@ -0,0 +1,4 @@ +MEMORY_MAX_RSS xxxx +RELATIONSHIP_FULFILLED false +RUNNING_TIME_SECONDS xxxx +VISITED_PAIR_OF_STATES 7 diff --git a/test/tck-compare/Lieb-et-al-1-Lieb-et-al-5.out-expected b/test/tck-compare/Lieb-et-al-1-Lieb-et-al-5.out-expected new file mode 100644 index 00000000..781e1138 --- /dev/null +++ b/test/tck-compare/Lieb-et-al-1-Lieb-et-al-5.out-expected @@ -0,0 +1,4 @@ +MEMORY_MAX_RSS xxxx +RELATIONSHIP_FULFILLED false +RUNNING_TIME_SECONDS xxxx +VISITED_PAIR_OF_STATES 12 diff --git a/test/tck-compare/Lieb-et-al-1-non-determ-bisim.out-expected b/test/tck-compare/Lieb-et-al-1-non-determ-bisim.out-expected new file mode 100644 index 00000000..31efe2e6 --- /dev/null +++ b/test/tck-compare/Lieb-et-al-1-non-determ-bisim.out-expected @@ -0,0 +1,4 @@ +MEMORY_MAX_RSS xxxx +RELATIONSHIP_FULFILLED true +RUNNING_TIME_SECONDS xxxx +VISITED_PAIR_OF_STATES 10 diff --git a/test/tck-compare/Lieb-et-al-1-self.out-expected b/test/tck-compare/Lieb-et-al-1-self.out-expected new file mode 100644 index 00000000..24975b2e --- /dev/null +++ b/test/tck-compare/Lieb-et-al-1-self.out-expected @@ -0,0 +1,4 @@ +MEMORY_MAX_RSS xxxx +RELATIONSHIP_FULFILLED true +RUNNING_TIME_SECONDS xxxx +VISITED_PAIR_OF_STATES 7 diff --git a/test/tck-compare/Lieb-et-al-2-Lieb-et-al-2-determ-split-bisim.out-expected b/test/tck-compare/Lieb-et-al-2-Lieb-et-al-2-determ-split-bisim.out-expected new file mode 100644 index 00000000..5e696d23 --- /dev/null +++ b/test/tck-compare/Lieb-et-al-2-Lieb-et-al-2-determ-split-bisim.out-expected @@ -0,0 +1,4 @@ +MEMORY_MAX_RSS xxxx +RELATIONSHIP_FULFILLED true +RUNNING_TIME_SECONDS xxxx +VISITED_PAIR_OF_STATES 12 diff --git a/test/tck-compare/Lieb-et-al-2-Lieb-et-al-2-determ-split-non-bisim.out-expected b/test/tck-compare/Lieb-et-al-2-Lieb-et-al-2-determ-split-non-bisim.out-expected new file mode 100644 index 00000000..781e1138 --- /dev/null +++ b/test/tck-compare/Lieb-et-al-2-Lieb-et-al-2-determ-split-non-bisim.out-expected @@ -0,0 +1,4 @@ +MEMORY_MAX_RSS xxxx +RELATIONSHIP_FULFILLED false +RUNNING_TIME_SECONDS xxxx +VISITED_PAIR_OF_STATES 12 diff --git a/test/tck-compare/Lieb-et-al-2-Lieb-et-al-2-non-determ-bisim.out-expected b/test/tck-compare/Lieb-et-al-2-Lieb-et-al-2-non-determ-bisim.out-expected new file mode 100644 index 00000000..5e696d23 --- /dev/null +++ b/test/tck-compare/Lieb-et-al-2-Lieb-et-al-2-non-determ-bisim.out-expected @@ -0,0 +1,4 @@ +MEMORY_MAX_RSS xxxx +RELATIONSHIP_FULFILLED true +RUNNING_TIME_SECONDS xxxx +VISITED_PAIR_OF_STATES 12 diff --git a/test/tck-compare/Lieb-et-al-2-Lieb-et-al-3.out-expected b/test/tck-compare/Lieb-et-al-2-Lieb-et-al-3.out-expected new file mode 100644 index 00000000..24975b2e --- /dev/null +++ b/test/tck-compare/Lieb-et-al-2-Lieb-et-al-3.out-expected @@ -0,0 +1,4 @@ +MEMORY_MAX_RSS xxxx +RELATIONSHIP_FULFILLED true +RUNNING_TIME_SECONDS xxxx +VISITED_PAIR_OF_STATES 7 diff --git a/test/tck-compare/Lieb-et-al-2-Lieb-et-al-4.out-expected b/test/tck-compare/Lieb-et-al-2-Lieb-et-al-4.out-expected new file mode 100644 index 00000000..a8111856 --- /dev/null +++ b/test/tck-compare/Lieb-et-al-2-Lieb-et-al-4.out-expected @@ -0,0 +1,4 @@ +MEMORY_MAX_RSS xxxx +RELATIONSHIP_FULFILLED false +RUNNING_TIME_SECONDS xxxx +VISITED_PAIR_OF_STATES 7 diff --git a/test/tck-compare/Lieb-et-al-2-Lieb-et-al-5.out-expected b/test/tck-compare/Lieb-et-al-2-Lieb-et-al-5.out-expected new file mode 100644 index 00000000..781e1138 --- /dev/null +++ b/test/tck-compare/Lieb-et-al-2-Lieb-et-al-5.out-expected @@ -0,0 +1,4 @@ +MEMORY_MAX_RSS xxxx +RELATIONSHIP_FULFILLED false +RUNNING_TIME_SECONDS xxxx +VISITED_PAIR_OF_STATES 12 diff --git a/test/tck-compare/Lieb-et-al-2-self.out-expected b/test/tck-compare/Lieb-et-al-2-self.out-expected new file mode 100644 index 00000000..24975b2e --- /dev/null +++ b/test/tck-compare/Lieb-et-al-2-self.out-expected @@ -0,0 +1,4 @@ +MEMORY_MAX_RSS xxxx +RELATIONSHIP_FULFILLED true +RUNNING_TIME_SECONDS xxxx +VISITED_PAIR_OF_STATES 7 diff --git a/test/tck-compare/Lieb-et-al-3-Lieb-et-al-4.out-expected b/test/tck-compare/Lieb-et-al-3-Lieb-et-al-4.out-expected new file mode 100644 index 00000000..a8111856 --- /dev/null +++ b/test/tck-compare/Lieb-et-al-3-Lieb-et-al-4.out-expected @@ -0,0 +1,4 @@ +MEMORY_MAX_RSS xxxx +RELATIONSHIP_FULFILLED false +RUNNING_TIME_SECONDS xxxx +VISITED_PAIR_OF_STATES 7 diff --git a/test/tck-compare/Lieb-et-al-3-Lieb-et-al-5.out-expected b/test/tck-compare/Lieb-et-al-3-Lieb-et-al-5.out-expected new file mode 100644 index 00000000..781e1138 --- /dev/null +++ b/test/tck-compare/Lieb-et-al-3-Lieb-et-al-5.out-expected @@ -0,0 +1,4 @@ +MEMORY_MAX_RSS xxxx +RELATIONSHIP_FULFILLED false +RUNNING_TIME_SECONDS xxxx +VISITED_PAIR_OF_STATES 12 diff --git a/test/tck-compare/Lieb-et-al-3-self.out-expected b/test/tck-compare/Lieb-et-al-3-self.out-expected new file mode 100644 index 00000000..24975b2e --- /dev/null +++ b/test/tck-compare/Lieb-et-al-3-self.out-expected @@ -0,0 +1,4 @@ +MEMORY_MAX_RSS xxxx +RELATIONSHIP_FULFILLED true +RUNNING_TIME_SECONDS xxxx +VISITED_PAIR_OF_STATES 7 diff --git a/test/tck-compare/Lieb-et-al-4-Lieb-et-al-5.out-expected b/test/tck-compare/Lieb-et-al-4-Lieb-et-al-5.out-expected new file mode 100644 index 00000000..781e1138 --- /dev/null +++ b/test/tck-compare/Lieb-et-al-4-Lieb-et-al-5.out-expected @@ -0,0 +1,4 @@ +MEMORY_MAX_RSS xxxx +RELATIONSHIP_FULFILLED false +RUNNING_TIME_SECONDS xxxx +VISITED_PAIR_OF_STATES 12 diff --git a/test/tck-compare/Lieb-et-al-4-self.out-expected b/test/tck-compare/Lieb-et-al-4-self.out-expected new file mode 100644 index 00000000..24975b2e --- /dev/null +++ b/test/tck-compare/Lieb-et-al-4-self.out-expected @@ -0,0 +1,4 @@ +MEMORY_MAX_RSS xxxx +RELATIONSHIP_FULFILLED true +RUNNING_TIME_SECONDS xxxx +VISITED_PAIR_OF_STATES 7 diff --git a/test/tck-compare/Lieb-et-al-5-self.out-expected b/test/tck-compare/Lieb-et-al-5-self.out-expected new file mode 100644 index 00000000..97a2aae4 --- /dev/null +++ b/test/tck-compare/Lieb-et-al-5-self.out-expected @@ -0,0 +1,4 @@ +MEMORY_MAX_RSS xxxx +RELATIONSHIP_FULFILLED true +RUNNING_TIME_SECONDS xxxx +VISITED_PAIR_OF_STATES 22 diff --git a/test/tck-compare/easy-ad94-added-transition-easy-ad94.out-expected b/test/tck-compare/easy-ad94-added-transition-easy-ad94.out-expected new file mode 100644 index 00000000..99d08c5e --- /dev/null +++ b/test/tck-compare/easy-ad94-added-transition-easy-ad94.out-expected @@ -0,0 +1,4 @@ +MEMORY_MAX_RSS xxxx +RELATIONSHIP_FULFILLED false +RUNNING_TIME_SECONDS xxxx +VISITED_PAIR_OF_STATES 6 diff --git a/test/tck-compare/easy-ad94-different-guard-easy-ad94-added-transition.out-expected b/test/tck-compare/easy-ad94-different-guard-easy-ad94-added-transition.out-expected new file mode 100644 index 00000000..b4177db5 --- /dev/null +++ b/test/tck-compare/easy-ad94-different-guard-easy-ad94-added-transition.out-expected @@ -0,0 +1,4 @@ +MEMORY_MAX_RSS xxxx +RELATIONSHIP_FULFILLED false +RUNNING_TIME_SECONDS xxxx +VISITED_PAIR_OF_STATES 5 diff --git a/test/tck-compare/easy-ad94-different-guard-easy-ad94.out-expected b/test/tck-compare/easy-ad94-different-guard-easy-ad94.out-expected new file mode 100644 index 00000000..b4177db5 --- /dev/null +++ b/test/tck-compare/easy-ad94-different-guard-easy-ad94.out-expected @@ -0,0 +1,4 @@ +MEMORY_MAX_RSS xxxx +RELATIONSHIP_FULFILLED false +RUNNING_TIME_SECONDS xxxx +VISITED_PAIR_OF_STATES 5 diff --git a/test/tck-compare/easy-ad94-easy-ad94-added-transition.out-expected b/test/tck-compare/easy-ad94-easy-ad94-added-transition.out-expected new file mode 100644 index 00000000..99d08c5e --- /dev/null +++ b/test/tck-compare/easy-ad94-easy-ad94-added-transition.out-expected @@ -0,0 +1,4 @@ +MEMORY_MAX_RSS xxxx +RELATIONSHIP_FULFILLED false +RUNNING_TIME_SECONDS xxxx +VISITED_PAIR_OF_STATES 6 diff --git a/test/tck-compare/easy-ad94-self-added-transition.out-expected b/test/tck-compare/easy-ad94-self-added-transition.out-expected new file mode 100644 index 00000000..03a58315 --- /dev/null +++ b/test/tck-compare/easy-ad94-self-added-transition.out-expected @@ -0,0 +1,4 @@ +MEMORY_MAX_RSS xxxx +RELATIONSHIP_FULFILLED true +RUNNING_TIME_SECONDS xxxx +VISITED_PAIR_OF_STATES 8 diff --git a/test/tck-compare/easy-ad94-self-different-guard.out-expected b/test/tck-compare/easy-ad94-self-different-guard.out-expected new file mode 100644 index 00000000..ab728476 --- /dev/null +++ b/test/tck-compare/easy-ad94-self-different-guard.out-expected @@ -0,0 +1,4 @@ +MEMORY_MAX_RSS xxxx +RELATIONSHIP_FULFILLED true +RUNNING_TIME_SECONDS xxxx +VISITED_PAIR_OF_STATES 6 diff --git a/test/tck-compare/easy-ad94-self.out-expected b/test/tck-compare/easy-ad94-self.out-expected new file mode 100644 index 00000000..ab728476 --- /dev/null +++ b/test/tck-compare/easy-ad94-self.out-expected @@ -0,0 +1,4 @@ +MEMORY_MAX_RSS xxxx +RELATIONSHIP_FULFILLED true +RUNNING_TIME_SECONDS xxxx +VISITED_PAIR_OF_STATES 6 diff --git a/test/tck-compare/no_initial_first.err-expected b/test/tck-compare/no_initial_first.err-expected index abca882d..3191e0dc 100644 --- a/test/tck-compare/no_initial_first.err-expected +++ b/test/tck-compare/no_initial_first.err-expected @@ -1 +1,2 @@ -WARNING: the first system has no initial state +ERROR: Currently, strong timed bisim is supported with exactly a single initial location per process, only +a process of missing_initial has no initial location diff --git a/test/tck-compare/no_initial_second.err-expected b/test/tck-compare/no_initial_second.err-expected index 990ff738..3191e0dc 100644 --- a/test/tck-compare/no_initial_second.err-expected +++ b/test/tck-compare/no_initial_second.err-expected @@ -1 +1,2 @@ -WARNING: the second system has no initial state +ERROR: Currently, strong timed bisim is supported with exactly a single initial location per process, only +a process of missing_initial has no initial location diff --git a/test/tck-compare/no_initial_second.out-expected b/test/tck-compare/no_initial_second.out-expected index f755e384..e69de29b 100644 --- a/test/tck-compare/no_initial_second.out-expected +++ b/test/tck-compare/no_initial_second.out-expected @@ -1,6 +0,0 @@ -DEEPEST_PATH 0 -MEMORY_MAX_RSS xxxx -RELATIONSHIP_FULFILLED true -RUNNING_TIME_SECONDS xxxx -VISITED_PAIR_OF_STATES_STATES 0 -VISITED_TRANSITIONS 0 diff --git a/test/tck-compare/tck-compare-Lieb_et_al_1.out-expected b/test/tck-compare/tck-compare-Lieb_et_al_1.out-expected new file mode 100644 index 00000000..5bd2fc69 --- /dev/null +++ b/test/tck-compare/tck-compare-Lieb_et_al_1.out-expected @@ -0,0 +1,19 @@ +# This file is a part of the TChecker project. +# +# See files AUTHORS and LICENSE for copyright details. + +system:Lieb_et_al_A1 + +clock:1:x + +event:a +event:b +event:c + +process:P +location:P:A{initial:} +location:P:B{invariant: x<2} +location:P:C{} +edge:P:A:B:a{provided: x<=0} +edge:P:B:C:b{} +edge:P:C:A:c{provided: x>3 : do: x=0} diff --git a/test/tck-compare/tck-compare-Lieb_et_al_1_diff_invariant.out-expected b/test/tck-compare/tck-compare-Lieb_et_al_1_diff_invariant.out-expected new file mode 100644 index 00000000..f880645e --- /dev/null +++ b/test/tck-compare/tck-compare-Lieb_et_al_1_diff_invariant.out-expected @@ -0,0 +1,19 @@ +# This file is a part of the TChecker project. +# +# See files AUTHORS and LICENSE for copyright details. + +system:Lieb_et_al_A1 + +clock:1:x + +event:a +event:b +event:c + +process:P +location:P:A{initial:} +location:P:B{invariant: x<3} +location:P:C{} +edge:P:A:B:a{provided: x<=0} +edge:P:B:C:b{} +edge:P:C:A:c{provided: x>3 : do: x=0} diff --git a/test/tck-compare/tck-compare-Lieb_et_al_1_non_determ_bisim.out-expected b/test/tck-compare/tck-compare-Lieb_et_al_1_non_determ_bisim.out-expected new file mode 100644 index 00000000..e2c021ac --- /dev/null +++ b/test/tck-compare/tck-compare-Lieb_et_al_1_non_determ_bisim.out-expected @@ -0,0 +1,22 @@ +# This file is a part of the TChecker project. +# +# See files AUTHORS and LICENSE for copyright details. + +system:Lieb_et_al_A1 + +clock:1:x + +event:a +event:b +event:c + +process:P +location:P:A{initial:} +location:P:B{invariant: x<2} +location:P:C{} +location:P:CPrime{} +edge:P:A:B:a{provided: x<=0} +edge:P:B:C:b{provided: x<=1} +edge:P:B:CPrime:b{provided:x>1} +edge:P:C:A:c{provided: x>3 : do: x=0} +edge:P:CPrime:A:c{provided: x>3 : do: x=0} diff --git a/test/tck-compare/tck-compare-Lieb_et_al_2.out-expected b/test/tck-compare/tck-compare-Lieb_et_al_2.out-expected new file mode 100644 index 00000000..26c15aaa --- /dev/null +++ b/test/tck-compare/tck-compare-Lieb_et_al_2.out-expected @@ -0,0 +1,19 @@ +# This file is a part of the TChecker project. +# +# See files AUTHORS and LICENSE for copyright details. + +system:Lieb_et_al_A1 + +clock:1:x + +event:a +event:b +event:c + +process:P +location:P:A{initial:} +location:P:B{invariant: x<2} +location:P:C{} +edge:P:A:B:a{do: x=0} +edge:P:B:C:b{} +edge:P:C:A:c{provided: x>3 : do: x=0} diff --git a/test/tck-compare/tck-compare-Lieb_et_al_2_determ_split_bisim.out-expected b/test/tck-compare/tck-compare-Lieb_et_al_2_determ_split_bisim.out-expected new file mode 100644 index 00000000..5b63a54c --- /dev/null +++ b/test/tck-compare/tck-compare-Lieb_et_al_2_determ_split_bisim.out-expected @@ -0,0 +1,24 @@ +# This file is a part of the TChecker project. +# +# See files AUTHORS and LICENSE for copyright details. + +system:Lieb_et_al_A2_determ_split_bisim + +clock:1:x + +event:a +event:b +event:c + +process:P +location:P:A{initial:} +location:P:B{invariant: x<2} +location:P:BPrime{invariant: x<2} +location:P:C{} +location:P:CPrime{} +edge:P:A:B:a{provided: x<2 : do: x=0} +edge:P:A:BPrime:a{provided: x>=2 : do: x=0} +edge:P:B:C:b{} +edge:P:BPrime:CPrime:b{} +edge:P:C:A:c{provided: x>3 : do: x=0} +edge:P:CPrime:A:c{provided: x>3 : do: x=0} diff --git a/test/tck-compare/tck-compare-Lieb_et_al_2_determ_split_non_bisim.out-expected b/test/tck-compare/tck-compare-Lieb_et_al_2_determ_split_non_bisim.out-expected new file mode 100644 index 00000000..c45da91c --- /dev/null +++ b/test/tck-compare/tck-compare-Lieb_et_al_2_determ_split_non_bisim.out-expected @@ -0,0 +1,24 @@ +# This file is a part of the TChecker project. +# +# See files AUTHORS and LICENSE for copyright details. + +system:Lieb_et_al_A2_determ_split_non_bisim + +clock:1:x + +event:a +event:b +event:c + +process:P +location:P:A{initial:} +location:P:B{invariant: x<2} +location:P:BPrime{invariant: x<2} +location:P:C{} +location:P:CPrime{} +edge:P:A:B:a{provided: x<2 : do: x=0} +edge:P:A:BPrime:a{provided: x>2 : do: x=0} +edge:P:B:C:b{} +edge:P:BPrime:CPrime:b{} +edge:P:C:A:c{provided: x>3 : do: x=0} +edge:P:CPrime:A:c{provided: x>3 : do: x=0} diff --git a/test/tck-compare/tck-compare-Lieb_et_al_2_non_determ_bisim.out-expected b/test/tck-compare/tck-compare-Lieb_et_al_2_non_determ_bisim.out-expected new file mode 100644 index 00000000..fee66d3c --- /dev/null +++ b/test/tck-compare/tck-compare-Lieb_et_al_2_non_determ_bisim.out-expected @@ -0,0 +1,24 @@ +# This file is a part of the TChecker project. +# +# See files AUTHORS and LICENSE for copyright details. + +system:Lieb_et_al_A2_non_determ_bisim + +clock:1:x + +event:a +event:b +event:c + +process:P +location:P:A{initial:} +location:P:B{invariant: x<2} +location:P:BPrime{invariant: x<2} +location:P:C{} +location:P:CPrime{} +edge:P:A:B:a{provided: x<2 : do: x=0} +edge:P:A:BPrime:a{provided: x>=1 : do: x=0} +edge:P:B:C:b{} +edge:P:BPrime:CPrime:b{} +edge:P:C:A:c{provided: x>3 : do: x=0} +edge:P:CPrime:A:c{provided: x>3 : do: x=0} diff --git a/test/tck-compare/tck-compare-Lieb_et_al_3.out-expected b/test/tck-compare/tck-compare-Lieb_et_al_3.out-expected new file mode 100644 index 00000000..d0c518a0 --- /dev/null +++ b/test/tck-compare/tck-compare-Lieb_et_al_3.out-expected @@ -0,0 +1,20 @@ +# This file is a part of the TChecker project. +# +# See files AUTHORS and LICENSE for copyright details. + +system:Lieb_et_al_A1 + +clock:1:x +clock:1:y + +event:a +event:b +event:c + +process:P +location:P:A{initial:} +location:P:B{invariant: x<2} +location:P:C{} +edge:P:A:B:a{do: x=0;y=0} +edge:P:B:C:b{} +edge:P:C:A:c{provided: y>3 : do: x=0;y=0} diff --git a/test/tck-compare/tck-compare-Lieb_et_al_4.out-expected b/test/tck-compare/tck-compare-Lieb_et_al_4.out-expected new file mode 100644 index 00000000..14929e25 --- /dev/null +++ b/test/tck-compare/tck-compare-Lieb_et_al_4.out-expected @@ -0,0 +1,20 @@ +# This file is a part of the TChecker project. +# +# See files AUTHORS and LICENSE for copyright details. + +system:Lieb_et_al_A1 + +clock:1:x +clock:1:y + +event:a +event:b +event:c + +process:P +location:P:A{initial:} +location:P:B{invariant: x<2} +location:P:C{} +edge:P:A:B:a{do: x=0} +edge:P:B:C:b{do:y=0} +edge:P:C:A:c{provided: y>3 : do: x=0;y=0} diff --git a/test/tck-compare/tck-compare-Lieb_et_al_5.out-expected b/test/tck-compare/tck-compare-Lieb_et_al_5.out-expected new file mode 100644 index 00000000..dffa5ec5 --- /dev/null +++ b/test/tck-compare/tck-compare-Lieb_et_al_5.out-expected @@ -0,0 +1,27 @@ +# This file is a part of the TChecker project. +# +# See files AUTHORS and LICENSE for copyright details. + +system:Lieb_et_al_A1 + +clock:1:x +clock:1:y + +event:a +event:b +event:c + +process:P +location:P:A{initial:} +location:P:B{invariant: x<2} +location:P:C{} +location:P:BPrime{invariant: x<2} +location:P:CPrime{} + +edge:P:A:B:a{do: x=0} +edge:P:B:C:b{do: y=0} +edge:P:C:A:c{provided: y>3 : do: x=0;y=0} + +edge:P:A:BPrime:a{do: x=0;y=0} +edge:P:BPrime:CPrime:b{} +edge:P:CPrime:A:c{provided: y>3 : do: x=0;y=0} diff --git a/test/tck-compare/tck-compare-ad94-self.out-expected b/test/tck-compare/tck-compare-ad94-self.out-expected new file mode 100644 index 00000000..56e77a93 --- /dev/null +++ b/test/tck-compare/tck-compare-ad94-self.out-expected @@ -0,0 +1,4 @@ +MEMORY_MAX_RSS xxxx +RELATIONSHIP_FULFILLED true +RUNNING_TIME_SECONDS xxxx +VISITED_PAIR_OF_STATES 46 diff --git a/test/tck-compare/tck-compare-ad94_Long.out-expected b/test/tck-compare/tck-compare-ad94_Long.out-expected new file mode 100644 index 00000000..61fb0c1e --- /dev/null +++ b/test/tck-compare/tck-compare-ad94_Long.out-expected @@ -0,0 +1,26 @@ +# labels=green +# This file is a part of the TChecker project. +# +# See files AUTHORS and LICENSE for copyright details. + +system:ad94_fig10_longVersion + +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=0} +edge:P:l1:l2:b{provided: y==10000000000} +edge:P:l1:l3:c{provided: x<10000000000} +edge:P:l2:l3:c{provided: x<10000000000} +edge:P:l3:l1:a{provided: y<10000000000 : do:y=0} +edge:P:l3:l3:d{provided: x>10000000000} diff --git a/test/tck-compare/tck-compare-count_to_inf.out-expected b/test/tck-compare/tck-compare-count_to_inf.out-expected new file mode 100644 index 00000000..34e122ac --- /dev/null +++ b/test/tck-compare/tck-compare-count_to_inf.out-expected @@ -0,0 +1,20 @@ +# This file is a part of the TChecker project. +# +# See files AUTHORS and LICENSE for copyright details. + +system:count_to_inf + +clock:1:x +clock:1:y + +event:a +event:b +event:c + +process:P +location:P:A{initial:} +location:P:B{invariant: y<1} +location:P:C{invariant: x<=2} +edge:P:A:B:a{do: x=0;y=0} +edge:P:B:C:b{do: x=0;y=0} +edge:P:C:C:c{provided: x>=2 : do: x=0} diff --git a/test/tck-compare/tck-compare-easy-ad94-added-transition.out-expected b/test/tck-compare/tck-compare-easy-ad94-added-transition.out-expected new file mode 100644 index 00000000..61504d2b --- /dev/null +++ b/test/tck-compare/tck-compare-easy-ad94-added-transition.out-expected @@ -0,0 +1,23 @@ +# labels=green +# This file is a part of the TChecker project. +# +# See files AUTHORS and LICENSE for copyright details. + +system:easy_ad94_added_transition_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: x=0; y=0} +edge:P:l1:l2:b{provided: y==1 && x<=2 } +edge:P:l1:l2:c{ } diff --git a/test/tck-compare/tck-compare-easy-ad94-different-guard.out-expected b/test/tck-compare/tck-compare-easy-ad94-different-guard.out-expected new file mode 100644 index 00000000..0f4bc6de --- /dev/null +++ b/test/tck-compare/tck-compare-easy-ad94-different-guard.out-expected @@ -0,0 +1,22 @@ +# labels=green +# This file is a part of the TChecker project. +# +# See files AUTHORS and LICENSE for copyright details. + +system:easy_ad94_different_guard_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: x=0; y=0} +edge:P:l1:l2:b{provided: y==2 && x<=2 } diff --git a/test/tck-compare/tck-compare-easy-ad94.out-expected b/test/tck-compare/tck-compare-easy-ad94.out-expected new file mode 100644 index 00000000..6a976b50 --- /dev/null +++ b/test/tck-compare/tck-compare-easy-ad94.out-expected @@ -0,0 +1,22 @@ +# labels=green +# This file is a part of the TChecker project. +# +# See files AUTHORS and LICENSE for copyright details. + +system:easy_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: x=0; y=0} +edge:P:l1:l2:b{provided: y==1 && x<=2 } diff --git a/test/tck-compare/tck-compare-no_initial_first.out-expected b/test/tck-compare/tck-compare-no_initial_first.out-expected new file mode 100644 index 00000000..e69de29b diff --git a/test/unit-tests/test-db.hh b/test/unit-tests/test-db.hh index b3591d48..ea11c524 100644 --- a/test/unit-tests/test-db.hh +++ b/test/unit-tests/test-db.hh @@ -70,12 +70,16 @@ TEST_CASE("construction of upper bounds", "[db]") SECTION("non representable upper bounds") { - REQUIRE_THROWS_AS(DB(tchecker::LT, max_int_used), std::invalid_argument); REQUIRE_THROWS_AS(DB(tchecker::LT, max_int_used + 1), std::invalid_argument); REQUIRE_THROWS_AS(DB(tchecker::LT, min_int_used - 1), std::invalid_argument); REQUIRE_NOTHROW(DB(tchecker::LT, max_int_used - 1)); REQUIRE_NOTHROW(DB(tchecker::LT, min_int_used)); } + + SECTION("Lower than infinity test") + { + REQUIRE(DB(tchecker::LT, max_int_used) == tchecker::dbm::LT_INFINITY); + } } TEST_CASE("hash values of upper bounds", "[db]") diff --git a/test/unit-tests/test-dbm.hh b/test/unit-tests/test-dbm.hh index 9603c996..76819de2 100644 --- a/test/unit-tests/test-dbm.hh +++ b/test/unit-tests/test-dbm.hh @@ -453,6 +453,76 @@ TEST_CASE("tighten (full)", "[dbm]") REQUIRE(DBM(2, 2) == tchecker::dbm::LE_ZERO); } + SECTION("tighten another non-empty, dim>1") + { + // Build DBM + tchecker::clock_id_t dim = 5; + tchecker::dbm::db_t dbm[dim * dim]; + + DBM(0, 0) = tchecker::dbm::LE_ZERO; + DBM(1, 0) = tchecker::dbm::LT_INFINITY; // x1=-MAX_VALUE + DBM(1, 1) = tchecker::dbm::LE_ZERO; + DBM(2, 1) = tchecker::dbm::LE_ZERO; + DBM(3, 1) = tchecker::dbm::LE_ZERO; + DBM(4, 1) = tchecker::dbm::LE_ZERO; + + DBM(0, 2) = tchecker::dbm::LE_ZERO; + DBM(1, 2) = tchecker::dbm::LE_ZERO; + DBM(2, 2) = tchecker::dbm::LE_ZERO; + DBM(3, 2) = tchecker::dbm::LE_ZERO; + DBM(4, 2) = tchecker::dbm::LE_ZERO; + + DBM(0, 3) = tchecker::dbm::LE_ZERO; + DBM(1, 3) = tchecker::dbm::LE_ZERO; + DBM(2, 3) = tchecker::dbm::LE_ZERO; + DBM(3, 3) = tchecker::dbm::LE_ZERO; + DBM(4, 3) = tchecker::dbm::LE_ZERO; + + DBM(0, 4) = tchecker::dbm::LE_ZERO; + DBM(1, 4) = tchecker::dbm::LE_ZERO; + DBM(2, 4) = tchecker::dbm::LE_ZERO; + DBM(3, 4) = tchecker::dbm::LE_ZERO; + DBM(4, 4) = tchecker::dbm::LE_ZERO; + + REQUIRE(tchecker::dbm::tighten(dbm, dim) == tchecker::dbm::NON_EMPTY); + REQUIRE(tchecker::dbm::is_tight(dbm, dim)); + + REQUIRE(DBM(0, 0) == tchecker::dbm::LE_ZERO); + REQUIRE(DBM(1, 0) == tchecker::dbm::LT_INFINITY); + REQUIRE(DBM(2, 0) == tchecker::dbm::LT_INFINITY); + REQUIRE(DBM(3, 0) == tchecker::dbm::LT_INFINITY); + REQUIRE(DBM(4, 0) == tchecker::dbm::LT_INFINITY); + + REQUIRE(DBM(0, 1) == tchecker::dbm::LE_ZERO); + REQUIRE(DBM(1, 1) == tchecker::dbm::LE_ZERO); + REQUIRE(DBM(2, 1) == tchecker::dbm::LE_ZERO); + REQUIRE(DBM(3, 1) == tchecker::dbm::LE_ZERO); + REQUIRE(DBM(4, 1) == tchecker::dbm::LE_ZERO); + + REQUIRE(DBM(0, 2) == tchecker::dbm::LE_ZERO); + REQUIRE(DBM(1, 2) == tchecker::dbm::LE_ZERO); + REQUIRE(DBM(2, 2) == tchecker::dbm::LE_ZERO); + REQUIRE(DBM(3, 2) == tchecker::dbm::LE_ZERO); + REQUIRE(DBM(4, 2) == tchecker::dbm::LE_ZERO); + + REQUIRE(DBM(0, 3) == tchecker::dbm::LE_ZERO); + REQUIRE(DBM(1, 3) == tchecker::dbm::LE_ZERO); + REQUIRE(DBM(2, 3) == tchecker::dbm::LE_ZERO); + REQUIRE(DBM(3, 3) == tchecker::dbm::LE_ZERO); + REQUIRE(DBM(4, 3) == tchecker::dbm::LE_ZERO); + + REQUIRE(DBM(0, 4) == tchecker::dbm::LE_ZERO); + REQUIRE(DBM(1, 4) == tchecker::dbm::LE_ZERO); + REQUIRE(DBM(2, 4) == tchecker::dbm::LE_ZERO); + REQUIRE(DBM(3, 4) == tchecker::dbm::LE_ZERO); + REQUIRE(DBM(4, 4) == tchecker::dbm::LE_ZERO); + } + SECTION("tighten empty, dim>1") { // Build DBM diff --git a/test/unit-tests/test-virtual_constraint.hh b/test/unit-tests/test-virtual_constraint.hh new file mode 100644 index 00000000..9654ceec --- /dev/null +++ b/test/unit-tests/test-virtual_constraint.hh @@ -0,0 +1,15 @@ +/* + * This file is a part of the TChecker project. + * + * See files AUTHORS and LICENSE for copyright details. + * + */ + #include "tchecker/zg/zone.hh" + #include "tchecker/vcg/virtual_constraint.hh" + + + TEST_CASE ("Extract virtual constraint", "[evc]") { + std::shared_ptrzone = tchecker::zg::factory(5); + std::shared_ptr vc = tchecker::virtual_constraint::factory(zone, 2); + REQUIRE(vc->get_no_of_virt_clocks() == 2); + } \ No newline at end of file diff --git a/test/unit-tests/unittest.cc b/test/unit-tests/unittest.cc index 03d5aa3a..de2e2ff0 100644 --- a/test/unit-tests/unittest.cc +++ b/test/unit-tests/unittest.cc @@ -26,5 +26,6 @@ #include "test-reference_clock_variables.hh" #include "test-refzg-semantics.hh" #include "test-variables-access.hh" +#include "test-virtual_constraint.hh" #include "test-waiting.hh" #include "test-zg-semantics.hh"