very first working version

added more system tests

added test

wip

wip

wip

rename

added oracle for 64bit

first version

wip

wip

.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"

CppCheckSuppressions.txt

@@ -4,12 +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
-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

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

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"
+

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"
+

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"
+

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"
+

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"
+

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"
+

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"
+

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"
+

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"
+

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"
+

examples/count_to_inf.sh

@@ -0,0 +1 @@
+cat "$(dirname $0)/count_to_inf.txt"

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}

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"

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"

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"

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}

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}

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}

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}

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}

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}

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}

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}

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}