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

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):
         """