pythin tests

5 files changed, 738 insertions, 0 deletions

diff --git a/formal/promela/src/src/tests/__init__.py b/formal/promela/src/src/tests/__init__.py
new file mode 100644
index 00000000..e69de29b
--- /dev/null
+++ b/formal/promela/src/src/tests/__init__.py
diff --git a/formal/promela/src/src/tests/library.coco b/formal/promela/src/src/tests/library.coco
new file mode 100644
index 00000000..50f9d1d0
--- /dev/null
+++ b/formal/promela/src/src/tests/library.coco
@@ -0,0 +1,154 @@
+ # SPDX-License-Identifier: BSD-2-Clause 
+ 
+ ##############################################################################
+ # Library Test
+ #
+ # Copyright (C) 2019-2021 Trinity College Dublin (www.tcd.ie)
+ #
+ # All rights reserved.
+ #
+ # Redistribution and use in source and binary forms, with or without
+ # modification, are permitted provided that the following conditions are
+ # met:
+ #
+ #     * Redistributions of source code must retain the above copyright
+ #       notice, this list of conditions and the following disclaimer.
+ #
+ #     * Redistributions in binary form must reproduce the above
+ #       copyright notice, this list of conditions and the following
+ #       disclaimer in the documentation and/or other materials provided
+ #       with the distribution.
+ #
+ #     * Neither the name of the copyright holders nor the names of its
+ #       contributors may be used to endorse or promote products derived
+ #       from this software without specific prior written permission.
+ #
+ # THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+ # "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+ # LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+ # A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+ # OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+ # SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+ # LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+ # DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+ # THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+ # (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+ # OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ ##############################################################################
+
+from src.library import *
+from src import testgen
+
+#
+
+import os
+import random
+
+#
+
+cwd = os.getcwd () + '/'
+cons_cwd = path -> cwd + path
+app_cwd = f -> f cwd
+
+models = '../../../models/'
+models_chains = models + 'chains/src/'
+models_events = models + 'events/src/'
+
+model_checker = '../examples/model_checker/spin.pml'
+
+not_exist_command = 'not_exist_command_' + str (random.random ())
+
+name_b = check_unparse_parse -> '1' if check_unparse_parse else '0'
+name_ml = (fic, check_unparse_parse) -> f'pytest_{name_b (check_unparse_parse)}_ml_{fic}.auto_output'
+name_yaml = (fic, check_unparse_parse) -> f'pytest_{name_b (check_unparse_parse)}_yaml_{fic}.auto_output'
+
+def gen_main (argv, check_unparse_parse, input_output_yaml):
+    testgen.main ( 0
+                 , argv + ([ '--promela', r' /*@ check_unparse_parse'
+                                          r' */' ]
+                           if check_unparse_parse else [])
+                 , input_output_yaml )
+
+def main_ml_promela0 (model_checker, refine, check_unparse_parse, dir0, fic, fic_out):
+    cfg = fileinput_input0 (cons_cwd (dir0 + 'testsuites.cfg'))
+    assert (r'export_dir \<open>_\<close>' in cfg)
+    assert not os.path.exists ('_')
+    gen_main ( list (map (app_cwd, [ model_checker
+                                   , cwd -> cwd + dir0 + fic + '.pml'
+                                   , refine dir0 fic ]))
+               + [ '--promela', cfg ]
+             , check_unparse_parse
+             , False)
+    os.rename ('_', name_ml (fic_out, check_unparse_parse))
+
+main_ml_promela_arg_model_checker = cwd -> cwd + model_checker
+main_ml_promela_arg_refine = (dir0, fic) -> cwd -> cwd + dir0 + fic + '.rfn'
+main_ml_promela = (check_unparse_parse, dir0, fic) -> main_ml_promela0 (main_ml_promela_arg_model_checker, main_ml_promela_arg_refine, check_unparse_parse, dir0, fic, fic)
+
+def symlink (dir0, dir1, fic):
+    os.symlink (dir0 + fic, dir1 + fic)
+    
+def main_yaml_promela (check_unparse_parse, dir0, fic):
+    rfn = fileinput_input0 (cons_cwd (dir0 + fic + '.rfn'))
+    assert r'export_input_yaml \<open>_\<close>' in rfn
+    assert r'export_input_only_content' in rfn
+    dir1 = name_ml (fic, check_unparse_parse) + '/_/'
+    assert all <| map (os.path.exists <.. testgen.export_yml_ext $ dir1, ['', '0', '1', '2', '3'])
+    if r'enclose_file \<open>enclose_1_head.c\<close>' in rfn and r'\<open>enclose_2_foot.c\<close>' in rfn:
+        symlink (cons_cwd dir0, dir1, 'enclose_1_head.c')
+        symlink (cons_cwd dir0, dir1, 'enclose_2_foot.c')
+    else:
+        assert r'enclose_file \<open>enclose_1_head.yml\<close>' in rfn and r'\<open>enclose_2_foot.yml\<close>' in rfn
+        symlink (cons_cwd dir0, dir1, 'enclose_1_head.yml')
+        symlink (cons_cwd dir0, dir1, 'enclose_2_foot.yml')
+    if r'refine_generic_file \<open>../examples/only_generic/chains-rfn.yml\<close>' in rfn:
+        symlink (cons_cwd (dir0 + '../'), dir1 + '../', 'examples')
+    else:
+        assert r'refine_generic_file' not in rfn # not yet implemented: regular expression to match the file name
+    if r'enclose_uniform_file \<open>enclose_init_1_head.c\<close>' in rfn and r'\<open>enclose_init_2_foot.c\<close>' in rfn:
+        symlink (cons_cwd dir0, dir1, 'enclose_init_1_head.c')
+        symlink (cons_cwd dir0, dir1, 'enclose_init_2_foot.c')
+    else:
+        assert r'enclose_uniform_file' not in rfn # not yet implemented: regular expression to match the file name
+    gen_main ( [ '--annotation_file', cons_cwd (testgen.export_yml_ext (dir1, '0'))
+               , cons_cwd (dir0 + fic + '.pml')
+               , '--annotation_file', cons_cwd (testgen.export_yml_ext (dir1, '2'))
+               , '--annotation', fileinput_input0 (cons_cwd (testgen.export_yml_ext (dir1, '3'))) ]
+             , check_unparse_parse
+             , True)
+    os.rename ('_', name_yaml (fic, check_unparse_parse))
+
+def main_promela0 (check_unparse_parse, dir0, fic):
+    main_ml_promela (check_unparse_parse, dir0, fic)
+    main_yaml_promela (check_unparse_parse, dir0, fic)
+
+def main_promela (dir0, fic):
+    main_promela0 (False, dir0, fic)
+    main_promela0 (True, dir0, fic)
+
+def main_promela_events (fic):
+    main_promela (models_events, fic)
+
+def main_ram (arg1, arg2):
+    gen_main ( list (map (cons_cwd, arg1))
+               + arg2
+             , False
+             , False)
+
+def main0 (arg):
+    main_ram ([model_checker], ['-p' + arg])
+
+def main1 (arg):
+    main_ram ([], [arg])
+
+def main2 (arg):
+    main1 ('-p' + arg)
+
+def main3 (arg):
+    main0 (arg + r' ltl { true }')
+
+#
+
+def test_anonymous_not_exec ():
+    # this empty test is only present for coverage reasons (it can then be used as an 'anonymous' function, in situations where the function is not expected to be executed)
+    return
diff --git a/formal/promela/src/src/tests/test_coverage_spin2test.coco b/formal/promela/src/src/tests/test_coverage_spin2test.coco
new file mode 100644
index 00000000..6b63cf45
--- /dev/null
+++ b/formal/promela/src/src/tests/test_coverage_spin2test.coco
@@ -0,0 +1,144 @@
+# SPDX-License-Identifier: BSD-2-Clause
+"""Converts Annotated SPIN counter-examples to program test code"""
+
+# Copyright (C) 2019-2021 Trinity College Dublin (www.tcd.ie)
+#
+# Redistribution and use in source and binary forms, with or without
+# modification, are permitted provided that the following conditions
+# are met:
+# 1. Redistributions of source code must retain the above copyright
+#    notice, this list of conditions and the following disclaimer.
+# 2. Redistributions in binary form must reproduce the above copyright
+#    notice, this list of conditions and the following disclaimer in the
+#    documentation and/or other materials provided with the distribution.
+#
+# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+# AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+# IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
+# ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
+# LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
+# CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
+# SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
+# INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
+# CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
+# ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+# POSSIBILITY OF SUCH DAMAGE.
+
+import src.refine_command as refine
+from src import spin2test
+
+#
+
+from itertools import chain
+import pytest
+
+#
+
+def test_spin2test1 ():
+    spin2test.main (0, '../../../models/events/rqmts-spec-level/', 'model-events-mgr')
+
+def test_spin2test2 ():
+    task_name = 'task_name'
+    decl_name = 'decl_name'
+    dclarray_name = 'dclarray_name'
+    ptr_name = 'ptr_name'
+    call_name0 = 'call_name0'
+    call_name1 = 'call_name1'
+    call_name2 = 'call_name2'
+    call_name3 = 'call_name3'
+    call_name4 = 'call_name4'
+    call_name5 = 'call_name5'
+    call_name6 = 'call_name6'
+    call_name7 = 'call_name7'
+    end_name = 'end_name'
+    scalar_name0 = 'scalar_name0'
+    scalar_name1 = 'scalar_name1'
+    state_name = 'state_name'
+    cmd1 = refine.command ({}, outputLOG = True, annoteComments = False, outputSWITCH = True)
+    cmd1.refineSPINLine_main ([])
+    cmd2 = refine.command (dict (chain ({ 'SUSPEND' : '{}{}{}'
+                                        , 'WAKEUP' : '{}{}{}'
+                                        , ptr_name + '_PTR' : '\n{}'
+                                        , ptr_name + '_FPTR' : '{}\n{}{}'
+                                        , call_name1 : '{}'
+                                        , call_name2 : '{}{}'
+                                        , call_name3 : '{}{}{}'
+                                        , call_name4 : '{}{}{}{}'
+                                        , call_name5 : '{}{}{}{}{}'
+                                        , call_name6 : '{}{}{}{}{}{}'
+                                        , call_name7 : '{}{}{}{}{}{}{}'
+                                        , scalar_name1 + '_FSCALAR' : '{}{}' }.items (),
+                                        {x: '' for x in [ 'NAME'
+                                                        , 'INIT'
+                                                        , task_name
+                                                        , 'SIGNAL'
+                                                        , 'WAIT'
+                                                        , decl_name + '_DCL'
+                                                        , dclarray_name + '_DCL'
+                                                        , call_name0
+                                                        , end_name + '_SEQ'
+                                                        , scalar_name0
+                                                        , state_name ]}.items ())),
+                           outputSWITCH = True)
+    def cmd12 (cmds):
+        for cmd0 in cmds:
+            cmd = ['3'] + cmd0
+            cmd1.refineSPINLine_main cmd
+            cmd2.refineSPINLine_main cmd
+    cmd12 ([ ['LOG', 'Sender', '0', 'finished']
+           , ['NAME', '']
+           , ['INIT']
+           , ['TASK', task_name]
+           , ['SIGNAL', '']
+           , ['WAIT', '']
+           , ['DECL', '', decl_name]
+           , ['DCLARRAY', '', dclarray_name, '']
+           , ['PTR', ptr_name, '0']
+           , ['PTR', ptr_name, '1']
+           , ['PTR', ptr_name, '']
+           , ['END', '']
+           , ['STRUCT', '']
+           , ['PTR', ptr_name, '0']
+           , ['CALL', call_name0]
+           , ['CALL', call_name1, '']
+           , ['CALL', call_name2, '', '']
+           , ['CALL', call_name3, '', '', '']
+           , ['CALL', call_name4, '', '', '', '']
+           , ['CALL', call_name5, '', '', '', '', '']
+           , ['CALL', call_name6, '', '', '', '', '', '']
+           , ['CALL', call_name7, '', '', '', '', '', '', '']
+           , ['SCALAR', scalar_name1, '']
+           , ['SCALAR', scalar_name1, '', '']
+           , ['SEQ', '']
+           , ['END', end_name]
+           , ['SCALAR', '_', '']
+           , ['SCALAR', scalar_name0, '']
+           , ['SCALAR', scalar_name0, '', '']
+           , ['STATE', '', state_name]
+           , ['DON_T_KNOW_HOW_TO_REFINE']
+           , []])
+    
+def test_spin2test3 ():
+    pid, name, task_name, value, typ, index, tid, state = 0, 0, 0, 0, 0, 0, 0, 0
+    rest = []
+    cmd = refine.command ({})
+    with pytest.raises Exception: cmd.refineSPINLine ([pid,'LOG']+rest, test = 'test')
+    with pytest.raises Exception: cmd.refineSPINLine ([pid,'NAME',name], test = 'test')
+    with pytest.raises Exception: cmd.refineSPINLine ([pid,'INIT'], test = 'test')
+    with pytest.raises Exception: cmd.refineSPINLine ([pid,'TASK',task_name], test = 'test')
+    with pytest.raises Exception: cmd.refineSPINLine ([pid,'SIGNAL',value], test = 'test')
+    with pytest.raises Exception: cmd.refineSPINLine ([pid,'WAIT',value], test = 'test')
+    with pytest.raises Exception: cmd.refineSPINLine ([pid,'DEF',name,value], test = 'test')
+    with pytest.raises Exception: cmd.refineSPINLine ([pid,'DECL',typ,name]+rest, test = 'test')
+    with pytest.raises Exception: cmd.refineSPINLine ([pid,'DCLARRAY',typ,name,value], test = 'test')
+    with pytest.raises Exception: cmd.refineSPINLine ([pid,'PTR',name,value], test = 'test')
+    with pytest.raises Exception: cmd.refineSPINLine ([pid,'CALL',name]+rest, test = 'test')
+    with pytest.raises Exception: cmd.refineSPINLine ([pid,'STRUCT',name], test = 'test')
+    with pytest.raises Exception: cmd.refineSPINLine ([pid,'SEQ',name], test = 'test')
+    with pytest.raises Exception: cmd.refineSPINLine ([pid,'END',name], test = 'test')
+    with pytest.raises Exception: cmd.refineSPINLine ([pid,'SCALAR','_',value], test = 'test')
+    with pytest.raises Exception: cmd.refineSPINLine ([pid,'SCALAR',name,value], test = 'test')
+    with pytest.raises Exception: cmd.refineSPINLine ([pid,'SCALAR',name,index,value], test = 'test')
+    with pytest.raises Exception: cmd.refineSPINLine ([pid,'STATE',tid,state], test = 'test')
+    with pytest.raises Exception: cmd.refineSPINLine ([pid], test = 'test')
+    with pytest.raises Exception: cmd.refineSPINLine ([], test = 'test')
diff --git a/formal/promela/src/src/tests/test_coverage_testgen.coco b/formal/promela/src/src/tests/test_coverage_testgen.coco
new file mode 100644
index 00000000..94314c8e
--- /dev/null
+++ b/formal/promela/src/src/tests/test_coverage_testgen.coco
@@ -0,0 +1,394 @@
+ # SPDX-License-Identifier: BSD-2-Clause 
+ 
+ ##############################################################################
+ # Test Coverage TestGen
+ #
+ # Copyright (C) 2019-2021 Trinity College Dublin (www.tcd.ie)
+ #
+ # All rights reserved.
+ #
+ # Redistribution and use in source and binary forms, with or without
+ # modification, are permitted provided that the following conditions are
+ # met:
+ #
+ #     * Redistributions of source code must retain the above copyright
+ #       notice, this list of conditions and the following disclaimer.
+ #
+ #     * Redistributions in binary form must reproduce the above
+ #       copyright notice, this list of conditions and the following
+ #       disclaimer in the documentation and/or other materials provided
+ #       with the distribution.
+ #
+ #     * Neither the name of the copyright holders nor the names of its
+ #       contributors may be used to endorse or promote products derived
+ #       from this software without specific prior written permission.
+ #
+ # THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+ # "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+ # LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+ # A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+ # OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+ # SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+ # LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+ # DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+ # THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+ # (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+ # OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ ##############################################################################
+
+from src.library import *
+from src import syntax_ml
+from src import syntax_pml
+from src.syntax_pml import src_comment, src_annotation, src_directive, arg_pml, arg_annotation
+from src import syntax_yaml
+from src import testgen
+from src.tests.library import *
+
+#
+
+import os
+import pytest
+import tempfile
+
+#
+
+def test_syntax_ml ():
+    with pytest.raises Exception:
+        syntax_ml.not_string ('', 0).parse ('')
+    syntax_ml.enclose_flat ('', '').parse ('')
+    syntax_ml.antiquotation.parse (r'\<ant>')
+    syntax_ml.parse_directive (r'# refine var_c \<^promela>\<open>var_pml\<close> remaining parsed tokens')
+    consume <| syntax_ml.unparse_annotation (None, None, None, None)
+
+def test_syntax_pml ():
+    with pytest.raises Exception:
+        syntax_pml.find_annot0 None
+    with pytest.raises Exception:
+        syntax_pml.find_annot0 ((1, 2), 3, zz = None)
+    consume <| syntax_pml.parse_comment ((arg_pml (), r'/**//*'
+                                                      '\n'
+                                                           r'*/'))
+    consume <| syntax_pml.parse_comment ((arg_pml (), r'/*'
+                                                      '\n'
+                                                       r'*//*'
+                                                      '\n'
+                                                           r'*/'))
+    syntax_pml.directives_refine.parse (r'#r c pml')
+    consume <| syntax_pml.unparse_source_directive (test_anonymous_not_exec, [None])
+
+    #
+    
+    def map_source ( map_annotation = syntax_yaml.unparse_annotation
+                   , parse_commands = syntax_ml.parse_commands
+                   , only_content = False
+                   , subst_lines = []
+                   , lines = (arg_pml (), r'/*@*/')):
+        consume <| syntax_pml.map_source (map_annotation, parse_commands, only_content, subst_lines, lines)
+    map_source (subst_lines = [(2, [(1, ('', []))])])
+    map_source (subst_lines = [(0, [(1, ('', []))])])
+    def map_source2 (only_content):
+        map_source (parse_commands = (_ -> None), only_content = only_content, lines = (arg_annotation (), ''))
+    map_source2 False
+    map_source2 True
+
+    #
+    
+    def parse (_):
+        yield None
+    consume <| syntax_pml.map_source0 (parse, syntax_yaml.unparse_annotation, test_anonymous_not_exec, False, [], (arg_annotation (), r''))
+
+def test_syntax_pml1 ():
+    main0 (r' /*@ no_printf_at */')
+
+def test_syntax_pml2 ():
+    main0 (r' /*@ no_printf_at \<open>zzz\<close> */')
+
+def test_syntax_pml3 ():
+    main0 (r' /*@ refine_uniform_at \<open>prop\<close>'
+           r' */'
+           r' init { true }'
+           r' ltl prop { true }')
+
+def test_syntax_yaml ():
+    syntax_yaml.safe_load (r':')
+    syntax_yaml.parse_directive (r'#refine a []')
+    syntax_yaml.parse_directive (r'#refine a [[1,2],3]')
+    consume <| syntax_pml.map_source (syntax_yaml.unparse_annotation, syntax_ml.parse_commands, False, [(1, [(1, ('', [src_directive, src_annotation ()]))])], (arg_pml (), r'/*@*/'))
+    with pytest.raises Exception:
+        consume <| syntax_yaml.unparse_annotation (src_annotation, None, None, None)
+    consume <| syntax_pml.map_source (syntax_yaml.unparse_annotation, syntax_ml.parse_commands, False, None, (arg_pml (), r'/*@*/'))
+    with pytest.raises Exception:
+        consume <| syntax_yaml.check_annotation (test_anonymous_not_exec, test_anonymous_not_exec, None, False, [], (arg_pml (), r''))
+
+def test_syntax_yaml_check ():
+    def unparse_annotation0 (cmds_generic, cmt_enclose, _, subst_bloc, cmds):
+        yield from syntax_yaml.unparse_annotation (cmt_enclose, cmds_generic, subst_bloc, cmds)
+
+    strip_find_annot1 = (_ -> ((x -> x), {}))
+    src_cmt = cmt_begin -> (src_comment (), ((41, cmt_begin), (41, '\n')))
+    bloc1 = []
+    bloc2 = [(0, [(1, [])])]
+
+    def check_annotation0 ( unparse_annotation = syntax_yaml.unparse_annotation
+                          , parse_commands = syntax_yaml.parse_commands
+                          , strip_find_annot = test_anonymous_not_exec
+                          , group_max = test_anonymous_not_exec
+                          , cmt_enclose = src_cmt ('//')
+                          , cmds_generic = False
+                          , subst_bloc = bloc1
+                          , cmds = [('0.8444218515250481', ['1', '41', '0'])]):
+        syntax_yaml.check_annotation0 (unparse_annotation, parse_commands, strip_find_annot, group_max, cmt_enclose, cmds_generic, subst_bloc, cmds)
+
+    def unparse_annotation1 (*args):
+        yield from unparse_annotation0 <*| (True,) + args
+    check_annotation0 ( unparse_annotation = unparse_annotation1
+                      , cmt_enclose = src_cmt ('@@')
+                      , cmds = ['0', 'CALL', 'append', '21', '6'])
+    
+    def unparse_annotation2 (*args):
+        yield from unparse_annotation0 <*| (False,) + args
+    check_annotation0 (unparse_annotation = unparse_annotation2, cmds_generic = True)
+
+    check_annotation0 (strip_find_annot = strip_find_annot1, group_max = (_ -> bloc2))
+
+    def unparse_annotation3 (cmt_enclose, cmds_generic, _, cmds):
+        yield from syntax_yaml.unparse_annotation (cmt_enclose, cmds_generic, bloc1, cmds)
+    check_annotation0 ( unparse_annotation = unparse_annotation3
+                      , strip_find_annot = strip_find_annot1
+                      , group_max = (_ -> bloc1)
+                      , subst_bloc = bloc2)
+
+#
+
+def test_chains1 ():
+    main_promela0 (True, models_chains, 'testsuites_spfreechain01')
+
+def test_chains2 ():
+    # covering: the path without refine_uniform
+    dir0 = models_chains
+    dir1 = './'
+    cwd = os.getcwd ()
+    with tempfile.TemporaryDirectory () as dir_test:
+        os.chdir dir_test
+        def write_unlink0 (fic):
+            toks = (r'-p'
+                    r' /*@ export_code \<open>init.c\<close>'
+                        r' enclose_file \<open>enclose_1_head.c\<close>'
+                                     r' \<open>enclose_2_foot.c\<close>'
+                        r' refine_generic_file \<open>chains-rfn.yml\<close>'
+                    r' */')
+            fic.write (toks.encode ())
+            fic.close ()
+            symlink (cons_cwd dir0, dir1, 'enclose_1_head.c')
+            symlink (cons_cwd dir0, dir1, 'enclose_2_foot.c')
+            os.symlink (cons_cwd dir0 + '../examples/only_generic/chains-rfn.yml', dir1 + 'chains-rfn.yml')
+            fic0 = dir1 + os.path.basename fic.name
+            os.symlink (fic.name, fic0)
+            main_ml_promela0 ( main_ml_promela_arg_model_checker
+                             , ((_1, _2) -> _0 -> fic0)
+                             , False
+                             , dir0
+                             , 'testsuites_spfreechain01'
+                             , 'testsuites_spfreechain01_no_uniform')
+        testgen.write_unlink (write_unlink0)
+        os.chdir cwd
+
+def test_events ():
+    main_promela_events ('testsuites_validation')
+
+def test_events_exec_all ():
+    main_ml_promela0 ( (_ -> r'-p'
+                             r' /*@ model_checker_verifier \<open>spin\<close> \<open>-a\<close>'
+                                 r' model_checker_compile \<open>gcc\<close> \<open>-DVECTORSZ=4096\<close> \<open>-o\<close> \<open>pan\<close> \<open>pan.c\<close>'
+                                 r' model_checker_exec_one \<open>./pan\<close> \<open>-a\<close> \<open>-n\<close>'
+                                 r' model_checker_exec_all \<open>./pan\<close> \<open>-a\<close> \<open>-n\<close> \<open>-e\<close>'
+                                 r' model_checker_trail \<open>spin\<close> \<open>-p\<close> \<open>-T\<close> \<open>-t\<close> \<open>-k\<close>'
+                                 r' export_trail_num \<open>1\<close>'
+                                 r' export_trail_num \<open>4\<close>'
+                             r' */')
+                     , main_ml_promela_arg_refine
+                     , False
+                     , models_events
+                     , 'testsuites_validation'
+                     , 'testsuites_validation_exec_all')
+
+#
+
+def test_fail_fileinput ():
+    fic = 'not_exist_fic'
+    assert not os.path.exists fic
+    consume <| fileinput_input fic
+    
+    assert os.path.isdir ('.')
+    consume <| fileinput_input ('.')
+
+def test_fail_mkdir ():
+    def write_unlink0 (fic):
+        fic.close ()
+        testgen.mkdir fic.name
+        testgen.mkdir (fic.name + '/_')
+    testgen.write_unlink write_unlink0
+
+def test_fail_copy1 ():
+    def write_unlink0 (fic1):
+        fic1.write('_'.encode())
+        fic1.close ()
+        testgen.copy_i fic1.name fic1.name
+        def write_unlink1 (fic2):
+            fic2.close ()
+            testgen.copy_i fic1.name fic2.name
+        testgen.write_unlink write_unlink1
+        with tempfile.TemporaryDirectory () as dir_test:
+            dir_test1 = dir_test + '/a'
+            fic2 = dir_test1 + '/' + os.path.basename fic1.name
+            testgen.copy_i (fic1.name, fic2)
+            os.symlink (fic1.name, dir_test1)
+            testgen.copy_i (fic1.name, fic2)
+            testgen.copy_i (dir_test, fic2)
+    testgen.write_unlink write_unlink0
+
+def test_fail_split_arg ():
+    consume <| testgen.split_arg ((_ -> None), [''])
+
+def test_fail_write_promela ():
+    st = testgen.read_eval_print (0, [], False)
+    with pytest.raises Exception:
+        st.write_promela (())
+    with pytest.raises Exception:
+        st.write_promela (st.init_top_elems (list (testgen.fold_prog st.argv), st.argv), a = '')
+
+#
+
+def test_fail_parse_syntax_yaml_refine_generic ():
+    main0 (r' /*@ refine_generic \<open>-\<close>'
+           r' */')
+
+def test_fail_parse_syntax_pml ():
+    main0 (r' -')
+
+def test_fail_command_not_found0 ():
+    main2 (r' /*@ model_checker_verifier \<open>' + not_exist_command + r'\<close>'
+           r' */'
+           r' ltl { true }')
+
+def test_fail_command_not_found1 ():
+    testgen.subprocess_exec (True, False, not_exist_command, [])
+
+def test_fail_command_empty ():
+    main2 (r' /*@ model_checker_verifier'
+           r' */'
+           r' ltl { true }')
+
+def test_fail_arg_missing_param ():
+    main2 ('')
+
+def test_fail_arg_unknown ():
+    main1 (r'--' + not_exist_command)
+
+def test_fail_arg_not_exist_fic ():
+    fic = 'not_exist_fic'
+    assert not os.path.exists fic
+    main1 fic
+
+def test_fail_vectorsz ():
+    main_ml_promela0 ( (_ -> r'-p'
+                             r' /*@ model_checker_verifier \<open>spin\<close> \<open>-a\<close>'
+                                 r' model_checker_compile \<open>gcc\<close> \<open>-o\<close> \<open>pan\<close> \<open>pan.c\<close>'
+                                 r' model_checker_exec_one \<open>./pan\<close> \<open>-a\<close> \<open>-n\<close>'
+                                 r' model_checker_trail \<open>spin\<close> \<open>-p\<close> \<open>-T\<close> \<open>-t\<close> \<open>-k\<close>'
+                             r' */')
+                     , main_ml_promela_arg_refine
+                     , False
+                     , models_events
+                     , 'testsuites_validation'
+                     , 'testsuites_validation_vectorsz')
+
+def test_insert_print_non_seq1 ():
+    # covering: print_first (when combined with normal, 'sequence' or 'atomic')
+    #           refine_uniform_strip, particularly when there is at least one newline in the refinement code
+    main3 (r' proctype f () { true }'
+           r' proctype g () { { int a = 0; int b = 0 } }'
+           r' proctype h () { atomic { int a = 0; int b = 0 } }'
+           r' /*@ export_code \<open>init.c\<close>'
+               r' refine_uniform_at \<open>f\<close>'
+                                 r' \<open>'
+                                    '\n' r'//\<close>'
+               r' refine_uniform_at \<open>g\<close> \<open>//\<close>'
+               r' refine_uniform_at \<open>h\<close> \<open>//\<close>'
+               r' print_first'
+               r' refine_uniform_strip'
+           r' */'
+           r' init { run f () }')
+
+def test_insert_print_non_seq2 ():
+    # covering: insertion of printf with print_first deactivated (when combined with normal, 'sequence' or 'atomic')
+    main3 (r' proctype f () { true }'
+           r' proctype g () { { int a = 0; int b = 0 } }'
+           r' proctype h () { atomic { int a = 0; int b = 0 } }'
+           r' /*@ export_code \<open>init.c\<close>'
+               r' refine_uniform_at \<open>g\<close> \<open>//\<close>'
+               r' refine_uniform_at \<open>h\<close> \<open>//\<close>'
+           r' */'
+           r' init { run f () }')
+
+def test_insert_print_non_seq3 ():
+    # covering: insertion of printf with print_first deactivated (when combined with normal, 'sequence' or 'atomic')
+    #           no_printf for all proctypes (as it is written in the same line as all proctypes)
+    main3 (r' proctype f () { true }'
+           r' proctype g () { { int a = 0; int b = 0 } }'
+           r' proctype h () { atomic { int a = 0; int b = 0; true } }'
+           r' /*@ export_code \<open>init.c\<close>'
+               r' no_printf'
+               r' refine_uniform_at \<open>g\<close> \<open>//\<close>'
+               r' refine_uniform_at \<open>h\<close> \<open>//\<close>'
+           r' */'
+           r' init { run f () }')
+
+def test_toplevel_constructs ():
+    # covering: the use of different types of constructs at toplevel
+    main3 (r' int a = 0;'
+           r' proctype f () { true }'
+           r' init { true }')
+
+def test_refine_arg_similar ():
+    # covering: refine_uniform_force
+    #           the use of similar parameters in proctype and inline
+    main3 (r' int a = 0;'
+           r' proctype f (int a; int a) { true }'
+           r' inline g (b, b) { true }'
+           r' /*@ refine_uniform_force'
+           r' */'
+           r' init { true }')
+
+def test_refine_not_serial_ty ():
+    # covering: not serializable type
+    main0 (r' int a = 0;'
+           r' proctype f (int b) { a = b }'
+           '\n'
+           r' /*@ refine_uniform_at \<open>f\<close> \<open>#refine aa\<close>'
+           r' */'
+           '\n'
+           r' init { run f (1) }'
+           r' ltl { <> ([] (a == 1)) }')
+
+def t_refine_redef_direct (arg):
+    main3 (r' proctype f (int a) { true }'
+           r' inline g (b) { true }' # note: removing this inline will decrease the coverage
+           r' /*@ refine_uniform_at \<open>f\<close>'
+                  + arg +
+           r' */'
+           r' init { true }')
+
+def test_refine_redef_direct1 ():
+    # covering: redefinition of directives
+    t_refine_redef_direct (r' \<open>#refine a'
+                              '\n' r'#refine a\<close>')
+
+def test_refine_redef_direct2 ():
+    # covering: definition of directives with a different type
+    t_refine_redef_direct (r' \<open>#refine a @{promela [bool]}\<close>')
+
+def test_refine_redef_direct3 ():
+    # covering: redefinition of directives with an array type
+    t_refine_redef_direct (r' \<open>#refine a'
+                              '\n' r'#refine a @{promela ["int[8]"]}\<close>')
diff --git a/formal/promela/src/src/tests/test_optional.coco b/formal/promela/src/src/tests/test_optional.coco
new file mode 100644
index 00000000..833cc3c3
--- /dev/null
+++ b/formal/promela/src/src/tests/test_optional.coco
@@ -0,0 +1,46 @@
+# SPDX-License-Identifier: BSD-2-Clause
+
+##############################################################################
+ # Test Optional
+ #
+ # Copyright (C) 2019-2021 Trinity College Dublin (www.tcd.ie)
+ #
+ # All rights reserved.
+ #
+ # Redistribution and use in source and binary forms, with or without
+ # modification, are permitted provided that the following conditions are
+ # met:
+ #
+ #     * Redistributions of source code must retain the above copyright
+ #       notice, this list of conditions and the following disclaimer.
+ #
+ #     * Redistributions in binary form must reproduce the above
+ #       copyright notice, this list of conditions and the following
+ #       disclaimer in the documentation and/or other materials provided
+ #       with the distribution.
+ #
+ #     * Neither the name of the copyright holders nor the names of its
+ #       contributors may be used to endorse or promote products derived
+ #       from this software without specific prior written permission.
+ #
+ # THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+ # "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+ # LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+ # A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+ # OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+ # SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+ # LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+ # DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+ # THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+ # (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+ # OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ ##############################################################################
+
+from src.tests.library import *
+
+#
+
+def test_events ():
+    main_promela_events ('testsuites_spintrcritical10_1')
+    main_promela_events ('testsuites_spintrcritical10_2')
+    main_promela_events ('testsuites_spintrcritical10_3')