Commit 7a6c0066 authored by Erwan Jahier's avatar Erwan Jahier
Browse files

lurette 0.1 Thu, 04 Oct 2001 13:51:25 +0200 by jahier

Version-Log:         empty
Project-Description: empty
parents
;; This file is automatically generated, editing may cause PRCS to do
;; REALLY bad things.
(Created-By-Prcs-Version 1 3 3)
(ID_EN_VRAC 2184 1002196285 0_ID_EN_VRAC 1.1)
(Mmakefile 102 1002196285 1_Mmakefile 1.1)
(env_automata.m 11091 1002196285 4_env_automa 1.1)
(memory.m 3884 1002196285 3_memory.m 1.1)
(lurette.m 3456 1002196285 5_lurette.m 1.1)
(test1.aut 1108 1002196285 2_test1.aut 1.1)
* Une propriété de programme que l'on arrive pas à prouver avec un
outil de vérification peut servir d'oracle à un outil de test.
=> L'outil de test et l'outil de verif doivent donc être intégrés
La question est : dans quel langage exprimer ces propriétés ?
* Il y a deux langages différents :
1) le langage pour exprimer les contraintes sur l'environnement (Lenv)
2) le langage pour spécifier l'oracle (Loracle)
Question. Doit-on avoir : Lenv = Loracle ???
Pourquoi pas. La différence étant que Lenv est un générateur, et que
Loracle n'est qu'un accepteur. Mais, bon, qui peut le plus peut le
moins.
* Pour l'instant, Lenv = Loracle = Lustre
-> Lustre ne suffit pas pour Lenv et Loracle car il ne permet pas
d'exprimer facilement la séquence (Reglo le fait).
-> Lustre (pas plus que Reglo d'ailleur) ne suffit pas pour Lenv car
il ne permet pas d'exprimer des pondérations (probas) sur les
différentes branches de l'automate représentant la propriété. Pour
l'oracle, ceci n'a aucune espèce d'importance puisque c'est juste un
accepteur, pas un générateur.
* Remarque en passant. Modéliser l'environnement ca revient à la même
chose que de modéliser les sorties de programmes pas encore écrits
(stubs).
* comparaison Lustre / Lutin
------------------------------------------------------------
Lustre | Lutin
------------------------------------------------------------
pas de séquence (1) | Séquences (via les reg expr)
|
équationnel | relationnel
(donc) déterministe | indéterministe (2)
|
pas de probas (3) | des probas
(puisque déterministe ...)|
|
------------------------------------------------------------
(1) i.e., la possibilité d'exprimer facilement la séquence. C'est
possible en Lustre, mais super lourdingue.
(2) L'indéterminisme n'est pas un problème ni pour l'oracle ni pour
Lenv car on n'a pas de contraintes temps-réels sur les propriétés
qu'ils expriment.
(3) la possibilité de pondérer les branches par des probas n'est
utile que quand on se sert des noeuds en tant que générateurs. En
d'autre terme, on ne s'en servira pas pour écrire les oracles.
#!/bin/sh makefile
# MCFLAGS = --trace deep
# MLFLAGS = --trace
# C2INITFLAGS = --trace
MC = mmc
%-----------------------------------------------------------------------%
% Copyright (C) 2001 - Verimag.
% This file may only be copied under the terms of the GNU Library General
% Public License
%-----------------------------------------------------------------------%
% File: env_automata.m
% Main author: jahier@imag.fr
% This module simulates the test environement for the lurette module.
% 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
% specification.
%
% 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
% through the automata.
%-----------------------------------------------------------------------%
%-----------------------------------------------------------------------%
:- module env_automata.
:- 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 == { 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.
% try(A, Node) returns the list of arc
% corresponding to the possible transitions in the automata A
% starting from the node Node.
:- func try(automata, node) = list({ arc(arc_content), arc_content }).
% step(A, Arc) returns the target node of the arc Arc.
:- func step(automata, arc(arc_content)) = 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.
:- mode 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,
VarListIn, VarListOut) -->
io__see(FileName, Res),
( { Res = ok } ->
io__read(ReadRes),
io__seen,
( { ReadRes = ok(automata(InitLabel, FinalLabelList, VarListIn0,
VarListOut0, ArcList)) } ->
{ list__foldl(add_an_arc, ArcList, graph__init, A) },
{ VarListIn = VarListIn0 },
{ VarListOut = VarListOut0 },
{ ( search_one_node(A, InitLabel, InitNode0) ->
InitNode = InitNode0
;
error("Init label not found")
)
},
{ ( map(search_one_node(A), FinalLabelList, FinalNodeList0) ->
FinalNodeList = FinalNodeList0
;
error("Final labels not found")
)
}
;
{ error(FileName ++ " has not the rigth format.\n") }
% XXX display the grammar rules specifying the .aut format here
)
;
print("*** Can't open file"), print(FileName), nl, nl,
{ error("") }
).
% search_node is nondet and by construction, there is exactly one solution
:- pred search_one_node(graph(N, A), N, node(N)).
:- mode search_one_node(in, in, out) is semidet.
search_one_node(G, NodeInfo, Node) :-
solutions(search_node(G, NodeInfo), [Node|_]).
:- pred add_an_arc(edge, automata, automata).
:- mode add_an_arc(in, in, out) is det.
add_an_arc(edge(SourceNodeL, FormulaL, TargetNodeL), Aut0, Aut) :-
solutions(graph__search_node(Aut0, SourceNodeL), Sol),
( Sol = [SourceNode0|_] ->
SourceNode = SourceNode0,
Aut1 = Aut0
;
graph__det_insert_node(Aut0, SourceNodeL, SourceNode, Aut1)
),
solutions(graph__search_node(Aut1, TargetNodeL), Sol2),
( Sol2 = [TargetNode0|_] ->
TargetNode = TargetNode0,
Aut2 = Aut1
;
graph__det_insert_node(Aut1, TargetNodeL, TargetNode, Aut2)
),
graph__det_insert_edge(Aut2, SourceNode, TargetNode, FormulaL, _Formula, Aut).
%-----------------------------------------------------------------------%
% XXX This is very inefficient (and a little bit obfuscated) because
% the graph library was not designed to access easily the arc contents.
% Probably I should change of data structure if it is really a problem
% (by replacing arcs by nodes ??).
try(A, Node) = ArcContentList :-
graph__successors(A, Node, NodeSucSet),
set__to_sorted_list(NodeSucSet, NodeSucList),
std_util__solutions(nondet_map(get_arc_content(A, Node), NodeSucList),
ArcContentListList),
condense(ArcContentListList, ArcContentList).
% Solutions can not guess which mode of list__map to use, and using
% this nondet_map instead of list__map makes it happy.
:- pred nondet_map(pred(X, Y), list(X), list(Y)).
:- mode nondet_map(pred(in, out) is nondet, in, out) is nondet.
nondet_map(Closure, List0, List) :-
list__map(Closure, List0, List).
:- pred get_arc_content(automata, node, node, { arc(arc_content), arc_content }).
:- mode get_arc_content(in, in, in, out) is nondet.
get_arc_content(A, Source, Target, { Arc, Formula }) :-
graph__path(A, Source, Target, [Arc]),
graph__arc_contents(A, Arc, Source, Target, Formula).
%-----------------------------------------------------------------------%
step(A, Arc) = Node :-
graph__arc_contents(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(false, _, _) = false.
eval(eps, _, _) = eps.
eval(and(Fl0, Fr0), Mem, D) = F :-
Fl1 = eval(Fl0, Mem, D),
( if Fl1 = false then
F = false
else
Fr1 = eval(Fr0, Mem, D),
( if Fl1 = true then F = Fr1
else if Fr1 = false then F = false
else if Fr1 = true then F = Fl1
else F = and(Fl1, Fr1)
)
).
eval(or(Fl0, Fr0), Mem, D) = F :-
Fl1 = eval(Fl0, Mem, D),
( if Fl1 = true then
F = true
else
Fr1 = eval(Fr0, Mem, D),
( if Fl1 = false then F = Fr1
else if Fr1 = true then F = true
else if Fr1 = false then F = Fl1
else F = and(Fl1, Fr1)
)
).
eval(not(F0), Mem, D) = F :-
( if F0 = false then F = true
else if F0 = true then F = false
else F = not(eval(F0, Mem, D))
).
eval(pos(Polynome), Mem, D) = F :-
Polynome1 = eval_polynome(Polynome, Mem, D),
(
Polynome1 = { [], Expr }
->
( (eval_expr(Expr) < float(0)) -> F = true ; F = false )
;
F = pos(Polynome1)
).
% % XXX How can I avoid this duplicated code?
% eval(pos_eq(Polynome), Mem, D) = F :-
% Polynome1 = eval_polynome(Polynome, Mem, D),
% (
% Polynome1 = { [], Expr }
% ->
% ( (eval_expr(Expr) >= 0) -> F = true ; F = false )
% ;
% F = pos_eq(Polynome1)
% ).
eval(b(VarName), Mem, D) = Val :-
Val0 = memory__lookup(Mem, VarName, D),
(
Val0 = memory__u
->
Val = b(VarName)
;
Val0 = memory__b(Bool)
->
Val = bool_to_formula(Bool)
;
% 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 ")
).
:- func eval_polynome(polynome, memory, date) = polynome.
:- mode eval_polynome(in, memory_ui, in) = out is det.
eval_polynome({ [], Constant }, _, _) = { [], Constant }.
eval_polynome({ [Monome0 | Tail0], Constant0 }, Mem, D) = Pol :-
{ Tail1, Constant1 } = eval_polynome({ Tail0, Constant0 }, Mem, D),
Monome0 = { Coeff, var(VarName) },
Val = memory__lookup(Mem, VarName, D),
( Val = u ->
Pol = { [Monome0 | Tail1], Constant1 }
;
Constant2 = minus(Constant1, times(int(Coeff), memory_num_val_to_expr(Val))),
Constant = val(string__float_to_string(eval_expr(Constant2))),
Pol = { Tail1, Constant }
).
:- func bool_to_formula(bool) = formula.
bool_to_formula(yes) = true.
bool_to_formula(no) = false.
%-----------------------------------------------------------------------%
% XXX Cette fonction devra plutot etre importée pour être sur que les
% conversions et les calculs en général soient cohérents avec ceux
% fait dans le solveur.
:- func eval_expr(expr) = float.
eval_expr(plus(Expr1, Expr2)) = eval_expr(Expr1) + eval_expr(Expr2).
eval_expr(minus(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(val(String)) = Float :-
( string__to_float(String, Float0) ->
Float = Float0
;
error("Bad format; can't convert to float.")
).
eval_expr(int(Int)) = Float :-
int__to_float(Int, Float).
:- func memory_num_val_to_expr(memory__element) = expr.
memory_num_val_to_expr(Elt) = Expr :-
( Elt = memory__val(String) ->
Expr = val(String)
;
error("Numerical value expected.")
).
%-----------------------------------------------------------------------------%
% Copyright (C) 2001 - Verimag.
% This file may only be copied under the terms of the GNU Library General
% Public License
%-----------------------------------------------------------------------------%
% File: lurette.m
% Main author: jahier@imag.fr
% This module is the main engine of the lurette, a testing
% environement for real-time systems.
% Les pamamètres du test sont :
% - L : taille de la séquence
% - N : épaisseur du test
% - ??: nombre de séquence (c'est quoi ca ?)
% - L'environnement
% - L'oracle
% - le SUT
% Initialisation
% - ...
% Faire L fois :
% - Founir à AutoEnv ses entrées (???) et récupérer un ensemble
% de formules pondérées F = {p1-f1, ..., pk-fk} (2)
% - Faire N fois :
% - Choisir une formule f dans F (en tenant compte de leur poids)
% - Récupérer une valuation in_i satisfiant f à l'aide du
% solveur (4)
% On a ainsi un ensemble de N valuations I = {in_1, ..., in_N}.
% - Récuperer les N résultats correspondants aux in_i en faisant des
% <<try>> dans le SUT (6). On obtient les N résultats
% out_1, ..., out_N.
% - Vérifier la validité des N couples (in_i, out_i) avec l'oracle (5)
% - Choisir une valeur in dans I
% - Faire faire un pas au SUT avec in (<<step>>).
% - Faire faire un pas à l'oracle avec in.
% - Faire faire un pas à l'automate (2) correspondant à la formule
% de laquelle le `in' choisi est issu.
% Dans un premier temps, une épaisseur de N=1 est ok.
:- module lurette.
%-----------------------------------------------------------------------%
:- interface.
:- import_module int, io.
:- type date == int.
:- pred main(io__state, io__state).
:- mode main(di, uo) is det.
%-----------------------------------------------------------------------%
:- implementation.
:- import_module bool, list, memory, env_automata.
main -->
print("lurette... "), nl,
read_automata("test1.aut", Automata, InitNode, FinalNodes, InVarList, OutVarList),
{ Mem = memory__init(InVarList ++ OutVarList, 10) },
loop(Mem, Automata, InitNode, FinalNodes, Mem2),
memory__dump(Mem2).
:- pred loop(memory, automata, node, list(node), memory, io__state, io__state).
:- mode loop(memory_di, in, in, in, memory_uo, di, uo) is det.
loop(Mem0, A, InitNode, FinalNodes, Mem) -->
print("*** Le Noeud courant est le noeud "),
print(InitNode), nl,
{ Mem1 = set(Mem0, "a", 1, b(yes)) },
{ Mem2 = set(Mem1, "i", 1, val("3")) },
{ Mem3 = set(Mem2, "f", 1, val("2")) },
{ Mem4 = set(Mem3, "fd", 1, val("4.6")) },
{ MemLast = set(Mem4, "b", 1, b(no)) },
( { member(InitNode, FinalNodes) } ->
print("The end ...\n"),
{ Mem = MemLast }
;
{ try(A, InitNode) = List },
(
{ List = [] },
print("Pas de transitions\n"),
memory__dump(MemLast),
{ Mem = MemLast }
;
{ List = [{ Arc, { _, ArcContent} } | _] },
print("*** on choisit l'arc "),
print(Arc),
print(" étiqueté par la formule "),
print(ArcContent),
print(" parmis les possibilitées "),
print(List), nl,
print("*** Une fois évaluée, la formule "), nl,
print(ArcContent),
print(" devient "), nl,
print(eval(ArcContent, MemLast, 1)),
nl,
{ NewNode = step(A, Arc) },
read_char(_),
loop(MemLast, A, NewNode, FinalNodes, Mem)
)
).
;; -*- Prcs -*-
(Created-By-Prcs-Version 1 3 3)
(Project-Description "")
(Project-Version lurette 0 1)
(Parent-Version -*- -*- -*-)
(Version-Log "")
(New-Version-Log "")
(Checkin-Time "Thu, 04 Oct 2001 12:51:25 +0100")
(Checkin-Login jahier)
(Populate-Ignore ())
(Project-Keywords)
(Files
;; This is a comment. Fill in files here.
;; For example: (prcs/checkout.cc ())
;; Files added by populate at Thu, 04 Oct 2001 12:47:52 +0100,
;; to version 0.0(w), by jahier:
(ID_EN_VRAC (lurette/0_ID_EN_VRAC 1.1 644))
(Mmakefile (lurette/1_Mmakefile 1.1 640))
(test1.aut (lurette/2_test1.aut 1.1 644))
(memory.m (lurette/3_memory.m 1.1 644))
(env_automata.m (lurette/4_env_automa 1.1 644))
(lurette.m (lurette/5_lurette.m 1.1 644))
)
(Merge-Parents)
(New-Merge-Parents)
%-----------------------------------------------------------------------------%
% Copyright (C) 2001 - Verimag.
% This file may only be copied under the terms of the GNU Library General
% Public License
%-----------------------------------------------------------------------------%
% File: memory.m
% Main author: jahier@imag.fr
% This module define the memory type, as well as its init, lookup,
% and set functions.
%-----------------------------------------------------------------------%
%-----------------------------------------------------------------------%
:- module memory.
:- interface.
:- import_module string, bool, int, list, array, map, io, std_util.
:- import_module lurette.
:- type memory__element --->
u % unknow value
; b(bool) % booleans
; val(string). % other types
% ; i(int) % integers
% ; r(rational). % rationals
% The memory is represented by a structure that contains:
% - The length L of the test
% - A dictionnary that indexes variables
% - An array that contains variable sequence of values
%
% The first L elements of the array contains the sequence value
% of the first variable in the index, and so on. For example, the
% `((4-1)*L) + 15-1'-th element of the array contains the value of
% the 4th variable at event 15. The size of the array is then of course
% l * the number of variables.