adds old examples

4 files changed, 249 insertions, 0 deletions

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 git@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 git@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