env.m

%-----------------------------------------------------------------------%
% 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.")
	).