Include example directory in zip creation

.github/actions/benchexec-test/action.yml

@@ -51,7 +51,7 @@ runs:
       run: |
         benchexec svcomp23-witness-benchmarks/concurrentwitness2test.xml -N 10 --no-container --tool-directory ConcurrentWitness2Test -t ConcurrencySafety-${{ inputs.tool }}
     - name: Upload results
-      uses: actions/upload-artifact@0b7f8abb1508181956e8e162db84b466c27e18ce # v3.1.2
+      uses: actions/upload-artifact@v4
       with:
         name: ${{ inputs.tool }}
         path: results

.github/actions/create-archive/action.yml

@@ -19,10 +19,10 @@ runs:
       shell: bash
       run: |
         mkdir ConcurrentWitness2Test
-        cp venv *.py *.md LICENSE requirements.txt svcomp.c start.sh ConcurrentWitness2Test/ -r
+        cp venv *.py *.md LICENSE requirements.txt svcomp.c *.sh example ConcurrentWitness2Test/ -r
         zip ConcurrentWitness2Test.zip ConcurrentWitness2Test -r
     - name: Upload results
-      uses: actions/upload-artifact@0b7f8abb1508181956e8e162db84b466c27e18ce # v3.1.2
+      uses: actions/upload-artifact@v4
       with:
         name: ConcurrentWitness2Test
         path: ConcurrentWitness2Test.zip

Exceptions.py

@@ -1,17 +1,17 @@
 """
-    Copyright 2023 Budapest University of Technology and Economics
+Copyright 2023 Budapest University of Technology and Economics
 
-    Licensed under the Apache License, Version 2.0 (the "License");
-    you may not use this file except in compliance with the License.
-    You may obtain a copy of the License at
+Licensed under the Apache License, Version 2.0 (the "License");
+you may not use this file except in compliance with the License.
+You may obtain a copy of the License at
 
-        http://www.apache.org/licenses/LICENSE-2.0
+    http://www.apache.org/licenses/LICENSE-2.0
 
-    Unless required by applicable law or agreed to in writing, software
-    distributed under the License is distributed on an "AS IS" BASIS,
-    WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
-    See the License for the specific language governing permissions and
-    limitations under the License.
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
 """
 
 

main.py

@@ -1,17 +1,17 @@
 """
-    Copyright 2023 Budapest University of Technology and Economics
+Copyright 2023 Budapest University of Technology and Economics
 
-    Licensed under the Apache License, Version 2.0 (the "License");
-    you may not use this file except in compliance with the License.
-    You may obtain a copy of the License at
+Licensed under the Apache License, Version 2.0 (the "License");
+you may not use this file except in compliance with the License.
+You may obtain a copy of the License at
 
-        http://www.apache.org/licenses/LICENSE-2.0
+    http://www.apache.org/licenses/LICENSE-2.0
 
-    Unless required by applicable law or agreed to in writing, software
-    distributed under the License is distributed on an "AS IS" BASIS,
-    WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
-    See the License for the specific language governing permissions and
-    limitations under the License.
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
 """
 
 import os

smoketest.sh

@@ -0,0 +1,2 @@
+#!/bin/bash
+./start.sh example/mix000.opt.i --witness example/mix000.opt.i.graphml --mode permissive

svcomp.c

@@ -34,7 +34,7 @@ void reach_error() {
     exit(74);
 }
 
-atomic_int c2tt_global_counter = ATOMIC_VAR_INIT(0);
+atomic_int c2tt_global_counter = 0;
 mtx_t c2tt_mtx;
 cnd_t c2tt_cv;
 _Bool c2tt_init;

tweaks.py

@@ -1,17 +1,17 @@
 """
-    Copyright 2023 Budapest University of Technology and Economics
+Copyright 2023 Budapest University of Technology and Economics
 
-    Licensed under the Apache License, Version 2.0 (the "License");
-    you may not use this file except in compliance with the License.
-    You may obtain a copy of the License at
+Licensed under the Apache License, Version 2.0 (the "License");
+you may not use this file except in compliance with the License.
+You may obtain a copy of the License at
 
-        http://www.apache.org/licenses/LICENSE-2.0
+    http://www.apache.org/licenses/LICENSE-2.0
 
-    Unless required by applicable law or agreed to in writing, software
-    distributed under the License is distributed on an "AS IS" BASIS,
-    WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
-    See the License for the specific language governing permissions and
-    limitations under the License.
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
 """
 
 from pycparser.c_ast import FuncDef, Decl, Struct, TypeDecl

witness2ast.py

@@ -1,17 +1,17 @@
 """
-    Copyright 2023 Budapest University of Technology and Economics
+Copyright 2023 Budapest University of Technology and Economics
 
-    Licensed under the Apache License, Version 2.0 (the "License");
-    you may not use this file except in compliance with the License.
-    You may obtain a copy of the License at
+Licensed under the Apache License, Version 2.0 (the "License");
+you may not use this file except in compliance with the License.
+You may obtain a copy of the License at
 
-        http://www.apache.org/licenses/LICENSE-2.0
+    http://www.apache.org/licenses/LICENSE-2.0
 
-    Unless required by applicable law or agreed to in writing, software
-    distributed under the License is distributed on an "AS IS" BASIS,
-    WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
-    See the License for the specific language governing permissions and
-    limitations under the License.
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
 """
 
 import networkx as nx