Commit 3eddc777 authored by Erwan Jahier's avatar Erwan Jahier
Browse files

lurette 0.4 Mon, 08 Oct 2001 15:01:02 +0200 by jahier

Parent-Version:      0.3
Version-Log:

J'ai amélioré l'affichage de l'automate. Maintenant, il se met
a jour au dur et à mesure de l'execution.

Project-Description: empty
parent d0546ffc
...@@ -2,10 +2,12 @@ ...@@ -2,10 +2,12 @@
;; REALLY bad things. ;; REALLY bad things.
(Created-By-Prcs-Version 1 3 3) (Created-By-Prcs-Version 1 3 3)
(ID_EN_VRAC 2184 1002196285 0_ID_EN_VRAC 1.1) (ID_EN_VRAC 2184 1002196285 0_ID_EN_VRAC 1.1)
(Mmakefile 102 1002196285 1_Mmakefile 1.1) (env.m 9917 1002546062 4_env_automa 1.3)
(env_automata.m 11091 1002196285 4_env_automa 1.1) (test2.aut 1231 1002546062 8_test2.aut 1.1)
(Mmakefile 93 1002546062 1_Mmakefile 1.2)
(dot_automata.m 5814 1002546062 9_dot_automa 1.1)
(memory.m 3884 1002196285 3_memory.m 1.1) (memory.m 3884 1002196285 3_memory.m 1.1)
(graph.m 15076 1002205313 7_graph.m 1.1) (graph.m 15076 1002205313 7_graph.m 1.1)
(dot.m 3637 1002205313 6_dot.m 1.1) (dot.m 3636 1002298322 6_dot.m 1.2)
(lurette.m 3530 1002205313 5_lurette.m 1.2) (lurette.m 4247 1002546062 5_lurette.m 1.4)
(test1.aut 1108 1002196285 2_test1.aut 1.1) (test1.aut 1108 1002196285 2_test1.aut 1.1)
#!/bin/sh makefile #!/bin/sh makefile
# MCFLAGS = --trace deep MCFLAGS = --trace deep
# MLFLAGS = --trace MLFLAGS = --trace
# C2INITFLAGS = --trace C2INITFLAGS = --trace
MC = mmc MC = mmc
%-----------------------------------------------------------------------%
% 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).
...@@ -4,25 +4,24 @@ ...@@ -4,25 +4,24 @@
% Public License % Public License
%-----------------------------------------------------------------------% %-----------------------------------------------------------------------%
% File: env_automata.m % File: env.m
% Main author: jahier@imag.fr % Main author: jahier@imag.fr
% This module simulates the test environement for the lurette module. % This module simulates the test environement for lurette.
% It assumes that a description of the test environement exists in the % It assumes that a description of the test environement exists in the
% form of an automata whose arcs are labelled by weighted formula. This % 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 % 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 % third party tool, issued from, e.g., a Lutin or a Lustre spec.
% specification.
% %
% This module provides the automata data type, a procedure to read the % This module provides the automata data type, a procedure to read the
% automata from an *.aut file, as well as various procedures to to step % automata from an *.aut file, as well as various procedures to step
% through the automata. % through the automata.
%-----------------------------------------------------------------------% %-----------------------------------------------------------------------%
%-----------------------------------------------------------------------% %-----------------------------------------------------------------------%
:- module env_automata. :- module env.
:- interface. :- interface.
:- import_module list, int, graph, io, std_util. :- import_module list, int, graph, io, std_util.
...@@ -34,7 +33,7 @@ ...@@ -34,7 +33,7 @@
:- type node_content == int. :- type node_content == int.
:- type node == node(node_content). :- type node == node(node_content).
:- type arc_content == { weight, formula }. :- type arc_content == pair(weight, formula).
:- type arc == arc(arc_content). :- type arc == arc(arc_content).
:- type weight == int. :- type weight == int.
...@@ -66,7 +65,6 @@ ...@@ -66,7 +65,6 @@
% it is not really necessary as one can multiply the constraint % it is not really necessary as one can multiply the constraint
% (in)equality by the lcm (ppcm in french ;) of the coefficient % (in)equality by the lcm (ppcm in french ;) of the coefficient
% denominators. % denominators.
:- type expr :- type expr
...@@ -74,7 +72,7 @@ ...@@ -74,7 +72,7 @@
; minus(expr, expr) ; minus(expr, expr)
; times(expr, expr) ; times(expr, expr)
; div(expr, expr) ; div(expr, expr)
; val(string) ; val(string)
; int(int). ; int(int).
...@@ -104,13 +102,13 @@ ...@@ -104,13 +102,13 @@
:- func eval(formula, memory, int) = formula. :- func eval(formula, memory, int) = formula.
:- mode eval(in, memory_ui, in) = out is det. :- mode eval(in, memory_ui, in) = out is det.
%-----------------------------------------------------------------------%
%-----------------------------------------------------------------------% %-----------------------------------------------------------------------%
:- implementation. :- implementation.
:- import_module string, bool, float, set, std_util, require. :- import_module string, bool, float, set, std_util, require.
:- import_module lurette. :- import_module lurette.
%-----------------------------------------------------------------------% %-----------------------------------------------------------------------%
:- type read_automata :- type read_automata
...@@ -176,7 +174,8 @@ add_an_arc(edge(SourceNodeL, FormulaL, TargetNodeL), Aut0, Aut) :- ...@@ -176,7 +174,8 @@ add_an_arc(edge(SourceNodeL, FormulaL, TargetNodeL), Aut0, Aut) :-
; ;
graph__det_insert_node(Aut1, TargetNodeL, TargetNode, Aut2) graph__det_insert_node(Aut1, TargetNodeL, TargetNode, Aut2)
), ),
graph__det_insert_edge(Aut2, SourceNode, TargetNode, FormulaL, _Formula, Aut). graph__det_insert_edge(Aut2, SourceNode, TargetNode, FormulaL,
_Formula, Aut).
%-----------------------------------------------------------------------% %-----------------------------------------------------------------------%
...@@ -186,8 +185,8 @@ try(A, Node) = ArcArcInfoPairList :- ...@@ -186,8 +185,8 @@ try(A, Node) = ArcArcInfoPairList :-
list__filter_map(select_arcs(A, Node), ArcList, ArcArcInfoPairList). list__filter_map(select_arcs(A, Node), ArcList, ArcArcInfoPairList).
:- pred select_arcs(automata::in, node::in, env_automata__arc::in, :- pred select_arcs(automata::in, node::in, env__arc::in,
{ env_automata__arc, arc_content }::out) is semidet. { env__arc, arc_content }::out) is semidet.
select_arcs(A, Node, Arc, ArcArcInfoPair) :- select_arcs(A, Node, Arc, ArcArcInfoPair) :-
graph__arc_contents(A, Arc, Node, _, ArcInfo), graph__arc_contents(A, Arc, Node, _, ArcInfo),
ArcArcInfoPair = { Arc, ArcInfo }. ArcArcInfoPair = { Arc, ArcInfo }.
...@@ -199,12 +198,6 @@ step(A, Arc) = Node :- ...@@ -199,12 +198,6 @@ step(A, Arc) = Node :-
%-----------------------------------------------------------------------% %-----------------------------------------------------------------------%
% 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 eval(formula, memory, int) = formula.
eval(true, _, _) = true. eval(true, _, _) = true.
eval(false, _, _) = false. eval(false, _, _) = false.
...@@ -212,45 +205,38 @@ eval(eps, _, _) = eps. ...@@ -212,45 +205,38 @@ eval(eps, _, _) = eps.
eval(and(Fl0, Fr0), Mem, D) = F :- eval(and(Fl0, Fr0), Mem, D) = F :-
Fl1 = eval(Fl0, Mem, D), Fl1 = eval(Fl0, Mem, D),
( if Fl1 = false then ( if Fl1 = false then F = false
F = false
else else
Fr1 = eval(Fr0, Mem, D), Fr1 = eval(Fr0, Mem, D),
( if Fl1 = true then F = Fr1 ( if Fl1 = true then F = Fr1
else if Fr1 = false then F = false else if Fr1 = false then F = false
else if Fr1 = true then F = Fl1 else if Fr1 = true then F = Fl1
else F = and(Fl1, Fr1) else F = and(Fl1, Fr1) )
)
). ).
% use `not' and `and' instead ?
eval(or(Fl0, Fr0), Mem, D) = F :- eval(or(Fl0, Fr0), Mem, D) = F :-
Fl1 = eval(Fl0, Mem, D), Fl1 = eval(Fl0, Mem, D),
( if Fl1 = true then ( if Fl1 = true then F = true
F = true
else else
Fr1 = eval(Fr0, Mem, D), Fr1 = eval(Fr0, Mem, D),
( if Fl1 = false then F = Fr1 ( if Fl1 = false then F = Fr1
else if Fr1 = true then F = true else if Fr1 = true then F = true
else if Fr1 = false then F = Fl1 else if Fr1 = false then F = Fl1
else F = and(Fl1, Fr1) else F = and(Fl1, Fr1) )
)
). ).
eval(not(F0), Mem, D) = F :- eval(not(F0), Mem, D) = F :-
( if F0 = false then F = true ( if F0 = false then F = true
else if F0 = true then F = false else if F0 = true then F = false
else F = not(eval(F0, Mem, D)) else F = not(eval(F0, Mem, D)) ).
).
eval(pos(Polynome), Mem, D) = F :- eval(pos(Polynome), Mem, D) = F :-
Polynome1 = eval_polynome(Polynome, Mem, D), Polynome1 = eval_polynome(Polynome, Mem, D),
( ( if Polynome1 = { [], Expr } then
Polynome1 = { [], Expr }
->
( (eval_expr(Expr) < float(0)) -> F = true ; F = false ) ( (eval_expr(Expr) < float(0)) -> F = true ; F = false )
; else
F = pos(Polynome1) F = pos(Polynome1) ).
).
% % XXX How can I avoid this duplicated code? % % XXX How can I avoid this duplicated code?
% eval(pos_eq(Polynome), Mem, D) = F :- % eval(pos_eq(Polynome), Mem, D) = F :-
...@@ -265,23 +251,18 @@ eval(pos(Polynome), Mem, D) = F :- ...@@ -265,23 +251,18 @@ eval(pos(Polynome), Mem, D) = F :-
eval(b(VarName), Mem, D) = Val :- eval(b(VarName), Mem, D) = Val :-
Val0 = memory__lookup(Mem, VarName, D), Val0 = memory__lookup(Mem, VarName, D),
( (
Val0 = memory__u Val0 = memory__u,
->
Val = b(VarName) Val = b(VarName)
; ;
Val0 = memory__b(Bool) Val0 = memory__b(Bool),
->
Val = bool_to_formula(Bool) Val = bool_to_formula(Bool)
; ;
Val0 = memory__val(_String),
% Should not occur, by construction
% How could I make mmc statically check that? % How could I make mmc statically check that?
% I can have 3 different arrays for bools, ints and rats,
% but then I have to duplicate the code to init, lookup,
% and set each of those arrays...
% Moreover, I need to encapsulate values to be able to
% handle unknown values straightforwardly
% %
error("Boolean expected; there is a Bug in memory.m ") error("Boolean expected; there is probably a Bug in memory.m ")
). ).
...@@ -308,10 +289,9 @@ bool_to_formula(no) = false. ...@@ -308,10 +289,9 @@ bool_to_formula(no) = false.
%-----------------------------------------------------------------------% %-----------------------------------------------------------------------%
% XXX Cette fonction devra plutot etre importe pour tre sur que les % XXX This ougth to be done in an external (C?) module that is also used
% conversions et les calculs en gnral soient cohrents avec ceux % by the constraint solver (for consistency).
% fait dans le solveur. %
:- func eval_expr(expr) = float. :- func eval_expr(expr) = float.
eval_expr(plus(Expr1, Expr2)) = eval_expr(Expr1) + eval_expr(Expr2). eval_expr(plus(Expr1, Expr2)) = eval_expr(Expr1) + eval_expr(Expr2).
...@@ -319,9 +299,9 @@ eval_expr(minus(Expr1, Expr2)) = eval_expr(Expr1) - eval_expr(Expr2). ...@@ -319,9 +299,9 @@ eval_expr(minus(Expr1, Expr2)) = eval_expr(Expr1) - eval_expr(Expr2).
eval_expr(times(Expr1, Expr2)) = eval_expr(Expr1) * eval_expr(Expr2). eval_expr(times(Expr1, Expr2)) = eval_expr(Expr1) * eval_expr(Expr2).
eval_expr(div(Expr1, Expr2)) = eval_expr(Expr1) / eval_expr(Expr2). eval_expr(div(Expr1, Expr2)) = eval_expr(Expr1) / eval_expr(Expr2).
eval_expr(val(String)) = Float :- eval_expr(val(String)) = Float :-
( string__to_float(String, Float0) -> ( if string__to_float(String, Float0) then
Float = Float0 Float = Float0
; else
error("Bad format; can't convert to float.") error("Bad format; can't convert to float.")
). ).
eval_expr(int(Int)) = Float :- eval_expr(int(Int)) = Float :-
...@@ -329,8 +309,8 @@ eval_expr(int(Int)) = Float :- ...@@ -329,8 +309,8 @@ eval_expr(int(Int)) = Float :-
:- func memory_num_val_to_expr(memory__element) = expr. :- func memory_num_val_to_expr(memory__element) = expr.
memory_num_val_to_expr(Elt) = Expr :- memory_num_val_to_expr(Elt) = Expr :-
( Elt = memory__val(String) -> ( if Elt = memory__val(String) then
Expr = val(String) Expr = val(String)
; else
error("Numerical value expected.") error("Numerical value expected.")
). ).
...@@ -16,7 +16,7 @@ ...@@ -16,7 +16,7 @@
% Les pamamtres du test sont : % Les pamamtres du test sont :
% - L : taille de la squence % - L : taille de la squence
% - N : paisseur du test % - N : paisseur du test
% - ??: nombre de séquence (c'est quoi ca ?) % - ??: nombre de squence
% - L'environnement % - L'environnement
% - L'oracle % - L'oracle
% - le SUT % - le SUT
...@@ -66,57 +66,75 @@ ...@@ -66,57 +66,75 @@
:- implementation. :- implementation.
:- import_module bool, list, memory, env_automata, dot. :- import_module bool, list, memory, env, dot_automata, graph, random.
:- import_module std_util.
main --> main -->
print("lurette... "), nl, io__command_line_arguments(Args),
{ TestFile = "test1.aut" }, (
read_automata(TestFile, Automata, InitNode, FinalNodes, InVarList, OutVarList), { Args = [TestFile|_] }
% dot__display_graph(TestFile, Automata), ->
{ Mem = memory__init(InVarList ++ OutVarList, 10) }, print("lurette... "), nl,
loop(Mem, Automata, InitNode, FinalNodes, Mem2), read_automata(TestFile, Automata, InitNode, FinalNodes, InVarList,
memory__dump(Mem2). OutVarList),
{ graph__node_contents(Automata, InitNode, Int) },
dot_automata__generate_graph(none, Int, TestFile, Automata),
:- pred loop(memory, automata, node, list(node), memory, io__state, io__state). dot_automata__display_graph(TestFile),
:- mode loop(memory_di, in, in, in, memory_uo, di, uo) is det. { Mem = memory__init(InVarList ++ OutVarList, 10) },
loop(Mem0, A, InitNode, FinalNodes, Mem) --> { random__init(73, RS) },
print("*** Le Noeud courant est le noeud "), test_lurette_loop(Mem, Automata, InitNode, FinalNodes, TestFile,