Vous avez reçu un message "Your GitLab account has been locked ..." ? Pas d'inquiétude : lisez cet article https://docs.gricad-pages.univ-grenoble-alpes.fr/help/unlock/

Commit 308a21af authored by Erwan Jahier's avatar Erwan Jahier
Browse files

lurette 0.13 Thu, 22 Nov 2001 13:53:30 +0100 by jahier

Parent-Version:      0.12
Version-Log:

Just a few cosmetic changes.

Project-Description: Lurette
parent 2aa3e529
......@@ -2,35 +2,38 @@
;; REALLY bad things.
(Created-By-Prcs-Version 1 3 3)
(vrai.h 1120 1006183551 31_vrai.h 1.1)
(env.mli 3513 1006182545 15_env.mli 1.3)
(env.mli 3457 1006433610 15_env.mli 1.4)
(test.aut 644 1003928781 22_test.aut 1.1)
(Mercury/graph.m 15076 1002205313 7_graph.m 1.1)
(Mercury/lurette.m 4239 1002789994 5_lurette.m 1.5)
(edge.h 1052 1006263320 33_edge.h 1.1)
(ID_EN_VRAC 2184 1002196285 0_ID_EN_VRAC 1.1)
(env.ml 24541 1006263320 16_env.ml 1.6)
(env.ml 24680 1006433610 16_env.ml 1.7)
(Mercury/test.aut 1231 1002546062 8_test2.aut 1.1)
(doc/Interface_draft 5232 1003928781 19_Interface_ 1.1)
(tram_simple.c 5627 1006433610 37_tram_simpl 1.1)
(Mercury/Mmakefile 102 1002789994 1_Mmakefile 1.3)
(doc/archi.fig 3693 1003928781 20_archi.fig 1.1)
(make_lurette 1121 1006263320 27_make_luret 1.3)
(Makefile 331 1006263320 18_Makefile 1.6)
(Makefile 332 1006433610 18_Makefile 1.7)
(interface/Makefile 123 1006263320 25_Makefile 1.4)
(OcamlMakefile 15015 1004519854 17_OcamlMakef 1.2)
(interface/TAGS 1497 1006182545 26_TAGS 1.2)
(README 0 1002791390 10_README 1.1)
(tram_simple.h 1746 1006433610 36_tram_simpl 1.1)
(Mercury/env.m 9937 1003928781 4_env_automa 1.5)
(random_bool.aut 418 1006182545 29_random_boo 1.1)
(interface/gen_stubs.ml 31527 1006263320 24_generate_l 1.7)
(interface/gen_stubs.ml 31628 1006433610 24_generate_l 1.8)
(Mercury/dot_automata.m 5814 1002546062 9_dot_automa 1.1)
(Mercury/dot.m 3636 1002298322 6_dot.m 1.2)
(Mercury/memory.m 3884 1002196285 3_memory.m 1.1)
(vrai.lus 65 1006182545 28_vrai.lus 1.1)
(graph.mli 1305 1003932490 13_graph.mli 1.2)
(graph.ml 2397 1003932490 14_graph.ml 1.2)
(lurette.mli 45 1006263320 11_lurette.ml 1.4)
(lurette.mli 44 1006433610 11_lurette.ml 1.5)
(TAGS 5673 1006182545 21_TAGS 1.5)
(vrai.c 1405 1006183551 30_vrai.c 1.1)
(lurette.ml 5245 1006263320 12_lurette.ml 1.7)
(util.ml 2865 1006433610 35_util.ml 1.1)
(lurette.ml 5064 1006433610 12_lurette.ml 1.8)
(interface/sut_idl_stub.ml 338 1006263457 34_sut_idl_st 1.1)
(edge.c 1693 1006263320 32_edge.c 1.1)
......@@ -7,7 +7,7 @@ SOURCES = $(SUT) \
$(ORACLE) \
oracle_stub.c oracle_idl_stub.idl \
lurette_stub.ml \
util.ml graph.mli graph.ml env.mli env.ml lurette.mli lurette.ml
util.ml graph.mli graph.ml env.mli env.ml lurette.mli lurette.ml
RESULT = lurette
-include $(OCAMLMAKEFILE)
This diff is collapsed.
......@@ -39,7 +39,7 @@ open Lurette_stub
type var_type = string
type var_name = string
type var_name_and_type = var_name * var_type
type vnt = var_name * var_type
type date
type formula_eps
type formula
......@@ -72,9 +72,9 @@ type env_stateT = {
val read_env_state : string ->
var_name_and_type list (* Environment input variable names and types *)
* var_name_and_type list (* Environment output variable names and types *)
* var_name_and_type list (* Environment local variable names and types *)
vnt list (* Environment input variable names and types *)
* vnt list (* Environment output variable names and types *)
* vnt list (* Environment local variable names and types *)
(*
** [read_env_state file] updates the global variable `env_state'
** using the content of file `file'. Also returns the new lists
......
......@@ -602,9 +602,9 @@ let (generate_lurette_stub_file: vn_ct_mlt_fvn list * vn_ct_mlt_fvn list -> unit
*)
fun mlt fvn ->
match mlt with
"int" -> put " print_int "; put fvn
| "bool" -> put " print_bool "; put fvn
| "float" -> put " print_float "; put fvn
"int" -> put " print_int "; put fvn ; put "; print_string \" \""
| "bool" -> put " print_bool "; put fvn ; put "; print_string \" \""
| "float" -> put " print_float "; put fvn ; put "; print_string \" \""
| _ -> put "print_string \"***\";\n" ;
in
let vnl_in = List.map (fun (w,x,y,z) -> w) sut_in in
......@@ -717,8 +717,8 @@ let (generate_lurette_stub_file: vn_ct_mlt_fvn list * vn_ct_mlt_fvn list -> unit
(*
** I define that type here because I need it here ...
** XXX Could I define it in env.ml and use it here? --> check that.
** I define that type here because I both need it here and in env.ml,
** and this (generated) module is already imported by env.ml ...
*)
put ("type atomic_expr = \n" ^
" | Int of int\n" ^
......@@ -727,7 +727,7 @@ let (generate_lurette_stub_file: vn_ct_mlt_fvn list * vn_ct_mlt_fvn list -> unit
"\n\n") ;
(*
** Defines 2 functionq to access a value from the inputs and outputs
** Defines 2 functions to access a value from the inputs and outputs
** given a variable name. For example, if sut_try have the ml type
** `int -> bool -> float -> bool * int', where the corresponding variable
** names are respectively "a_i", "b", "f", "res_b" and "res_i", then
......
../util.ml
\ No newline at end of file
......@@ -18,15 +18,15 @@ open Util
(*
** [var_decl_are_inconsistent in_env out_env in_sut out_sut]
** checks the consistency of variable declarations made in the environment
** and the SUT. Raises an exception if the decla are inconsistents.
** and the SUT. Raises an exception if the declarations are inconsistents.
*)
let print_var_list vl =
List.iter (fun (v, t) -> print_string ("\n " ^ v ^ " of type " ^ t ^ ",")) vl
let (var_decl_are_inconsistent :
var_name_and_type list -> var_name_and_type list
-> var_name_and_type list -> var_name_and_type list
vnt list -> vnt list
-> vnt list -> vnt list
-> unit) =
fun in_env out_env in_sut out_sut ->
if not(list_are_equals out_env in_sut) then
......@@ -50,9 +50,10 @@ let (var_decl_are_inconsistent :
(*------------------------------------------------------------------------*)
let (read_var_names: string -> var_name_and_type list * var_name_and_type list) =
let (read_var_names: string -> vnt list * vnt list) =
fun file ->
let rec (read_var_list: in_channel -> var_name_and_type list -> var_name_and_type list) =
let rec (read_var_list: in_channel -> vnt list ->
vnt list) =
fun ic acc ->
let str = input_line ic in
if ((str = "\\\\OUTPUT") || (str = "\\\\THE_END"))
......@@ -84,20 +85,21 @@ let rec (main : int -> int -> 'a) =
with Failure(err_msg) -> (print_string err_msg)
and
(read_list_of_aut: int ->
var_name_and_type list * var_name_and_type list * var_name_and_type list ->
var_name_and_type list * var_name_and_type list * var_name_and_type list ) =
vnt list * vnt list * vnt list ->
vnt list * vnt list * vnt list ) =
fun cpt (in0, out0, loc0) ->
if cpt = 0 then (in0, out0, loc0)
else
let aut = Sys.argv.(arg_nb-cpt) in
let (i, o, l) = (Env.read_env_state aut) in
read_list_of_aut (cpt-1)
((append i in0), (append o out0), (append l loc0))
((merge i in0), (merge o out0), (merge l loc0))
and
(main2 : int -> int -> 'a) =
fun test_size thickness ->
let (env_in0, env_out0, env_loc0) =
if (arg_nb = 0) then (failwith "lurette takes as argument a list of .aut files.\n")
if (arg_nb = 0) then
(failwith "lurette takes as argument a list of .aut files.\n")
else read_list_of_aut (arg_nb-1) ([], [], [])
in
let env_in = sort_list_string_pair env_in0 in
......
......@@ -3,6 +3,5 @@
open Env
val main : int -> int -> unit
;; -*- Prcs -*-
(Created-By-Prcs-Version 1 3 3)
(Project-Description "Lurette")
(Project-Version lurette 0 12)
(Parent-Version lurette 0 11)
(Project-Version lurette 0 13)
(Parent-Version lurette 0 12)
(Version-Log "
Add a version of sut_idl_stub.ml in interface for testing purposes.
Just a few cosmetic changes.
")
(New-Version-Log "")
(Checkin-Time "Tue, 20 Nov 2001 14:37:37 +0100")
(Checkin-Time "Thu, 22 Nov 2001 13:53:30 +0100")
(Checkin-Login jahier)
(Populate-Ignore ())
(Project-Keywords)
......@@ -18,20 +18,23 @@ Add a version of sut_idl_stub.ml in interface for testing purposes.
;; Sources files
(lurette.mli (lurette/11_lurette.ml 1.4 644))
(lurette.ml (lurette/12_lurette.ml 1.7 644))
(lurette.mli (lurette/11_lurette.ml 1.5 644))
(lurette.ml (lurette/12_lurette.ml 1.8 644))
(graph.mli (lurette/13_graph.mli 1.2 644))
(graph.ml (lurette/14_graph.ml 1.2 644))
(env.mli (lurette/15_env.mli 1.3 644))
(env.ml (lurette/16_env.ml 1.6 644))
(env.mli (lurette/15_env.mli 1.4 644))
(env.ml (lurette/16_env.ml 1.7 644))
(util.ml (lurette/35_util.ml 1.1 644))
(interface/gen_stubs.ml (lurette/24_generate_l 1.7 644))
(interface/util.ml (../util.ml) :symlink)
(interface/gen_stubs.ml (lurette/24_generate_l 1.8 644))
;; Make files
(OcamlMakefile (lurette/17_OcamlMakef 1.2 644))
(Makefile (lurette/18_Makefile 1.6 644))
(Makefile (lurette/18_Makefile 1.7 644))
(interface/Makefile (lurette/25_Makefile 1.4 644))
(make_lurette (lurette/27_make_luret 1.3 744))
......@@ -79,6 +82,12 @@ Add a version of sut_idl_stub.ml in interface for testing purposes.
(Mercury/graph.m (lurette/7_graph.m 1.1 644))
;; Files added by populate at Tue, 20 Nov 2001 14:43:30 +0100,
;; to version 0.12(w), by jahier:
(tram_simple.h (lurette/36_tram_simpl 1.1 644))
(tram_simple.c (lurette/37_tram_simpl 1.1 644))
)
(Merge-Parents)
(New-Merge-Parents)
/********
* ec2c version 0.4-beta
* c file generated for node : tram_simple
********/
#include <stdlib.h>
#define _tram_simple_EC2C_SRC_FILE
#include "tram_simple.h"
/*--------
Internal structure for the call
--------*/
typedef struct {
void* client_data;
//INPUTS
_boolean _demande_porte;
_boolean _en_station;
_boolean _porte_ouverte;
_boolean _attention_depart;
//OUTPUTS
_boolean _fermer_porte;
_boolean _ouvrir_porte;
_boolean _porte_ok;
_boolean _attention_depart_a_retentit;
_boolean _depart;
_boolean _accepter_demande;
_boolean _porte_demandee;
_boolean _depart_imminent;
//REGISTERS
_boolean M38;
_boolean M38_nil;
_boolean M32;
_boolean M32_nil;
_boolean M22;
_boolean M22_nil;
_boolean M16;
_boolean M16_nil;
_boolean M12;
_boolean M12_nil;
_boolean M7;
} tram_simple_ctx;
/*--------
Output procedures must be defined,
Input procedures must be used:
--------*/
void tram_simple_I_demande_porte(tram_simple_ctx* ctx, _boolean V){
ctx->_demande_porte = V;
}
void tram_simple_I_en_station(tram_simple_ctx* ctx, _boolean V){
ctx->_en_station = V;
}
void tram_simple_I_porte_ouverte(tram_simple_ctx* ctx, _boolean V){
ctx->_porte_ouverte = V;
}
void tram_simple_I_attention_depart(tram_simple_ctx* ctx, _boolean V){
ctx->_attention_depart = V;
}
extern void tram_simple_O_fermer_porte(void*, _boolean);
extern void tram_simple_O_ouvrir_porte(void*, _boolean);
extern void tram_simple_O_porte_ok(void*, _boolean);
extern void tram_simple_O_attention_depart_a_retentit(void*, _boolean);
extern void tram_simple_O_depart(void*, _boolean);
extern void tram_simple_O_accepter_demande(void*, _boolean);
extern void tram_simple_O_porte_demandee(void*, _boolean);
extern void tram_simple_O_depart_imminent(void*, _boolean);
#ifdef CKCHECK
extern void tram_simple_BOT_fermer_porte(void*);
extern void tram_simple_BOT_ouvrir_porte(void*);
extern void tram_simple_BOT_porte_ok(void*);
extern void tram_simple_BOT_attention_depart_a_retentit(void*);
extern void tram_simple_BOT_depart(void*);
extern void tram_simple_BOT_accepter_demande(void*);
extern void tram_simple_BOT_porte_demandee(void*);
extern void tram_simple_BOT_depart_imminent(void*);
#endif
/*--------
Internal reset input procedure
--------*/
static void tram_simple_reset_input(tram_simple_ctx* ctx){
//NOTHING FOR THIS VERSION...
}
/*--------
Reset procedure
--------*/
void tram_simple_reset(tram_simple_ctx* ctx){
ctx->M38_nil = _true;
ctx->M32_nil = _true;
ctx->M22_nil = _true;
ctx->M16_nil = _true;
ctx->M12_nil = _true;
ctx->M7 = _true;
tram_simple_reset_input(ctx);
}
/*--------
Dynamic allocation of an internal structure
--------*/
tram_simple_ctx* tram_simple_new_ctx(void* cdata){
tram_simple_ctx* ctx = (tram_simple_ctx*)calloc(1, sizeof(tram_simple_ctx));
ctx->client_data = cdata;
tram_simple_reset(ctx);
return ctx;
}
/*--------
Copy the value of an internal structure
--------*/
void tram_simple_copy_ctx(tram_simple_ctx* dest, tram_simple_ctx* src){
memcpy((void*)dest, (void*)src, sizeof(tram_simple_ctx));
}
/*--------
Step procedure
--------*/
void tram_simple_step(tram_simple_ctx* ctx){
//LOCAL VARIABLES
_boolean L17;
_boolean L15;
_boolean L14;
_boolean L13;
_boolean L11;
_boolean L10;
_boolean L6;
_boolean L20;
_boolean L21;
_boolean L19;
_boolean L18;
_boolean L5;
_boolean L4;
_boolean L25;
_boolean L24;
_boolean L28;
_boolean L27;
_boolean L31;
_boolean L30;
_boolean L39;
_boolean L37;
_boolean L36;
_boolean L35;
_boolean T38;
_boolean T32;
_boolean T22;
_boolean T16;
_boolean T12;
//CODE
L17 = (! ctx->_en_station);
L15 = (ctx->M16 && L17);
if (ctx->M7) {
L14 = _false;
} else {
L14 = L15;
}
L13 = (! L14);
L11 = (ctx->M12 && L13);
if (ctx->_attention_depart) {
L10 = _true;
} else {
L10 = L11;
}
if (ctx->M7) {
L6 = _false;
} else {
L6 = L10;
}
L20 = (! ctx->_porte_ouverte);
L21 = (ctx->M22 && L20);
if (ctx->_demande_porte) {
L19 = L20;
} else {
L19 = L21;
}
if (ctx->M7) {
L18 = _false;
} else {
L18 = L19;
}
L5 = (L6 && L18);
L4 = (L5 && ctx->_porte_ouverte);
tram_simple_O_fermer_porte(ctx->client_data, L4);
L25 = (ctx->_en_station && L18);
L24 = (L25 && L20);
tram_simple_O_ouvrir_porte(ctx->client_data, L24);
if (ctx->_demande_porte) {
L28 = L20;
} else {
L28 = _true;
}
L27 = (L6 && L28);
tram_simple_O_porte_ok(ctx->client_data, L27);
if (ctx->_attention_depart) {
L31 = _true;
} else {
L31 = ctx->M32;
}
if (ctx->M7) {
L30 = _false;
} else {
L30 = L31;
}
tram_simple_O_attention_depart_a_retentit(ctx->client_data, L30);
tram_simple_O_depart(ctx->client_data, L14);
L39 = (! ctx->_attention_depart);
L37 = (ctx->M38 && L39);
if (L14) {
L36 = _true;
} else {
L36 = L37;
}
if (ctx->M7) {
L35 = _true;
} else {
L35 = L36;
}
tram_simple_O_accepter_demande(ctx->client_data, L35);
tram_simple_O_porte_demandee(ctx->client_data, L18);
tram_simple_O_depart_imminent(ctx->client_data, L6);
T38 = L35;
T32 = L30;
T22 = L18;
T16 = ctx->_en_station;
T12 = L6;
ctx->M38 = T38;
ctx->M38_nil = _false;
ctx->M32 = T32;
ctx->M32_nil = _false;
ctx->M22 = T22;
ctx->M22_nil = _false;
ctx->M16 = T16;
ctx->M16_nil = _false;
ctx->M12 = T12;
ctx->M12_nil = _false;
ctx->M7 = ctx->M7 && !(_true);
}
/********
* ec2c version 0.4-beta
* c header file generated for node : tram_simple
* to be used with : tram_simple.c
********/
/*-------- Predefined types ---------*/
#ifndef _tram_simple_EC2C_PREDEF_TYPES
#define _tram_simple_EC2C_PREDEF_TYPES
typedef int _boolean;
typedef int _integer;
typedef char* _string;
typedef double _real;
typedef double _double;
typedef float _float;
#define _false 0
#define _true 1
#endif
/*--------- Pragmas ----------------*/
//MODULE: tram_simple 4 8
//IN: _boolean demande_porte
//IN: _boolean en_station
//IN: _boolean porte_ouverte
//IN: _boolean attention_depart
//OUT: _boolean fermer_porte
//OUT: _boolean ouvrir_porte
//OUT: _boolean porte_ok
//OUT: _boolean attention_depart_a_retentit
//OUT: _boolean depart
//OUT: _boolean accepter_demande
//OUT: _boolean porte_demandee
//OUT: _boolean depart_imminent
#ifndef _tram_simple_EC2C_SRC_FILE
/*--------Context type -------------*/
struct tram_simple_ctx;
/*--------Context allocation --------*/
extern struct tram_simple_ctx* tram_simple_new_ctx(void* client_data);
/*--------Context copy -------------*/
extern void tram_simple_copy_ctx(struct tram_simple_ctx* dest, struct
tram_simple_ctx* src);
/*-------- Reset procedure -----------*/
extern void tram_simple_reset(struct tram_simple_ctx* ctx);
/*-------- Step procedure -----------*/
extern void tram_simple_step(struct tram_simple_ctx* ctx);
/*-------- Input procedures -------------*/
extern void tram_simple_I_demande_porte(struct tram_simple_ctx*, _boolean);
extern void tram_simple_I_en_station(struct tram_simple_ctx*, _boolean);
extern void tram_simple_I_porte_ouverte(struct tram_simple_ctx*, _boolean);
extern void tram_simple_I_attention_depart(struct tram_simple_ctx*, _boolean);
#endif
let rec (rm: 'a -> 'a list -> 'a list) =
(*
** [rm x l] returns l without x. x should be in l.
*)
fun x l ->
match l with
[] -> assert false
| y::t -> (if x = y then t else y::(rm x t))
let rec (list_is_included: 'a list -> 'a list -> bool) =
(*
** [list_is_included l1 l2] tests if l1 is included into l2.
*)
fun l1 l2 ->
match l1 with
[] -> true
| (x1::t1) -> ( if (List.mem x1 l2) then
list_is_included t1 (rm x1 l2)
else
false )
let (list_are_equals: 'a list -> 'a list -> bool) =
(*
** Tests if 2 lists are equals.
*)
fun l1 l2 ->
(list_is_included l1 l2 && list_is_included l2 l1)
(*
** XXX to put in util.ml
*)
let (readfile: string -> string) =
fun file ->
(*
** [readfile file] outputs the whole contents of the file `file' in a
** string.
*)
let rec (readfile_ic : in_channel -> string -> string) =
fun ic acc ->
let line = try (input_line ic) with End_of_file -> (close_in ic) ; "end_of_file" in
if (line = "end_of_file") then acc else (readfile_ic ic (acc ^ "\n" ^ line))
in
let ic = (open_in file) in
let str = readfile_ic ic "" in
close_in ic;
str
let rec (list_map3: ('a -> 'b -> 'c -> 'd) -> 'a list -> 'b list
-> 'c list -> 'd list) =
fun f l1 l2 l3 ->
match (l1, l2, l3) with
([], [], []) -> []
| (e1::t1, e2::t2, e3::t3) ->
(f e1 e2 e3)::(list_map3 f t1 t2 t3)
| _ -> failwith ("*** Error: list_map3 should be called with lists "
^ "of the same size.")
let rec (list_map4: ('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list
-> 'c list -> 'd list -> 'e list) =
fun f l1 l2 l3 l4 ->
match (l1, l2, l3, l4) with
([], [], [], []) -> []
| (e1::t1, e2::t2, e3::t3, e4::t4) ->
(f e1 e2 e3 e4)::(list_map4 f t1 t2 t3 t4)
| _ -> failwith ("*** Error: list_map3 should be called with lists "
^ "of the same size.")
(*
** Sorts variables lexicographically w.r.t. to their names.
*)
let (sort_list_string_pair: (string * string) list -> (string * string) list) =
fun var_list ->
List.sort (fun (vn1, t1) (vn2, t2) -> compare vn1 vn2) var_list
(*
** merges two lists without introducing duplicates.
*)
let rec (merge: 'a list -> 'a list -> 'a list) =
fun list1 list2 ->
match list1 with
[] -> list2
| x1::t1 ->
if (List.mem x1 list2)
then merge t1 list2
else merge t1 (x1::list2)
(*
** [readfile file] outputs the whole contents of the file `file' in a
** string.
*)
let (readfile: string -> string) =
let rec (readfile_ic : in_channel -> string -> string) =
fun ic acc ->
let line = try (input_line ic) with End_of_file -> (close_in ic) ; "end_of_file" in
if (line = "end_of_file") then acc else (readfile_ic ic (acc ^ line))
in
fun file -> readfile_ic (open_in file) ""