--- formal/promela/src/examples/draft/make.sh | 77 +++++++++++ formal/promela/src/examples/draft/parse.pml | 129 ++++++++++++++++++ .../src/examples/model_checker/spin.pml | 8 ++ formal/promela/src/examples/requirements.txt | 35 +++++ 4 files changed, 249 insertions(+) create mode 100644 formal/promela/src/examples/draft/make.sh create mode 100644 formal/promela/src/examples/draft/parse.pml create mode 100644 formal/promela/src/examples/model_checker/spin.pml create mode 100644 formal/promela/src/examples/requirements.txt
diff --git a/formal/promela/src/examples/draft/make.sh b/formal/promela/src/examples/draft/make.sh new file mode 100644 index 00000000..b4da0981 --- /dev/null +++ b/formal/promela/src/examples/draft/make.sh @@ -0,0 +1,77 @@ +#!/bin/bash + +# SPDX-License-Identifier: BSD-3-Clause +# Copyright (C) 2019-2021 Trinity College Dublin (www.tcd.ie) + +set -e +set -x + +###### + +HOME0="$(dirname "$(python3 -c "import os; print(os.path.realpath('$0'))")")" +cd "$HOME0" + +###### + +pip_check_test='true' +function pip_check () { + if [ "$pip_check_test" ] ; then + set +e + version=$(pip3 show "$1") + st="$?" + set -e + [ "$st" = 0 ] || (echo '`'"pip3 show $1"'`'" failed: "'`'"pip3 install $1"'`' && exit "$st") + + version=$(echo "$version" | grep -m 1 Version | cut -d ' ' -f 2) + set +x + [ "$version" = "$2" ] || (echo "$1 version $version installed instead of $2: "'`'"pip3 install $1==$2"'`' && echo -n "Continue? (ENTER/CTRL+C): " && read) + set -x + fi +} + +# The compilation will require the installation of these libraries: + +pip_check coconut 1.4.3 +pip_check mypy 0.761 + +coconut --target 3 library.coco --mypy --ignore-missing-imports --allow-redefinition +coconut --target 3 syntax_pml.coco --mypy --ignore-missing-imports --allow-redefinition +coconut --target 3 syntax_yaml.coco --mypy --ignore-missing-imports --allow-redefinition +coconut --target 3 syntax_ml.coco --mypy --ignore-missing-imports --allow-redefinition +coconut --target 3 refine_command.coco refine_command.py +coconut --target 3 testgen.coco --mypy --follow-imports silent --ignore-missing-imports --allow-redefinition + +###### + +# as well as all dependencies of ( https://github.com/johnyf/promela ): + +pip_check promela 0.0.2 + +# The above command was mainly executed to install dependencies of the package. + +## git clone g...@gitlab.scss.tcd.ie:tuongf/promela_yacc.git # see also deliverables/FV2-201/wip/ftuong/src_ext + +###### + +# Additionally, we use a library to do various operations on C-style comments ( https://github.com/codeauroraforum/comment-filter ): + +## git clone g...@gitlab.scss.tcd.ie:tuongf/comment-filter.git # see also deliverables/FV2-201/wip/ftuong/src_ext + +# We also modify $PYTHONPATH (so that the library can be used, at least while mypy is executing): + +export PYTHONPATH=`pwd`/comment-filter + +###### + +# At run-time, we will need these libraries: + +pip_check parsec 3.5 +## apt install spin # 6.4.6+dfsg-2 + +###### + +cd - + +# Finally, the main execution proceeds as follows: + +exec python3 "$HOME0/testgen.py" "$@" diff --git a/formal/promela/src/examples/draft/parse.pml b/formal/promela/src/examples/draft/parse.pml new file mode 100644 index 00000000..ec86d1fd --- /dev/null +++ b/formal/promela/src/examples/draft/parse.pml @@ -0,0 +1,129 @@ +/****************************************************************************** + * FV2-201 + * + * 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. + ******************************************************************************/ + +/*@ + +ML \<open> +structure V1 = +struct + +datatype 'a tree = T of 'a tree list + | L of 'a + +val tl' = fn [] => [] | _ :: l => l + +fun get_forest_ass x = + (fn L b => [ L (not b) ] + | T ts => + let val (_, _, ts_res) = + fold + (fn t => fn (ts_pred, ts_succ, ts_res) => + ( t :: ts_pred + , tl' ts_succ + , map let val ts_pred' = rev ts_pred + in fn t_ass => T (ts_pred' @ t_ass :: ts_succ) end + (get_forest_ass t) + :: + ts_res)) + ts + ([], tl' ts, []) + in flat (rev ts_res) end + ) x +end + +structure V2 = +struct + +datatype 'a tree = T of string option * 'a tree list + | L of 'a + +val tl' = fn [] => [] | _ :: l => l + +fun get_forest_ass x = + (fn L b => [ (NONE, L (not b)) ] + | T (t_msg, ts) => + let val (_, _, ts_res) = + fold + (fn t => fn (ts_pred, ts_succ, ts_res) => + ( t :: ts_pred + , tl' ts_succ + , map let val ts_pred' = rev ts_pred + in fn (msg, t_ass) => ( (case msg of NONE => t_msg | _ => msg) + , T (t_msg, ts_pred' @ t_ass :: ts_succ)) + end + (get_forest_ass t) + :: + ts_res)) + ts + ([], tl' ts, []) + in flat (rev ts_res) end + ) x +end +\<close> + +ML \<open> +let + open V1 + val ass = L true + val leaf = T [] + val node = T [ass, T [leaf, T [ass]]] +in + get_forest_ass (T [ T [ T [ T [ ass + , ass] ] + , leaf ] + , node + , node ]) +end +\<close> + +ML \<open> +let + open V2 + val ass = L true + fun t l = T (NONE, l) + fun t' s l = T (SOME s, l) + val leaf = t [] + val node = t' "b1" [ass, t' "b2" [leaf, t' "b3" [ass]]] +in + get_forest_ass (t' "c1" [ t' "c2" [ t' "c3" [ t' "c4" [ ass + , ass] ] + , leaf ] + , node + , node ]) +end +\<close> + +*/ \ No newline at end of file diff --git a/formal/promela/src/examples/model_checker/spin.pml b/formal/promela/src/examples/model_checker/spin.pml new file mode 100644 index 00000000..a1caa8ed --- /dev/null +++ b/formal/promela/src/examples/model_checker/spin.pml @@ -0,0 +1,8 @@ +// apt install spin // 6.4.6+dfsg-2 +/*@ + model_checker_verifier \<open>spin\<close> \<open>-a\<close> + model_checker_compile \<open>gcc\<close> \<open>-DVECTORSZ=4096\<close> \<open>-o\<close> \<open>pan\<close> \<open>pan.c\<close> + model_checker_exec_one \<open>./pan\<close> \<open>-a\<close> \<open>-n\<close> + model_checker_exec_all \<open>./pan\<close> \<open>-a\<close> \<open>-n\<close> \<open>-e\<close> + model_checker_trail \<open>spin\<close> \<open>-p\<close> \<open>-T\<close> \<open>-t\<close> \<open>-k\<close> +*/ diff --git a/formal/promela/src/examples/requirements.txt b/formal/promela/src/examples/requirements.txt new file mode 100644 index 00000000..f6f48fd4 --- /dev/null +++ b/formal/promela/src/examples/requirements.txt @@ -0,0 +1,35 @@ +astroid==2.4.2 +attrs==20.3.0 +coconut==1.4.3 +coverage==5.3 +cPyparsing==2.4.5.0.1.1 +decorator==4.4.2 +flake8==3.8.4 +importlib-metadata==3.1.1 +iniconfig==1.1.1 +isort==5.6.4 +lazy-object-proxy==1.4.3 +mccabe==0.6.1 +mypy==0.782 +mypy-extensions==0.4.3 +networkx==2.5 +packaging==20.7 +parsec==3.5 +pluggy==0.13.1 +ply==3.10 +prompt-toolkit==3.0.8 +py==1.9.0 +pycodestyle==2.6.0 +pyflakes==2.2.0 +Pygments==2.7.2 +pylint==2.6.0 +pytest==6.1.2 +PyYAML==5.3.1 +six==1.15.0 +toml==0.10.2 +typed-ast==1.4.1 +typing-extensions==3.7.4.3 +wcwidth==0.2.5 +wrapt==1.12.1 +yapf==0.30.0 +zipp==3.4.0 -- 2.37.1 (Apple Git-137.1) _______________________________________________ devel mailing list devel@rtems.org http://lists.rtems.org/mailman/listinfo/devel