diff --git a/docs/examples/tags/bad.log b/docs/examples/tags/bad.log new file mode 100644 index 0000000..26ddb04 --- /dev/null +++ b/docs/examples/tags/bad.log @@ -0,0 +1,20 @@ +./gen.sh -s bad +$ sby --dumptasks bad.sby +task1 +task2 +task3 +$ sby --dumptags bad.sby +task1 +task2 +task3 +task_1_or_2 +task_1_or_3 +$ sby --dumptags bad.sby task1 +task1 +task_1_or_2 +task_1_or_3 +$ sby --dumpcfg bad.sby task1 +[options] +mode bmc +depth 100 + diff --git a/docs/examples/tags/bad.sby b/docs/examples/tags/bad.sby new file mode 100644 index 0000000..aa795c8 --- /dev/null +++ b/docs/examples/tags/bad.sby @@ -0,0 +1,15 @@ +[tasks] +task1 task_1_or_2 task_1_or_3 +task2 task_1_or_2 +task3 task_1_or_3 + +[options] +task_1_or_2: +mode bmc +depth 100 + +task3: +mode prove + +[engines] +... diff --git a/docs/source/advanced/tags.rst b/docs/source/advanced/tags.rst index 2665827..fcefa04 100644 --- a/docs/source/advanced/tags.rst +++ b/docs/source/advanced/tags.rst @@ -1,6 +1,39 @@ Tasks and tags ============== +Multi-line tag sections +----------------------- +If ``:`` is used on a line by itself then the conditional string +extends until ``--`` is found on a line by itself. + +.. code-block:: sby + + [options] + task_1_or_2: + mode bmc + depth 100 + -- + + task3: + mode prove + -- + +If the closing ``--`` line is ommitted, the current conditional block will +extend until the next conditional block. However it is recommended to always +include the closing ``--`` line to avoid inadvertently making the rest of the +file conditional. + +.. literalinclude:: /../examples/tags/bad.sby + :language: sby + :start-at: [options] + :caption: ``bad.sby`` + +.. literalinclude:: /../examples/tags/bad.log + :language: console + :start-at: dumpcfg + :caption: ``[engines]`` section is only enabled for ``task3`` + + Complex pycode blocks --------------------- The following example demonstrates how to configure safety and liveness checks