Skip to content

GitLab

Commit d22646a1 authored by Erwan Jahier's avatar Erwan Jahier
Browse files

lurette 0.14 Mon, 03 Dec 2001 12:45:17 +0100 by jahier 

Parent-Version:      0.13
Version-Log:

Now lurette can hanble multiple environements that can either be
run as a product or in parallel.
Project-Description: Lurette
parent 308a21af
Expand all Hide whitespace changes
Inline Side-by-side
.lurette.prcs_aux
View file @ d22646a1
;; 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 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 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)
(test/vrai.h 1120 1006183551 31_vrai.h 1.1)
(source/env_state.ml 1378 1007379917 51_env_state. 1.1)
(source/graph.ml 2397 1003932490 14_graph.ml 1.2)
(test/tram_env_porte.env 857 1007379917 b/11_tram_env_p 1.1)
(source/util.ml 3175 1007379917 35_util.ml 1.2)
(source/wtree.ml 9181 1007379917 b/1_wtree.ml 1.1)
(source/solver.ml 1841 1007379917 39_solver.ml 1.1)
(source/lurette.ml 6270 1007379917 12_lurette.ml 1.9)
(source/solver.mli 617 1007379917 38_solver.mli 1.1)
(source/env.mli 2838 1007379917 15_env.mli 1.5)
(test/vrai.lus 65 1006182545 28_vrai.lus 1.1)
(lurette.depfull.dot 1146 1007379917 b/5_lurette.de 1.1)
(test/tram_env_tramway.env 1207 1007379917 b/10_tram_env_t 1.1)
(source/env.ml 7966 1007379917 16_env.ml 1.8)
(make_lurette 1008 1007379917 27_make_luret 1.4)
(test/vrai_tram.lus 453 1007379917 b/6_vrai_tram. 1.1)
(test/edge.c 1693 1006263320 32_edge.c 1.1)
(lurette.dep.dot 485 1007379917 b/4_lurette.de 1.1)
(doc/archi.fig 3693 1003928781 20_archi.fig 1.1)
(make_lurette 1121 1006263320 27_make_luret 1.3)
(Makefile 332 1006433610 18_Makefile 1.7)
(interface/Makefile 123 1006263320 25_Makefile 1.4)
(OcamlMakefile 15015 1004519854 17_OcamlMakef 1.2)
(source/parse_env.mli 788 1007379917 40_parse_env. 1.1)
(ID_EN_VRAC 2184 1002196285 0_ID_EN_VRAC 1.1)
(test/edge.h 1052 1006263320 33_edge.h 1.1)
(doc/automata_format 0 1007379917 b/3_automata_f 1.1)
(source/eval.ml 6238 1007379917 49_eval.ml 1.1)
(source/parse_env.ml 6007 1007379917 41_parse_env. 1.1)
(interface/gen_stubs.ml 31593 1007379917 24_generate_l 1.9)
(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 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 44 1006433610 11_lurette.ml 1.5)
(TAGS 5673 1006182545 21_TAGS 1.5)
(vrai.c 1405 1006183551 30_vrai.c 1.1)
(util.ml 2865 1006433610 35_util.ml 1.1)
(lurette.ml 5064 1006433610 12_lurette.ml 1.8)
(doc/Interface_draft 5232 1003928781 19_Interface_ 1.1)
(source/formula.mli 1735 1007379917 44_formula.ml 1.1)
(test/tram_env_usager.env 801 1007379917 b/9_tram_env_u 1.1)
(TAGS 9825 1007379917 21_TAGS 1.6)
(source/wtree.mli 2906 1007379917 b/0_wtree.mli 1.1)
(source/env_state.mli 897 1007379917 50_env_state. 1.1)
(interface/sut_idl_stub.ml 338 1006263457 34_sut_idl_st 1.1)
(edge.c 1693 1006263320 32_edge.c 1.1)
(source/eval.mli 498 1007379917 48_eval.mli 1.1)
(README 0 1002791390 10_README 1.1)
(OcamlMakefile 15998 1007379917 17_OcamlMakef 1.3)
(source/show_env.ml 3303 1007379917 43_show_env.m 1.1)
(test/tram_simple.c 5627 1006433610 37_tram_simpl 1.1)
(doc/synthese 2556 1007379917 b/2_synthese 1.1)
(interface/Makefile 123 1006263320 25_Makefile 1.4)
(source/show_env.mli 848 1007379917 42_show_env.m 1.1)
(test/tram_simple.h 1746 1006433610 36_tram_simpl 1.1)
(Makefile 1218 1007379917 18_Makefile 1.8)
(test/vrai_tram.c 2855 1007379917 b/8_vrai_tram. 1.1)
(source/print.mli 108 1007379917 46_print.mli 1.1)
(source/graph.mli 1305 1003932490 13_graph.mli 1.2)
(source/formula.ml 3404 1007379917 45_formula.ml 1.1)
(test/vrai.c 1405 1006183551 30_vrai.c 1.1)
(source/lurette.mli 38 1007379917 11_lurette.ml 1.6)
(source/print.ml 1098 1007379917 47_print.ml 1.1)
(test/vrai_tram.h 2293 1007379917 b/7_vrai_tram. 1.1)
Makefile
View file @ d22646a1
OCAMLMAKEFILE = ./OcamlMakefile
LURETTE_DIR = /home/jahier/lurette
OCAMLMAKEFILE = $(LURETTE_DIR)/OcamlMakefile
-include lurette.in
-include ./lurette.in
SOURCES = $(SUT) \
sut_stub.c sut_idl_stub.idl \
$(ORACLE) \
oracle_stub.c oracle_idl_stub.idl \
OCAML_DEFAULT_DIRS=$(LURETTE_DIR)/source
SOURCES = $(SUT) sut_stub.c sut_idl_stub.idl \
$(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
$(LURETTE_DIR)/source/util.ml \
$(LURETTE_DIR)/source/graph.mli $(LURETTE_DIR)/source/graph.ml \
$(LURETTE_DIR)/source/formula.mli $(LURETTE_DIR)/source/formula.ml \
$(LURETTE_DIR)/source/print.mli $(LURETTE_DIR)/source/print.ml \
$(LURETTE_DIR)/source/env_state.mli $(LURETTE_DIR)/source/env_state.ml \
$(LURETTE_DIR)/source/eval.mli $(LURETTE_DIR)/source/eval.ml \
$(LURETTE_DIR)/source/solver.mli $(LURETTE_DIR)/source/solver.ml \
$(LURETTE_DIR)/source/wtree.mli $(LURETTE_DIR)/source/wtree.ml \
$(LURETTE_DIR)/source/parse_env.mli $(LURETTE_DIR)/source/parse_env.ml \
$(LURETTE_DIR)/source/env.mli $(LURETTE_DIR)/source/env.ml \
$(LURETTE_DIR)/source/show_env.mli $(LURETTE_DIR)/source/show_env.ml \
$(LURETTE_DIR)/source/lurette.mli $(LURETTE_DIR)/source/lurette.ml
RESULT = lurette
-include $(OCAMLMAKEFILE)
Mercury/Mmakefile deleted 100644 → 0
View file @ 308a21af
#!/bin/sh makefile
# MCFLAGS = --trace deep
# MLFLAGS = --trace
# C2INITFLAGS = --trace
MC = mmc
Mercury/dot.m deleted 100644 → 0
View file @ 308a21af
%-----------------------------------------------------------------------%
% Copyright (C) 2001 - Verimag.
% This file may only be copied under the terms of the GNU Library General
% Public License
%-----------------------------------------------------------------------%
% File: dot
% Main author: jahier@imag.fr
% Display a graph with dot.
:- module dot.
%-----------------------------------------------------------------------%
:- interface.
:- import_module string, io, graph.
:- pred display_graph(string, graph(N, A), io__state, io__state).
:- mode display_graph(in, in, di, uo) is det.
%-----------------------------------------------------------------------%
:- implementation.
:- import_module list, require, set.
display_graph(String, Graph) -->
{ TmpFile = String ++ ".tmp" },
{ DotFile = String ++ ".dot" },
{ PsFile = String ++ ".ps" },
io__tell(TmpFile, ResTmp),
(
{ ResTmp = error(ErrMsg) },
print(ErrMsg),
{ error("Can't open " ++ TmpFile ++ "for output in tmp.m") }
;
{ ResTmp = ok },
dump_graph(Graph),
io__told
),
% Calling sed
{ CallSed = "sed y/\\\"/' '/ " ++ TmpFile ++ " | sed y/\\'/\\\"/ > " ++ DotFile },
print(CallSed), nl,
io__call_system(CallSed, ResSedCall),
( { ResSedCall = ok(_) } ; { ResSedCall = error(ErrMsg3) }, print(ErrMsg3) ),
% Calling dot to create the postscript file
{ CallDot = "dot -Tps " ++ DotFile ++ " -o " ++ PsFile },
print(CallDot), nl,
io__call_system(CallDot, ResDotCall),
( { ResDotCall = ok(_) } ; { ResDotCall = error(ErrMsg2) }, print(ErrMsg2) ),
% Calling gv
{ CallGv = "gv " ++ PsFile },
print(CallGv), nl,
io__call_system(CallGv, ResGvCall),
( { ResGvCall = ok(_) } ; { ResGvCall = error(ErrMsg4) }, print(ErrMsg4) ).
:- type arc(N, A) ---> arc(N, A, N).
:- type arc ---> some [N, A] arc(N, A).
:- pred dump_graph(graph(N, A), io__state, io__state).
:- mode dump_graph(in, di, uo) is det.
dump_graph(Graph) -->
print("digraph G {\n\n"),
print("ordering=out;\n\n"),
{ graph__nodes(Graph, NodesSet) },
{ NodesInfoSet = set__map(graph__node_contents(Graph), NodesSet) },
{ set__to_sorted_list(NodesInfoSet, NodesInfoList) },
dump_nodes(NodesInfoList),
{ graph_to_arc_list(Graph, ArcList) },
dump_arc(ArcList),
print("}\n").
:- pred graph_to_arc_list(graph(N, A), list(arc(N, A))).
:- mode graph_to_arc_list(in, out) is det.
graph_to_arc_list(Graph, ArcList) :-
graph__arcs(Graph, GraphArcList),
list__map(graph_arc_to_arc(Graph), GraphArcList, ArcList).
:- pred graph_arc_to_arc(graph(N, A), graph__arc(A), arc(N, A)).
:- mode graph_arc_to_arc(in, in, out) is det.
graph_arc_to_arc(Graph, GraphArc, Arc) :-
graph__arc_contents(Graph, GraphArc, Start, End, ArcInfo),
node_contents(Graph, Start, StartInfo),
node_contents(Graph, End, EndInfo),
Arc = arc(StartInfo, ArcInfo, EndInfo).
:- pred dump_arc(list(arc(N, A)), io__state, io__state).
:- mode dump_arc(in, di, uo) is det.
dump_arc([]) -->
nl.
% dump_arc([arc(X,Y)|CG]) -->
% print("\t"), print(X), print(" -> "), print(Y ), print(";\n"),
% dump_arc(CG).
dump_arc([arc(X, Label, Y)|CG]) -->
print("\t"),
print(X),
print(" -> "),
print(Y),
print(" [label=\' "),
print(Label),
print("\' ];\n"),
dump_arc(CG).
:- pred dump_nodes(list(N), io__state, io__state).
:- mode dump_nodes(in, di, uo) is det.
dump_nodes([]) --> [].
dump_nodes([X|Xs]) -->
print("\t \t"),
print(X),
print("\n"),
dump_nodes2(Xs).
:- pred dump_nodes2(list(N), io__state, io__state).
:- mode dump_nodes2(in, di, uo) is det.
dump_nodes2([]) --> nl.
dump_nodes2([X|Xs]) -->
print("\t ; \t "), print(X ), print("\n"),
dump_nodes2(Xs).
Mercury/dot_automata.m deleted 100644 → 0
View file @ 308a21af
%-----------------------------------------------------------------------%
% Copyright (C) 2001 - Verimag.
% This file may only be copied under the terms of the GNU Library General
% Public License
%-----------------------------------------------------------------------%
% File: dot
% Main author: jahier@imag.fr
% Display a graph with dot.
:- module dot_automata.
%-----------------------------------------------------------------------%
:- interface.
:- import_module string, io, env.
:- type arc_to_color
---> none
; to_color(env__arc, formula).
:- pred display_graph(string, io__state, io__state).
:- mode display_graph(in, di, uo) is det.
:- pred generate_graph(arc_to_color, int, string, automata, io__state, io__state).
:- mode generate_graph(in, in, in, in, di, uo) is det.
%-----------------------------------------------------------------------%
:- implementation.
:- import_module int, list, require, set, graph, std_util.
generate_graph(Arc, Node, String, Graph) -->
{ TmpFile = String ++ ".tmp" },
{ DotFile = String ++ ".dot" },
{ PsFile = String ++ ".ps" },
io__tell(TmpFile, ResTmp),
(
{ ResTmp = error(ErrMsg) },
print(ErrMsg),
{ error("Can't open " ++ TmpFile ++ "for output in tmp.m") }
;
{ ResTmp = ok },
dump_graph(Arc, Node, Graph),
io__told
),
% Calling sed
{ CallSed = "sed y/\\\"/' '/ " ++ TmpFile ++ " | sed y/\\'/\\\"/ > " ++ DotFile },
% print(CallSed), nl,
io__call_system(CallSed, ResSedCall),
( { ResSedCall = ok(_) } ; { ResSedCall = error(ErrMsg3) }, print(ErrMsg3) ),
% Calling dot to create the postscript file
{ CallDot = "dot -Tps " ++ DotFile ++ " -o " ++ PsFile },
% print(CallDot), nl,
io__call_system(CallDot, ResDotCall),
( { ResDotCall = ok(_) } ; { ResDotCall = error(ErrMsg2) }, print(ErrMsg2) ).
display_graph(String) -->
{ PsFile = String ++ ".ps" },
% Calling gv
{ CallGv = "gv " ++ PsFile ++ " &"},
print(CallGv), nl,
io__call_system(CallGv, ResGvCall),
( { ResGvCall = ok(_) } ; { ResGvCall = error(ErrMsg4) }, print(ErrMsg4) ).
:- pred dump_graph(arc_to_color, int, automata, io__state, io__state).
:- mode dump_graph(in, in, in, di, uo) is det.
dump_graph(ArcToColor, Node, Graph) -->
print("digraph G {\n\n"),
print("ordering=out;\n\n"),
{ graph__nodes(Graph, NodesSet) },
{ NodesInfoSet = set__map(graph__node_contents(Graph), NodesSet) },
{ set__to_sorted_list(NodesInfoSet, NodesInfoList) },
dump_nodes(Node, NodesInfoList),
{ graph_to_arc_list(Graph, ArcList) },
dump_arc(Graph, ArcToColor, ArcList),
print("}\n").
:- type edge ---> arc(node_content, pair(env__arc, arc_content), node_content).
:- pred graph_to_arc_list(automata, list(edge)).
:- mode graph_to_arc_list(in, out) is det.
graph_to_arc_list(Graph, ArcList) :-
graph__arcs(Graph, GraphArcList),
list__map(graph_arc_to_arc(Graph), GraphArcList, ArcList).
:- pred graph_arc_to_arc(automata, env__arc, edge).
:- mode graph_arc_to_arc(in, in, out) is det.
graph_arc_to_arc(Graph, GraphArc, Arc) :-
graph__arc_contents(Graph, GraphArc, Start, End, ArcInfo),
node_contents(Graph, Start, StartInfo),
node_contents(Graph, End, EndInfo),
Arc = arc(StartInfo, GraphArc - ArcInfo, EndInfo).
:- pred dump_arc(automata, arc_to_color, list(edge), io__state, io__state).
:- mode dump_arc(in, in, in, di, uo) is det.
dump_arc(_Graph, _ArcToColor, []) --> nl.
dump_arc(Graph, ArcToColorInfo, [arc(X, Arc - Label, Y)|CG]) -->
print("\t"),
print(X),
print(" -> "),
print(Y),
print(" [label=\' "),
print_arc_label(Label),
(
{ ArcToColorInfo = to_color(ArcToColor, EvaluatedFormula) },
{ ArcToColor = Arc }
->
print("\\n --> "),
print_formula(EvaluatedFormula),
print("\' , style=filled,color=red,fontcolor=red]\n")
;
print("\' ];\n\n")
),
dump_arc(Graph, ArcToColorInfo, CG).
:- pred print_formula(formula, io__state, io__state).
:- mode print_formula(in, di, uo) is det.
print_formula(F) -->
( { F = pos({[{Int, var(VarNum)}|Tail], Const})} ->
print(Int),
print(VarNum),
list__foldl(print_coef, Tail),
print(" > "),
(
{ Const = int(N) }
->
print(N)
;
{ Const = val(V) }
->
print(V)
;
print(Const)
)
;
print(F)
).
:- pred dump_nodes(int, list(int), io__state, io__state).
:- mode dump_nodes(in, in, di, uo) is det.
dump_nodes(_Node, []) --> [].
dump_nodes(Node, [X|Xs]) -->
print("\t \t"),
print(X),
( { X = Node } ->
print(" [style=filled,color=red]\n")
;
print("\n")
),
dump_nodes2(Node, Xs).
:- pred dump_nodes2(int, list(int), io__state, io__state).
:- mode dump_nodes2(in, in, di, uo) is det.
dump_nodes2(_Node, []) --> nl.
dump_nodes2(Node, [X|Xs]) -->
print("\t ; \t "),
print(X ),
( { X = Node } ->
print(" [style=filled,color=red]\n")
;
print("\n")
),
dump_nodes2(Node, Xs).
%-----------------------------------------------------------------------%
%-----------------------------------------------------------------------%
:- pred print_arc_label(arc_content, io__state, io__state).
:- mode print_arc_label(in, di, uo) is det.
print_arc_label(Arc) -->
( { Arc = Weigth - pos({[{Int, var(VarNum)}|Tail], Const})} ->
print(Weigth),
print(" : "),
print(Int), print(VarNum),
list__foldl(print_coef, Tail),
print(" > "),
( { Const = int(N) } -> print(N) ; print(Const))
;
{ Arc = Weigth - Formula },
print(Weigth),
print(" : "),
print(Formula)
).
:- pred print_coef({int, var_num}, io__state, io__state).
:- mode print_coef(in, di, uo) is det.
print_coef({Int, var(VarNum)}) -->
( { Int > 0 } ->
print(" + "),
( { Int \= 1 } -> print(Int) ; print("+ ") )
;
print(" "),
( { Int \= -1 } -> print(Int) ; print("- ") )
),
% print("."),
print(VarNum).
Mercury/env.m deleted 100644 → 0
View file @ 308a21af
%-----------------------------------------------------------------------%
% Copyright (C) 2001 - Verimag.
% This file may only be copied under the terms of the GNU Library General
% Public License
%-----------------------------------------------------------------------%
% File: env.m
% Main author: jahier@imag.fr
% This module simulates the test environement for lurette.
% It assumes that a description of the test environement exists in the
% form of an automata whose arcs are labelled by weighted formula. This
% description is read from an *.aut file that has been produced by a
% third party tool, issued from, e.g., a Lutin or a Lustre spec.
%
% This module provides the automata data type, a procedure to read the
% automata from an *.aut file, as well as various procedures to step
% through the automata.
%-----------------------------------------------------------------------%
%-----------------------------------------------------------------------%
:- module env.
:- interface.
:- import_module list, int, graph, io, std_util.
:- import_module memory.
% An automata is a graph whose arcs are labelled by weighted formula
:- type automata == graph(node_content, arc_content).
:- type node_content == int.
:- type node == node(node_content).
:- type arc_content == pair(weight, formula).
:- type arc == arc(arc_content).
:- type weight == int.
:- type formula
---> and(formula, formula)
; or(formula, formula)
; not(formula)
; true
; false
; b(string) % boolean identifier
% Linear Constraints
; pos(polynome) % S_i^n ai.xi + b > 0
% ; pos_eq(polynome) % S_i^n ai.xi + b >= 0
% XXX
; eps. % epsilon transition
% Type of the (free) numerical variables that appear in formula.
:- type var_num ---> var(string).
:- type polynome == { list({ int, var_num }), expr }.
% `{[{3, i("a")}, {2, i("b")}, {-1, i("c")}], 3}' represents
% the polynome `3*a + 2*b - c + 3', where a, b, c are integers.
%
% Note that we could have had rational coefficients here too, but
% it is not really necessary as one can multiply the constraint
% (in)equality by the lcm (ppcm in french ;) of the coefficient
% denominators.
:- type expr
---> plus(expr, expr)
; minus(expr, expr)
; times(expr, expr)
; div(expr, expr)
; val(string)
; int(int).
%-----------------------------------------------------------------------%
% read_automata(File, Automata, InitNode, FinalNode, InVar, OutVar)
% returns the automata contained in File, as well as its init and final
% nodes, and its input and output variable list.
:- pred read_automata(string, automata, node, list(node),
list(pair(string)), list(pair(string)),
io__state, io__state).
:- mode read_automata(in, out, out, out, out, out, di, uo) is det.
% env__try(A, Node) returns the list of arc
% corresponding to the possible transitions in the automata A
% starting from the node Node.
:- func env__try(automata, node) = list({ env__arc, arc_content }).
% env__step(A, Arc) returns the target node of the arc Arc.
:- func env__step(automata, env__arc) = node.
% env__eval(F, Mem, N) returns an evaluated version of the
% formula F. Input variables as well as variables ``under a pre''
% are replaced by their values. Then, the formula is normalized,
% i.e., the closed sub-terms of the formula are simplified.
:- func env__eval(formula, memory, int) = formula.
:- mode env__eval(in, memory_ui, in) = out is det.
%-----------------------------------------------------------------------%
%-----------------------------------------------------------------------%
:- implementation.
:- import_module string, bool, float, set, std_util, require.
:- import_module lurette.
%-----------------------------------------------------------------------%
:- type read_automata
---> automata(node_content, list(node_content),
list(pair(string)), list(pair(string)), list(edge)).
:- type edge ---> edge(node_content, arc_content, node_content).
read_automata(FileName, A, InitNode, FinalNodeList,