From fec915763a2a27d4e2b5deb3b84875cd6080e967 Mon Sep 17 00:00:00 2001
From: Erwan Jahier <erwan.jahier@univ-grenoble-alpes.fr>
Date: Tue, 30 Aug 2022 16:10:16 +0200
Subject: [PATCH] refactoring
---
lib/sas.lus | 2 +-
.../bfs_spanning_tree_oracle.lus | 2 +-
test/bfs-spanning-tree/p.lus | 9 ---------
test/bfs-spanning-tree/state.lus | 16 +++++++++++++---
test/kclustering/verify.lus | 2 +-
5 files changed, 16 insertions(+), 15 deletions(-)
diff --git a/lib/sas.lus b/lib/sas.lus
index ffa29ac8..e8ea5cc1 100644
--- a/lib/sas.lus
+++ b/lib/sas.lus
@@ -17,7 +17,7 @@ let
tel;
-- Any activation Ai implies Ei was previously enabled.
-node activation_is_valid<<const an:int>>(acti, enab : bool^an) returns (y : bool);
+function activation_is_valid<<const an:int>>(acti, enab : bool^an) returns (y : bool);
let
y = boolall<<an>>(map<<=>,an>>(acti, enab));
tel;
diff --git a/test/bfs-spanning-tree/bfs_spanning_tree_oracle.lus b/test/bfs-spanning-tree/bfs_spanning_tree_oracle.lus
index 5e57786a..1e0cae5f 100644
--- a/test/bfs-spanning-tree/bfs_spanning_tree_oracle.lus
+++ b/test/bfs-spanning-tree/bfs_spanning_tree_oracle.lus
@@ -1,5 +1,5 @@
--- Here, we use the Lustre version of the algorithm as an oracle for the ocaml version
+-- Here, we use the Lustre version of the algorithm as a test oracle for the ocaml version
include "../../lib/utils.lus"
diff --git a/test/bfs-spanning-tree/p.lus b/test/bfs-spanning-tree/p.lus
index 932ae34a..e7100537 100644
--- a/test/bfs-spanning-tree/p.lus
+++ b/test/bfs-spanning-tree/p.lus
@@ -1,12 +1,3 @@
------------------------------------------------------------
---Usefull function for type struct:
-function d (neigh: state)
-returns(res: int)
-let
- res=neigh.d;
-tel;
-
------------------------------------------------------------
--Return the tab minimal value:
function min_tab<<const n:int>> (this : int; neighbors : int^n)
returns (new: int);
diff --git a/test/bfs-spanning-tree/state.lus b/test/bfs-spanning-tree/state.lus
index 9b552c0c..5df8fa20 100644
--- a/test/bfs-spanning-tree/state.lus
+++ b/test/bfs-spanning-tree/state.lus
@@ -1,6 +1,4 @@
--- automatically generated by salut
-
type state = struct { d:int ; par:int };
type action = enum { CD , CP };
@@ -10,8 +8,20 @@ function action_of_int(i : int) returns (a : action);
let
a = if i = 0 then CD else CP;
tel;
-function legitimate<<const actions_number:int; const card:int>>(enables : bool^actions_number^card; config: state^card)
+function legitimate<<const actions_number:int; const card:int>>(
+ enables : bool^actions_number^card; config: state^card)
returns (res : bool);
let
res=silent<<actions_number,card>>(enables);
tel;
+
+-----------------------------------------------------------
+--Usefull function for type struct:
+-----------------------------------------------------------
+
+function d (neigh: state)
+returns(res: int)
+let
+ res=neigh.d;
+tel;
+
diff --git a/test/kclustering/verify.lus b/test/kclustering/verify.lus
index 08aa21ed..6fe2c212 100644
--- a/test/kclustering/verify.lus
+++ b/test/kclustering/verify.lus
@@ -41,7 +41,7 @@ tel;
----------------------------------------------------------------------------
-- all states are initially in correctly
----------------------------------------------------------------------------
-node rangei<<const low:int; const card:int; const max:int>>(config:state^card) returns (res:bool);
+function rangei<<const low:int; const card:int; const max:int>>(config:state^card) returns (res:bool);
var
e:state;
let
--
GitLab