fixing automatic test generation

[andrewbutterfield]

Currently this relies on putting config data into Promela comments.

This should be moved to YAML files

[andrewbutterfield]

Step 1: Replace .pml files whose only content is a comment with XML-like stuff inside with .yml file Then remove comment_filter

[andrewbutterfield]

As side-effect of this will be to remove any remaining Coconut, so I plan to close #15 now.

[andrewbutterfield]

Need to go through other coconut sources to see what dependencies are. See what is using comment filter stuff

[GH-James]

I've been working based on the model in proto/freecchain-src/

There are 2 refine files which seem to use different methods for refinement, as well as have different resulting c test files

• proto/freecchain-src/refine_validation/testsuites_spfreechain.rfn
• proto/freecchain-src/refine_sptests/testsuites_spfreechain.rfn

The first appears to work more similarly to the methods im familiar with It seems to be based on prints in the trail beginning with @@@ It generates test code as in attached: generated_c_method_1.txt

Im unsure how the second method works/what it intends to do. It generates test code as in attached: generated_c_method_2.txt

If method 1 produces code as is required, that will make creating config files much more similar to the testbuilder process. generated_c_method_2.txt generated_c_method_1.txt

[GH-James]

Following from this, if we want code such as in generated_c_method_1.txt I would be much more confident converting remaining promela config files into yaml.

Assuming I can do the above, I wonder if it would make sense to remove the ability to pass in promela-comment-syntax config files, and only allow yaml files? It may allow for some further code cleanup.

[andrewbutterfield]

They both seem a but of a mix from my perspective, and would need some modificaiton downstream.

Focus on method 1 for now, and only allow yaml files for config (does that affect method 2)

[GH-James]

It would affect method 2 as far as I can tell.

The promela comment/annotation language allows multiple keys with the same value, while yaml does not.

eg

no_annotation_at \<open>show_chain0\<close>
no_annotation_at\<open>show_chain1\<close>

I made an equivalent, which I'm not fond of that basically becomes

dict:
- no_annotation_at: show_chain0
- no_annotation_at: show_chain1

The full original refine_sptests/testsuits_spfreechain.rfn and attempted yaml equivalent refine_sptests/testsuits_spfreechain.yml were added in commit: 322f76f on the AutomaticTestGeneration branch.

The parsed object is quite unusual, and although I believe the yaml generates the equivalent parsed object of the promela annotation, the c files are silently not generated.

Thus far, the limitation of yaml files only appears to affect method 2.