Commit 8e4320dd authored by Erwan Jahier's avatar Erwan Jahier
Browse files

lurette 0.10 Mon, 19 Nov 2001 16:25:51 +0100 by jahier

Parent-Version:      perso.6
Version-Log:

lurette.ml:
        Removing dead code.

Project-Description: Lurette
parent 30511592
;; This file is automatically generated, editing may cause PRCS to do
;; 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)
(test.aut 644 1003928781 22_test.aut 1.1)
(Mercury/graph.m 15076 1002205313 7_graph.m 1.1)
......@@ -9,23 +10,24 @@
(env.ml 24522 1006182545 16_env.ml 1.5)
(Mercury/test.aut 1231 1002546062 8_test2.aut 1.1)
(doc/Interface_draft 5232 1003928781 19_Interface_ 1.1)
(make_lurette 1059 1006182545 27_make_luret 1.2)
(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)
(OcamlMakefile 15015 1004519854 17_OcamlMakef 1.2)
(interface/TAGS 1497 1006182545 26_TAGS 1.2)
(README 0 1002791390 10_README 1.1)
(random_bool.aut 418 1006182545 29_random_boo 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)
(Mercury/dot_automata.m 5814 1002546062 9_dot_automa 1.1)
(vrai.lus 65 1006182545 28_vrai.lus 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 439 1006182545 11_lurette.ml 1.2)
(lurette.mli 38 1006183551 11_lurette.ml 1.3)
(TAGS 5673 1006182545 21_TAGS 1.5)
(lurette.ml 6688 1006182545 12_lurette.ml 1.5)
(vrai.c 1405 1006183551 30_vrai.c 1.1)
(lurette.ml 5899 1006183551 12_lurette.ml 1.6)
../Lustre/edge.c
\ No newline at end of file
interface/edge.h
\ No newline at end of file
......@@ -43,9 +43,9 @@ let (list_are_equals: 'a list -> 'a list -> bool) =
(*
** [var_decl_are_inconsistent in_env out_env in_sut out_sut in_or out_or]
** checks the consistency of variable declarations made in the environment,
** the SUT and the oracle. Raises an exception if the decla are inconsistents.
** [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.
*)
let print_var_list vl =
......@@ -54,9 +54,8 @@ let print_var_list 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
-> var_name_and_type list -> var_name_and_type list
-> unit) =
fun in_env out_env in_sut out_sut in_or out_or ->
fun in_env out_env in_sut out_sut ->
if not(list_are_equals out_env in_sut) then
(
print_string "\nenv outputs: ";
......@@ -73,22 +72,6 @@ let (var_decl_are_inconsistent :
print_var_list out_sut;
failwith "\n*** env inputs and sut outputs should be the same.\n"
)
else if not(list_is_included in_or (List.append in_sut out_sut)) then
(
print_string "\noracle inputs: ";
print_var_list in_or;
print_string "\nsut inputs: ";
print_var_list in_sut;
print_string "\nsut outputs: ";
print_var_list out_sut;
failwith "\n*** Oracle inputs should be the union of sut inputs and outputs.\n"
)
else if (match out_or with [(_, "boolean")] -> false | _ -> true) then
(
print_string "\noracle outputs: ";
print_var_list out_or;
failwith "\n*** Oracle outputs should be of type boolean.\n"
)
else
()
......@@ -144,19 +127,14 @@ and
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
(sut_in, sut_out) = read_var_names "sut_var_names.txt"
in
let
(oracle_in, oracle_out) = read_var_names "oracle_var_names.txt"
in
let print_var_list vl =
List.iter (fun (t, v) -> print_string (v ^ ":" ^ t ^ ", ")) vl
in
Random.self_init ();
var_decl_are_inconsistent env_in env_out sut_in sut_out oracle_in oracle_out ;
var_decl_are_inconsistent env_in env_out
sut_input_var_name_and_type_list sut_output_var_name_and_type_list;
generate_env_graph [] "environment" ;
gv ("environment.ps");
......
......@@ -3,19 +3,6 @@
open Env
(*
** [var_decl_are_inconsistent in_env out_env in_sut out_sut in_or out_or]
** checks the consistency of variable declarations made in the environment,
** the SUT and the oracle.
*)
val var_decl_are_inconsistent : 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
-> unit
val main : int -> unit
;; -*- Prcs -*-
(Created-By-Prcs-Version 1 3 3)
(Project-Description "Lurette")
(Project-Version lurette perso 6)
(Parent-Version lurette 0 9)
(Version-Log "")
(Project-Version lurette 0 10)
(Parent-Version lurette perso 6)
(Version-Log "
lurette.ml:
Removing dead code.
")
(New-Version-Log "")
(Checkin-Time "Mon, 19 Nov 2001 16:09:29 +0100")
(Checkin-Time "Mon, 19 Nov 2001 16:25:51 +0100")
(Checkin-Login jahier)
(Populate-Ignore ())
(Project-Keywords)
......@@ -16,8 +19,8 @@
;; Sources files
(lurette.mli (lurette/11_lurette.ml 1.2 644))
(lurette.ml (lurette/12_lurette.ml 1.5 644))
(lurette.mli (lurette/11_lurette.ml 1.3 644))
(lurette.ml (lurette/12_lurette.ml 1.6 644))
(graph.mli (lurette/13_graph.mli 1.2 644))
(graph.ml (lurette/14_graph.ml 1.2 644))
......@@ -31,6 +34,7 @@
(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))
;; Documentation
......@@ -44,6 +48,18 @@
(interface/TAGS (lurette/26_TAGS 1.2 644))
(test.aut (lurette/22_test.aut 1.1 644))
;; Various files used for testing purposes
(vrai.lus (lurette/28_vrai.lus 1.1 644))
(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)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Lurette source files Version Mercury
(Mercury/memory.m (lurette/3_memory.m 1.1 644))
......@@ -62,17 +78,6 @@
; I have added graph__arc_content in the interface of this library module
(Mercury/graph.m (lurette/7_graph.m 1.1 644))
;; Files added by populate at Mon, 05 Nov 2001 14:16:21 +0100,
;; to version perso.4(w), by jahier:
(make_lurette (lurette/27_make_luret 1.2 744))
;; Files added by populate at Fri, 09 Nov 2001 13:34:18 +0100,
;; to version perso.5(w), by jahier:
(vrai.lus (lurette/28_vrai.lus 1.1 644))
(random_bool.aut (lurette/29_random_boo 1.1 644))
)
(Merge-Parents)
(New-Merge-Parents)
/********
* ec2c version 0.4-beta
* c file generated for node : vrai
********/
#include <stdlib.h>
#define _vrai_EC2C_SRC_FILE
#include "vrai.h"
/*--------
Internal structure for the call
--------*/
typedef struct {
void* client_data;
//INPUTS
_boolean _X;
_boolean _Y;
//OUTPUTS
_boolean _ok;
//REGISTERS
} vrai_ctx;
/*--------
Output procedures must be defined,
Input procedures must be used:
--------*/
void vrai_I_X(vrai_ctx* ctx, _boolean V){
ctx->_X = V;
}
void vrai_I_Y(vrai_ctx* ctx, _boolean V){
ctx->_Y = V;
}
extern void vrai_O_ok(void*, _boolean);
#ifdef CKCHECK
extern void vrai_BOT_ok(void*);
#endif
/*--------
Internal reset input procedure
--------*/
static void vrai_reset_input(vrai_ctx* ctx){
//NOTHING FOR THIS VERSION...
}
/*--------
Reset procedure
--------*/
void vrai_reset(vrai_ctx* ctx){
vrai_reset_input(ctx);
}
/*--------
Dynamic allocation of an internal structure
--------*/
vrai_ctx* vrai_new_ctx(void* cdata){
vrai_ctx* ctx = (vrai_ctx*)calloc(1, sizeof(vrai_ctx));
ctx->client_data = cdata;
vrai_reset(ctx);
return ctx;
}
/*--------
Copy the value of an internal structure
--------*/
void vrai_copy_ctx(vrai_ctx* dest, vrai_ctx* src){
memcpy((void*)dest, (void*)src, sizeof(vrai_ctx));
}
/*--------
Step procedure
--------*/
void vrai_step(vrai_ctx* ctx){
//LOCAL VARIABLES
//CODE
vrai_O_ok(ctx->client_data, _true);
}
/********
* ec2c version 0.4-beta
* c header file generated for node : vrai
* to be used with : vrai.c
********/
/*-------- Predefined types ---------*/
#ifndef _vrai_EC2C_PREDEF_TYPES
#define _vrai_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: vrai 2 1
//IN: _boolean X
//IN: _boolean Y
//OUT: _boolean ok
#ifndef _vrai_EC2C_SRC_FILE
/*--------Context type -------------*/
struct vrai_ctx;
/*--------Context allocation --------*/
extern struct vrai_ctx* vrai_new_ctx(void* client_data);
/*--------Context copy -------------*/
extern void vrai_copy_ctx(struct vrai_ctx* dest, struct vrai_ctx* src);
/*-------- Reset procedure -----------*/
extern void vrai_reset(struct vrai_ctx* ctx);
/*-------- Step procedure -----------*/
extern void vrai_step(struct vrai_ctx* ctx);
/*-------- Input procedures -------------*/
extern void vrai_I_X(struct vrai_ctx*, _boolean);
extern void vrai_I_Y(struct vrai_ctx*, _boolean);
#endif
Markdown is supported
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