Skip to content

GitLab

Commit 714ddf46 authored by Erwan Jahier's avatar Erwan Jahier
Browse files

lurette 0.11 Tue, 20 Nov 2001 14:35:20 +0100 by jahier 

Parent-Version:      0.10
Version-Log:

Fixing bugs. Now it can runs sut that have several inputs and outputs.

Project-Description: Lurette
parent 8e4320dd
Expand all Hide whitespace changes
Inline Side-by-side
.lurette.prcs_aux
View file @ 714ddf46
......@@ -6,28 +6,30 @@
(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 24522 1006182545 16_env.ml 1.5)
(env.ml 24541 1006263320 16_env.ml 1.6)
(Mercury/test.aut 1231 1002546062 8_test2.aut 1.1)
(doc/Interface_draft 5232 1003928781 19_Interface_ 1.1)
(Mercury/Mmakefile 102 1002789994 1_Mmakefile 1.3)
(doc/archi.fig 3693 1003928781 20_archi.fig 1.1)
(make_lurette 1059 1006182545 27_make_luret 1.2)
(Makefile 323 1006182545 18_Makefile 1.5)
(interface/Makefile 115 1006182545 25_Makefile 1.3)
(make_lurette 1121 1006263320 27_make_luret 1.3)
(Makefile 331 1006263320 18_Makefile 1.6)
(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)
(Mercury/env.m 9937 1003928781 4_env_automa 1.5)
(random_bool.aut 418 1006182545 29_random_boo 1.1)
(interface/gen_stubs.ml 31878 1006182545 24_generate_l 1.6)
(interface/gen_stubs.ml 31527 1006263320 24_generate_l 1.7)
(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 38 1006183551 11_lurette.ml 1.3)
(lurette.mli 45 1006263320 11_lurette.ml 1.4)
(TAGS 5673 1006182545 21_TAGS 1.5)
(vrai.c 1405 1006183551 30_vrai.c 1.1)
(lurette.ml 5899 1006183551 12_lurette.ml 1.6)
(lurette.ml 5245 1006263320 12_lurette.ml 1.7)
(edge.c 1693 1006263320 32_edge.c 1.1)
Makefile
View file @ 714ddf46
......@@ -7,7 +7,7 @@ SOURCES = $(SUT) \
$(ORACLE) \
oracle_stub.c oracle_idl_stub.idl \
lurette_stub.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)
edge.c deleted 120000 → 0
View file @ 8e4320dd
../Lustre/edge.c
\ No newline at end of file
edge.c 0 → 100644
View file @ 714ddf46
/********
* ec2c version 0.4-beta
* c file generated for node : edge
********/
#include <stdlib.h>
#define _edge_EC2C_SRC_FILE
#include "edge.h"
/*--------
Internal structure for the call
--------*/
typedef struct {
void* client_data;
//INPUTS
_boolean _X;
//OUTPUTS
_boolean _Y;
//REGISTERS
_boolean M7;
_boolean M7_nil;
_boolean M2;
} edge_ctx;
/*--------
Output procedures must be defined,
Input procedures must be used:
--------*/
void edge_I_X(edge_ctx* ctx, _boolean V){
ctx->_X = V;
}
extern void edge_O_Y(void*, _boolean);
#ifdef CKCHECK
extern void edge_BOT_Y(void*);
#endif
/*--------
Internal reset input procedure
--------*/
static void edge_reset_input(edge_ctx* ctx){
//NOTHING FOR THIS VERSION...
}
/*--------
Reset procedure
--------*/
void edge_reset(edge_ctx* ctx){
ctx->M7_nil = _true;
ctx->M2 = _true;
edge_reset_input(ctx);
}
/*--------
Dynamic allocation of an internal structure
--------*/
edge_ctx* edge_new_ctx(void* cdata){
edge_ctx* ctx = (edge_ctx*)calloc(1, sizeof(edge_ctx));
ctx->client_data = cdata;
edge_reset(ctx);
return ctx;
}
/*--------
Copy the value of an internal structure
--------*/
void edge_copy_ctx(edge_ctx* dest, edge_ctx* src){
memcpy((void*)dest, (void*)src, sizeof(edge_ctx));
}
/*--------
Step procedure
--------*/
void edge_step(edge_ctx* ctx){
//LOCAL VARIABLES
_boolean L6;
_boolean L5;
_boolean L1;
_boolean T7;
//CODE
L6 = (! ctx->M7);
L5 = (ctx->_X && L6);
if (ctx->M2) {
L1 = _false;
} else {
L1 = L5;
}
edge_O_Y(ctx->client_data, L1);
T7 = ctx->_X;
ctx->M7 = T7;
ctx->M7_nil = _false;
ctx->M2 = ctx->M2 && !(_true);
}
edge.h deleted 120000 → 0
View file @ 8e4320dd
interface/edge.h
\ No newline at end of file
edge.h 0 → 100644
View file @ 714ddf46
/********
* ec2c version 0.4-beta
* c header file generated for node : edge
* to be used with : edge.c
********/
/*-------- Predefined types ---------*/
#ifndef _edge_EC2C_PREDEF_TYPES
#define _edge_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: edge 1 1
//IN: _boolean X
//OUT: _boolean Y
#ifndef _edge_EC2C_SRC_FILE
/*--------Context type -------------*/
struct edge_ctx;
/*--------Context allocation --------*/
extern struct edge_ctx* edge_new_ctx(void* client_data);
/*--------Context copy -------------*/
extern void edge_copy_ctx(struct edge_ctx* dest, struct edge_ctx* src);
/*-------- Reset procedure -----------*/
extern void edge_reset(struct edge_ctx* ctx);
/*-------- Step procedure -----------*/
extern void edge_step(struct edge_ctx* ctx);
/*-------- Input procedures -------------*/
extern void edge_I_X(struct edge_ctx*, _boolean);
#endif
env.ml
View file @ 714ddf46
......@@ -544,7 +544,7 @@ let (env_try : int -> sut_out -> (node list * sut_in * env_loc) list) =
match f with
Bid(var_name) -> ([(var_name, Bool(true))], [])
| Not(Bid(var_name)) -> ([(var_name, Bool(false))], [])
| _ -> failwith "That kind of formula is not supported (yet!), sorry...\n"
| _ -> failwith "*** solve_formula: That kind of formula is not supported (yet!), sorry...\n"
(*
** XXX
** XXX FIXME !!!
......
interface/Makefile
View file @ 714ddf46
OCAMLMAKEFILE = ../OcamlMakefile
SOURCES = gen_stubs.ml
SOURCES = util.ml gen_stubs.ml
RESULT = gen_stubs
LIBS = str
......
interface/gen_stubs.ml
View file @ 714ddf46
This diff is collapsed.
lurette.ml
View file @ 714ddf46
......@@ -12,34 +12,7 @@
open Env
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
[] -> failwith "Element not in the list; can not remove it"
| 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)
open Util
(*
......@@ -49,7 +22,7 @@ let (list_are_equals: 'a list -> 'a list -> bool) =
*)
let print_var_list vl =
List.iter (fun (v, t) -> print_string (v ^ " of type " ^ t ^ " ")) 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
......@@ -104,10 +77,10 @@ open List
let arg_nb = (Array.length Sys.argv)
let rec (main : int -> 'a) =
(* XXX the test size should be a parameter of main too *)
fun thickness ->
try main2 thickness
let rec (main : int -> int -> 'a) =
fun test_size thickness ->
try main2 test_size thickness
with Failure(err_msg) -> (print_string err_msg)
and
(read_list_of_aut: int ->
......@@ -121,12 +94,15 @@ and
read_list_of_aut (cpt-1)
((append i in0), (append o out0), (append l loc0))
and
(main2 : int -> 'a) =
fun thickness ->
let (env_in, env_out, env_loc) =
(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")
else read_list_of_aut (arg_nb-1) ([], [], [])
in
let env_in = sort_list_string_pair env_in0 in
let env_out = sort_list_string_pair env_out0 in
let env_loc = sort_list_string_pair env_loc0 in
let print_var_list vl =
List.iter (fun (t, v) -> print_string (v ^ ":" ^ t ^ ", ")) vl
in
......@@ -173,8 +149,7 @@ and
*)
let (results: bool list) = List.map2 (fun x y -> oracle_try (x, y)) inputs outputs in
let _ = if (List.mem false results) then
(* XXX give a better error message *)
failwith "*** According to the oracle, an invalid input-output pair has been generated"
assert false
else
()
in
......@@ -205,11 +180,8 @@ and
print_string "\nOne more loop ? [type any char to stop, `CR' to continue]\n";
let str = read_line () in
if (str = "") then main_loop thickness new_output else ();
;;
main 2;;
main 100 2;;
lurette.mli
View file @ 714ddf46
......@@ -4,5 +4,5 @@ open Env
val main : int -> unit
val main : int -> int -> unit
lurette.prj
View file @ 714ddf46
;; -*- Prcs -*-
(Created-By-Prcs-Version 1 3 3)
(Project-Description "Lurette")
(Project-Version lurette 0 10)
(Parent-Version lurette perso 6)
(Project-Version lurette 0 11)
(Parent-Version lurette 0 10)
(Version-Log "
lurette.ml:
Removing dead code.
Fixing bugs. Now it can runs sut that have several inputs and outputs.
")
(New-Version-Log "")
(Checkin-Time "Mon, 19 Nov 2001 16:25:51 +0100")
(Checkin-Time "Tue, 20 Nov 2001 14:35:20 +0100")
(Checkin-Login jahier)
(Populate-Ignore ())
(Project-Keywords)
......@@ -19,22 +18,22 @@ lurette.ml:
;; Sources files
(lurette.mli (lurette/11_lurette.ml 1.3 644))
(lurette.ml (lurette/12_lurette.ml 1.6 644))
(lurette.mli (lurette/11_lurette.ml 1.4 644))
(lurette.ml (lurette/12_lurette.ml 1.7 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.5 644))
(env.ml (lurette/16_env.ml 1.6 644))
(interface/gen_stubs.ml (lurette/24_generate_l 1.6 644))
(interface/gen_stubs.ml (lurette/24_generate_l 1.7 644))
;; Make files
(OcamlMakefile (lurette/17_OcamlMakef 1.2 644))
(Makefile (lurette/18_Makefile 1.5 644))
(interface/Makefile (lurette/25_Makefile 1.3 644))
(make_lurette (lurette/27_make_luret 1.2 744))
(Makefile (lurette/18_Makefile 1.6 644))
(interface/Makefile (lurette/25_Makefile 1.4 644))
(make_lurette (lurette/27_make_luret 1.3 744))
;; Documentation
......@@ -54,8 +53,8 @@ lurette.ml:
(random_bool.aut (lurette/29_random_boo 1.1 644))
(vrai.c (lurette/30_vrai.c 1.1 644))
(vrai.h (lurette/31_vrai.h 1.1 644))
(edge.c (../Lustre/edge.c) :symlink)
(edge.h (interface/edge.h) :symlink)
(edge.c (lurette/32_edge.c 1.1 640))
(edge.h (lurette/33_edge.h 1.1 640))
......@@ -78,6 +77,7 @@ lurette.ml:
; I have added graph__arc_content in the interface of this library module
(Mercury/graph.m (lurette/7_graph.m 1.1 644))
)
(Merge-Parents)
(New-Merge-Parents)
make_lurette
View file @ 714ddf46
#! /bin/sh
#
# XXX should be an ocaml script for portability ...
Help="usage: make_lurette <sut> <oracle>
Help="usage: make_lurette <sut> <oracle> <env_1> ... <env_n>
The first and second args of this scripts should respectively be the
name of the sut and the name of the oracle modules (without any
extension).
extension).
The remaining args are the list of environment automata.
XXX pass it here or in lurette ???
1) It call gen_stubs script to generate the stub files to interface
the C (poc) files implementing the sut and the oracle with the rest of
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment