Specification fix: ensure that the initial thread can be referenced

With the previous specification, the initially active thread (as created
by starting a program) could not be referenced in transitions without
violating the specification (only threads specified in createThread
could be referenced).

Includes a revert of 1a83971, as the
check can now proceed as the ambiguity is resolved.

README.md

@@ -76,8 +76,8 @@ The following information should additionally be available in the witness:
 
 | key | Meaning | Allowed in Violation Witnesses | Allowed in Correctness Witnesses |
 | --- | --- | ---- | ---- |
-| threadId | Represents the currently active thread for the transition. If no ``threadId`` is given, any thread can be active. The value should be a unique identififer for a thread. | Yes | Yes |
-| createThread | The currently active thread (value of ``threadId``) creates a new thread (value of ``createThread``) . In general, using a ``threadId`` is only allowed after creating a matching thread. The new thread's function can be entered on a second transition following this transition, such that the transition with the ``enterFunction`` key has the ``threadId`` of the created thread. When the function of the thread is exited, the thread is assumed to be terminated and its ``threadId`` should no longer be used. | Yes | Yes |
+| threadId | Represents the currently active thread for the transition. The initially active thread has id ``0``. If no ``threadId`` is given, any thread can be active. The value should be a unique identififer for a thread. | Yes | Yes |
+| createThread | The currently active thread (value of ``threadId``) creates a new thread (value of ``createThread``) . In general, using a ``threadId`` is only allowed after creating a matching thread, except for thread ``0``, which exits by virtue of starting the program. The new thread's function can be entered on a second transition following this transition, such that the transition with the ``enterFunction`` key has the ``threadId`` of the created thread. When the function of the thread is exited, the thread is assumed to be terminated and its ``threadId`` should no longer be used. | Yes | Yes |
 
 CPAchecker partially supports the validation of violation witnesses for concurrent programs.
 This witness specification and the validator are a work in progress and will be subject to modifications.

lint/witnesslint/linter.py

@@ -124,6 +124,7 @@ def __init__(self, witness, program, options):
         self.correctness_witness_only = set()
         self.check_existence_later = set()
         self.check_later = []
+        self.witness.threads['0'] = None
 
     def collect_program_info(self, program):
         """
@@ -440,15 +441,11 @@ def handle_edge_data(self, data, key, parent):
                     break
             self.check_functionname(data.text, data.sourceline)
         elif key == witness.THREADID:
-            # Check disabled for SV-COMP'21 as questions about the specification
-            # need to be resolved first, see
-            # https://gitlab.com/sosy-lab/sv-comp/archives-2021/-/issues/30
-            # if data.text not in self.witness.threads:
-            #     logging.warning(
-            #         "Thread with id {} doesn't exist".format(data.text),
-            #         data.sourceline,
-            #     )
-            pass
+            if data.text not in self.witness.threads:
+                logging.warning(
+                    "Thread with id {} doesn't exist".format(data.text),
+                    data.sourceline,
+                )
         elif key == witness.CREATETHREAD:
             if data.text in self.witness.threads:
                 logging.warning(