%-----------------------------------------------------------------------% % 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, 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). %-----------------------------------------------------------------------% try(A, Node) = ArcArcInfoPairList :- graph__arcs(A, ArcList), list__filter_map(select_arcs(A, Node), ArcList, ArcArcInfoPairList). :- pred select_arcs(automata::in, node::in, env__arc::in, { env__arc, arc_content }::out) is semidet. select_arcs(A, Node, Arc, ArcArcInfoPair) :- graph__arc_contents(A, Arc, Node, _, ArcInfo), ArcArcInfoPair = { Arc, ArcInfo }. %-----------------------------------------------------------------------% step(A, Arc) = Node :- graph__arc_contents(A, Arc, _, Node, _). %-----------------------------------------------------------------------% 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) ) ). % use `not' and `and' instead ? 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), ( if Polynome1 = { [], Expr } then ( (eval_expr(Expr) < float(0)) -> F = true ; F = false ) else 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) ; Val0 = memory__val(_String), % Should not occur, by construction % How could I make mmc statically check that? % error("Boolean expected; there is probably 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 This ougth to be done in an external (C?) module that is also used % by the constraint solver (for consistency). % :- 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 :- ( if string__to_float(String, Float0) then Float = Float0 else 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 :- ( if Elt = memory__val(String) then Expr = val(String) else error("Numerical value expected.") ).