Slightly change tasks syntax

Signed-off-by: Clifford Wolf <clifford@clifford.at>

diff --git a/docs/source/reference.rst b/docs/source/reference.rst
index 2d37263a8ef8da1404c4393b69f991e450df4a4a..4f0b67f45b3071a3606748a7a7457bba7f57bde2 100644 (file)
--- a/docs/source/reference.rst
+++ b/docs/source/reference.rst
@@ -10,8 +10,8 @@ is for the most part irrelevant, but by convention the usual order is
 Tasks section
 -------------
 
-The ``[tasks]`` section can be used to configure multiple verification tasks in only
-one ``.sby`` file. Each line in the ``[tasks]`` section configures one task. For example:
+The optional ``[tasks]`` section can be used to configure multiple verification tasks in
+a single ``.sby`` file. Each line in the ``[tasks]`` section configures one task. For example:
 
 .. code-block:: text
 
@@ -43,8 +43,8 @@ tasks or task groups:
    task_1_or_2: depth 100
    task3: mode prove
 
-If the tag ``<taskname>:`` is used on a line by itself then the following block
-until the next blank line is conditional.
+If the tag ``<taskname>:`` is used on a line by itself then the conditional string
+extends until the next conditional block or ``--`` on a line by itself.
 
 .. code-block:: text
 
@@ -55,6 +55,7 @@ until the next blank line is conditional.
 
    task3:
    mode prove
+   --
 
 The tag ``~<taskname>:`` can be used for a line or block that should not be used when
 the given task is active:
@@ -68,6 +69,7 @@ the given task is active:
 
    task3:
    mode prove
+   --
 
 The following example demonstrates how to configure safety and liveness checks for all
 combinations of some host implementations A and B and device implementations X and Y:

diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py
index eb6378350a09a0dea41ac77985e526fe2b08f3e1..73dd7e10c91e1d35bbe54c7a8c66223c1ae0fb0c 100644 (file)
--- a/sbysrc/sby_core.py
+++ b/sbysrc/sby_core.py
@@ -173,6 +173,7 @@ class SbyJob:
                 task_tags_active = set()
                 task_tags_all = set()
                 task_skip_block = False
+                task_skiping_blocks = False
                 for line in f:
                     line = line.rstrip("\n")
                     line = line.rstrip("\r")
@@ -180,28 +181,33 @@ class SbyJob:
                     if tasks_section and line.startswith("["):
                         tasks_section = False
 
-                    tasks_skip = False
-                    if task_skip_block:
-                        if line == "":
+                    if task_skiping_blocks:
+                        if line == "--":
                             task_skip_block = False
-                    else:
-                        for t in task_tags_all:
-                            if line.startswith(t+":"):
-                                line = line[len(t)+1:].lstrip()
-                                if t not in task_tags_active:
-                                    if line == "":
-                                        task_skip_block = True
-                                    tasks_skip = True
-                                break
-                            if line.startswith("~"+t+":"):
-                                line = line[len(t)+2:].lstrip()
-                                if t in task_tags_active:
-                                    if line == "":
-                                        task_skip_block = True
-                                    tasks_skip = True
-                                break
-
-                    if tasks_skip or task_skip_block:
+                            task_skiping_blocks = False
+                            continue
+
+                    task_skip_line = False
+                    for t in task_tags_all:
+                        if line.startswith(t+":"):
+                            line = line[len(t)+1:].lstrip()
+                            match = t in task_tags_active
+                        elif line.startswith("~"+t+":"):
+                            line = line[len(t)+2:].lstrip()
+                            match = t not in task_tags_active
+                        else:
+                            continue
+
+                        if line == "":
+                            task_skiping_blocks = True
+                            task_skip_block = not match
+                            task_skip_line = True
+                        else:
+                            task_skip_line = not match
+
+                        break
+
+                    if task_skip_line or task_skip_block:
                         continue
 
                     if tasks_section: