Docs: Add default tasks and alt tag assignment

Demonstrate `--dumpcfg` sans task in the complex code example (and how the empty task impacts tag matching).

docs/examples/tags/bad.log

@@ -13,6 +13,17 @@ $ sby --dumptags bad.sby task1
 task1
 task_1_or_2
 task_1_or_3
+$ sby --dumpdefaults bad.sby
+task1
+task2
+task3
+$ sby --dumpcfg bad.sby
+[tasks]
+task1 task_1_or_2 task_1_or_3
+task2 task_1_or_2
+task3 task_1_or_3
+
+[options]
 $ sby --dumpcfg bad.sby task1
 [options]
 mode bmc

docs/examples/tags/complex.log

@@ -28,6 +28,35 @@ deviceX
 hostA
 unbounded
 unbounded_hAdX
+$ sby --dumpdefaults complex.sby
+unbounded_hAdX
+unbounded_hAdY
+unbounded_hBdX
+unbounded_hBdY
+liveness_hAdX
+liveness_hAdY
+liveness_hBdX
+liveness_hBdY
+$ sby --dumpcfg complex.sby
+[tasks]
+unbounded_hAdX unbounded hostA deviceX
+unbounded_hAdY unbounded hostA deviceY
+unbounded_hBdX unbounded hostB deviceX
+unbounded_hBdY unbounded hostB deviceY
+liveness_hAdX liveness hostA deviceX
+liveness_hAdY liveness hostA deviceY
+liveness_hBdX liveness hostB deviceX
+liveness_hBdY liveness hostB deviceY
+
+[options]
+
+[engines]
+abc pdr
+aiger suprove
+
+[script]
+
+[files]
 $ sby --dumpcfg complex.sby unbounded_hAdX
 [options]
 mode prove

docs/examples/tags/complex.sby

@@ -11,8 +11,8 @@ unbounded: mode prove
 liveness: mode live
 
 [engines]
-unbounded: abc pdr
-liveness: aiger suprove
+~liveness: abc pdr
+~unbounded: aiger suprove
 
 [script]
 --pycode-begin--

docs/examples/tags/default.log

@@ -0,0 +1,27 @@
+./gen.sh -s default
+$ sby --dumptasks default.sby
+task1
+task2
+task3
+$ sby --dumptags default.sby
+task1
+task2
+task3
+task_1_or_2
+task_1_or_3
+$ sby --dumptags default.sby task1
+task1
+task_1_or_2
+task_1_or_3
+$ sby --dumpdefaults default.sby
+task2
+task3
+$ sby --dumpcfg default.sby
+[tasks]
+task1 task_1_or_3 task_1_or_2
+task2 task_1_or_2
+task3 task_1_or_3
+
+task2 task3 : default
+$ sby --dumpcfg default.sby task1
+

docs/examples/tags/default.sby

@@ -0,0 +1,6 @@
+[tasks]
+task1 task_1_or_3 task_1_or_2
+task2 task_1_or_2
+task3 task_1_or_3
+
+task2 task3 : default

docs/examples/tags/example.log

@@ -13,6 +13,18 @@ $ sby --dumptags example.sby task1
 task1
 task_1_or_2
 task_1_or_3
+$ sby --dumpdefaults example.sby
+task1
+task2
+task3
+$ sby --dumpcfg example.sby
+[tasks]
+task1 task_1_or_2 task_1_or_3
+task2 task_1_or_2
+task3 task_1_or_3
+
+[options]
+depth 100
 $ sby --dumpcfg example.sby task1
 [options]
 mode bmc

docs/examples/tags/gen.sh

@@ -33,4 +33,6 @@ set -x
 $sby --dumptasks ${script}.sby
 $sby --dumptags ${script}.sby
 $sby --dumptags ${script}.sby $task
+$sby --dumpdefaults ${script}.sby
+$sby --dumpcfg ${script}.sby
 $sby --dumpcfg ${script}.sby $task

docs/source/advanced/tags.rst

@@ -31,9 +31,47 @@ file conditional.
 .. literalinclude:: /../examples/tags/bad.log
    :language: console
    :start-at: dumpcfg
+   :end-before: dumpcfg
    :caption: ``[engines]`` section is only enabled for ``task3``
 
 
+Alternative tag assignment
+--------------------------
+
+An alternative tag assignment method is provided which uses the colon (``:``)
+character to separate tasks and tags.  With this method it is possible to assign
+a group of tags to multiple tasks at the same time.
+
+.. code-block:: sby
+
+   [tasks]
+   task1
+   task2
+   task3
+
+   task1 task2 : deep bounded
+
+
+Default tasks
+-------------
+
+A special tag, ``default``, is provided for controlling which tasks should be
+run when no specific tasks are provided.  The ``--dumpdefaults`` option is
+provided for getting the list of default tasks for a given ``.sby`` file.  Note
+that ``default`` does *not* get added to the list of tags, and should not be
+used for controlling conditional lines.
+
+.. literalinclude:: /../examples/tags/default.sby
+   :language: sby
+   :caption: ``default.sby`` tasks section
+
+.. literalinclude:: /../examples/tags/default.log
+   :language: console
+   :start-at: dumpdefaults
+   :end-before: dumpcfg
+   :caption: Using ``--dumpdefaults``
+
+
 Complex pycode blocks
 ---------------------
 The following example demonstrates how to configure safety and liveness checks
@@ -56,7 +94,10 @@ so it is important to check ``if task is not None`` to avoid the
 
 When working with complex ``.sby`` files like this, it is very helpful to use
 ``--dumptasks`` and ``--dumpcfg`` to confirm things are being pre-processed as
-expected.
+expected.  Note that when ``--dumpcfg`` is called without any tasks, the
+generated config does not include any lines that are conditionally enabled
+(``<tag>:``) and all lines that are conditionally disabled (``~<tag>:``).  The
+``[tasks]`` section is also only included when called without any tasks.
 
 .. literalinclude:: /../examples/tags/complex.log
    :language: console

docs/source/reference.rst

@@ -56,7 +56,7 @@ only the tags for that task will be listed.
 .. literalinclude:: ../examples/tags/example.log
    :language: console
    :start-at: dumptags
-   :end-before: dumpcfg
+   :end-before: dumpdefaults
    :caption: Using ``--dumptags``
 
 It is possible to check the pre-processed config file for a given task with the