source: rtems-central/formal/promela/src/src/spin2test.coco @ 1283c16

Last change on this file since 1283c16 was 1283c16, checked in by Andrew Butterfield <Andrew.Butterfield@…>, on 01/10/23 at 19:57:22

main Coconut sources

  • Property mode set to 100644
File size: 3.7 KB
Line 
1# SPDX-License-Identifier: BSD-2-Clause
2"""Converts Annotated SPIN counter-examples to program test code"""
3
4# Copyright (C) 2019-2021 Trinity College Dublin (www.tcd.ie)
5#
6# Redistribution and use in source and binary forms, with or without
7# modification, are permitted provided that the following conditions
8# are met:
9# 1. Redistributions of source code must retain the above copyright
10#    notice, this list of conditions and the following disclaimer.
11# 2. Redistributions in binary form must reproduce the above copyright
12#    notice, this list of conditions and the following disclaimer in the
13#    documentation and/or other materials provided with the distribution.
14#
15# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
16# AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
17# IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
18# ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
19# LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
20# CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
21# SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
22# INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
23# CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
24# ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
25# POSSIBILITY OF SUCH DAMAGE.
26
27import src.refine_command as refine
28
29#
30
31import logging
32import sys
33import yaml
34
35#
36
37refine.logger.setLevel (logging.DEBUG)
38refine.logger.addHandler (logging.StreamHandler (sys.stderr))
39
40def words(string): return string.rsplit(' ')
41
42def main (testNumber, dir0, fileRoot):
43    "\n\tSpin2Test (Coconut/Python)\n\n" |> refine.logger.debug
44    refine.logger.debug("Test Number {}\n".format(testNumber))
45
46    if int(testNumber) < 0:
47        num = ""
48    else:
49        num = "-{}".format(testNumber)
50
51    spinFile = dir0 +         fileRoot + num + ".spn"
52    refFile  = dir0 +         fileRoot +   "-rfn.yml"
53    preFile  = dir0 +         fileRoot +   "-pre.h"
54    postFile = dir0 +         fileRoot +  "-post.h"
55    runFile  = dir0 +         fileRoot +   "-run.h"
56    testFile = dir0 + "tr-" + fileRoot + num + ".c"
57
58    summaryFormat = "!{} --({}`)-> [{};_;{};{}] >> {}\n"
59    refine.logger.debug(summaryFormat.format( spinFile,refFile
60                                            , preFile,postFile
61                                            , runFile,testFile ))
62
63    print summaryFormat
64
65    annote_lines = []
66    with open(spinFile) as spinfile:
67        debug_lines = ''
68        for line in spinfile:
69            if line[0:4] == "@@@ ":
70                debug_lines = debug_lines + line
71                annote_lines = annote_lines + [line[4:][:-1]]
72        refine.logger.debug (debug_lines)
73
74    annote_bundle = fmap (words,annote_lines)
75
76    refine.logger.debug("Annotation Bundle:\n {}".format(annote_bundle))
77
78    with open(refFile) as reffile:
79       ref_dict = yaml.safe_load(reffile.read())
80       refine.logger.debug("\nREFINE DUMP")
81       refine.logger.debug(yaml.dump(ref_dict))
82
83    cmd = refine.command(ref_dict)
84
85    cmd.setupLanguage()
86    for ln in annote_bundle:
87        cmd.refineSPINLine_main(ln)
88
89    refine.logger.debug("\nP-Ids in use: {}\n ".format(cmd.procIds))
90    refine.logger.debug("\n\tRefinement Complete; No of processes = {}".format(len(cmd.procIds)))
91
92    with open(testFile,'w') as tstfile:
93
94        with open(preFile) as prefile:
95            tstfile.write(prefile.read())
96
97        for line in cmd.test_body():
98            tstfile.write(line)
99
100        with open(postFile) as postfile:
101            tstfile.write(postfile.read())
102
103        with open(runFile) as runfile:
104            tstfile.write(runfile.read().format(testNumber))
Note: See TracBrowser for help on using the repository browser.