From 974c2339d99f76a2344381bbd848cf70257c98ad Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Wed, 6 May 2026 09:07:32 +1200 Subject: [PATCH] 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 | 11 +++++++++ docs/examples/tags/complex.log | 29 +++++++++++++++++++++++ docs/examples/tags/complex.sby | 4 ++-- docs/examples/tags/default.log | 27 +++++++++++++++++++++ docs/examples/tags/default.sby | 6 +++++ docs/examples/tags/example.log | 12 ++++++++++ docs/examples/tags/gen.sh | 2 ++ docs/source/advanced/tags.rst | 43 +++++++++++++++++++++++++++++++++- docs/source/reference.rst | 2 +- 9 files changed, 132 insertions(+), 4 deletions(-) create mode 100644 docs/examples/tags/default.log create mode 100644 docs/examples/tags/default.sby diff --git a/docs/examples/tags/bad.log b/docs/examples/tags/bad.log index 26ddb04..57b5776 100644 --- a/docs/examples/tags/bad.log +++ b/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 diff --git a/docs/examples/tags/complex.log b/docs/examples/tags/complex.log index d669f87..d9baad5 100644 --- a/docs/examples/tags/complex.log +++ b/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 diff --git a/docs/examples/tags/complex.sby b/docs/examples/tags/complex.sby index 58295ea..f155b7b 100644 --- a/docs/examples/tags/complex.sby +++ b/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-- diff --git a/docs/examples/tags/default.log b/docs/examples/tags/default.log new file mode 100644 index 0000000..5761655 --- /dev/null +++ b/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 + diff --git a/docs/examples/tags/default.sby b/docs/examples/tags/default.sby new file mode 100644 index 0000000..03c61f7 --- /dev/null +++ b/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 diff --git a/docs/examples/tags/example.log b/docs/examples/tags/example.log index 25e9ad1..d11acbb 100644 --- a/docs/examples/tags/example.log +++ b/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 diff --git a/docs/examples/tags/gen.sh b/docs/examples/tags/gen.sh index 60c6dda..05d8112 100755 --- a/docs/examples/tags/gen.sh +++ b/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 diff --git a/docs/source/advanced/tags.rst b/docs/source/advanced/tags.rst index fcefa04..4681270 100644 --- a/docs/source/advanced/tags.rst +++ b/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 +(``:``) and all lines that are conditionally disabled (``~:``). The +``[tasks]`` section is also only included when called without any tasks. .. literalinclude:: /../examples/tags/complex.log :language: console diff --git a/docs/source/reference.rst b/docs/source/reference.rst index 2f7d58e..4c0b7a4 100644 --- a/docs/source/reference.rst +++ b/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