da_item.cc

由matlab开发的hybrid系统的描述语言

/*
	HYSDEL
	Copyright (C) 1999-2002  Fabio D. Torrisi

	This file is part of HYSDEL.
    
	HYSDEL is free software; you can redistribute it and/or
	modify it under the terms of the GNU General Public
	License as published by the Free Software Foundation; either
	version 2 of the License, or (at your option) any later version.

	HYSDEL is distributed in the hope that it will be useful,
	but WITHOUT ANY WARRANTY; without even the implied warranty of
	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
	General Public License for more details.

	You should have received a copy of the GNU General Public
	License along with this library; if not, write to the Free Software
	Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA

	CONTACT INFORMATION
	===================
	Fabio D. Torrisi
	ETH Zentrum
	Physikstrasse. 3 ETL,
	CH-8032 Zurich
	Switzerland
	mailto:[e-mail] (preferred)
*/

#include "DA_item.h"

#include "MLD_representation.h"
#include "Expr.h"
#include "Symbol_table.h"
#include "Variable_expr.h"
#include "Equivalence_expr.h"
#include "Var_symbol.h"
#include "Number_expr.h"
#include "Min_max_eps.h"
#include "Minus_expr.h"
#include "Neg_expr.h"
#include "Logic_item.h"
#include "Linear_item.h"
#include "Plus_expr.h"
#include "Mult_expr.h"
#include "Cast_log2real_expr.h"
#include "Var_symbol.h"
#include "Not_expr.h"
#include "Min_max_eps.h"
#include "Affine_func.h"
#include "Min_expr.h"
#include "Max_expr.h"
#include <stdio.h>
#include "Globals.h"
#include "Problem.h"
#include "Problem_handler.h"


DA_item::DA_item(const Var_symbol * lhs, Expr * logic_expr, Expr * aff_then,
	Min_max_eps * mme_then, Expr * aff_else, Min_max_eps * mme_else,
	const Globals * glob) : Definition_item(lhs, glob) {
		logic = logic_expr;
		affine_then = aff_then;
		this->mme_then = mme_then;
		construct_else(aff_else, mme_else);
		cond_var = NULL;
		then_min_computed=false;
		then_max_computed=false;
		else_min_computed=false;
		else_max_computed=false;
}

list < const Var_symbol * > DA_item::get_required_mme() const {
	list < const Var_symbol * > req;

	add_required(req, affine_then);
	add_required(req, affine_else);
	return req;
}

list < const Var_symbol * > DA_item::get_required_simu() const {
	list < const Var_symbol * > req;

	req = get_required_mme();
	if (cond_var && cond_var->is_var_symbol())
		req.push_back((const Var_symbol *) cond_var); else
		add_required(req, logic);
	return req;
}

DA_item::~DA_item() {
	delete affine_then;
	delete affine_else;
	delete mme_then;
	delete mme_else;
	this->Definition_item::~Definition_item();
}

void DA_item::construct_else(Expr * aff, Min_max_eps * mme) {
	if (aff == NULL) {
		affine_else = new Number_expr(0.0, globals);
		mme_else = new Min_max_eps(new Number_expr(0.0, globals),
			new Number_expr(0.0, globals),
			new Number_expr(0.0, globals), globals);
	} else {
		affine_else = aff;
		mme_else = mme;
	}
}


list < Item * > DA_item::unroll() {
	Logic_item * li;
	list < Item * > res, tmplst;
	list < Item * >::iterator iter;

	res = affine_then->unroll();
	tmplst = affine_else->unroll();
	res.insert(res.end(), tmplst.begin(), tmplst.end());
	if (logic->is_variable_expr()) {
		cond_var = ((Variable_expr *) logic)->get_value();
	} else {
		if (logic->is_not_expr() &&
			((Not_expr *) logic)->get_child()->is_variable_expr()) { //
				// logic is !VAR  -> exchange then<->else
				Min_max_eps * tmpmme;
				Expr * tmp = ((Not_expr *) logic)->get_child();
				cond_var = ((Variable_expr *)
					tmp)->get_value();
				delete tmp;
				tmp = affine_then;
				affine_then = affine_else;
				affine_else = tmp;
				tmpmme = mme_then;
				mme_then = mme_else;
				mme_else = tmpmme;
		} else {
			cond_var = globals->symbol_table->create_additional(AUX_KIND, BOOL_TYPE);
			li = new Logic_item((Var_symbol *) cond_var,
				logic, globals);
			res.push_back(li);
		}
	}
	if (affine_then->is_const() && affine_else->is_const()) {
		// Case z = if delta then const1 else const2 
		// translates to z = const2 -(const2 - const1) * delta

		Expr * tmp1, * tmp2, * aff;
		Expr * cond_var_expr;
		Linear_item * li1;
		cond_var_expr = new Cast_log2real_expr(
			new Variable_expr((Var_symbol *) cond_var, globals));		
		tmp1 = new Minus_expr(affine_else->clone(), 
			affine_then->clone());
		tmp2 = new Mult_expr(tmp1, cond_var_expr);	
		aff = new Minus_expr(affine_else->clone(), tmp2);
		li1 = new Linear_item(lhs_var, aff, globals);
		li1->set_source_line(source_line);
		li1->set_source(source);
		res.push_back(li1);	
		this->translate_MLD_enabled = 0;
	}
	for (iter = res.begin(); iter != res.end(); iter++)
		(* iter)->set_unrolled_from(this);
		
	return res;
}

MLD_representation * DA_item::translate_MLD() const {
	MLD_representation * mld;
	Expr * tmp1, * tmp2, * tmp3, * tmp4, * ineq_expr;
	Expr * cond_var_expr, * lhs_var_expr;
	Affine_func * aff;
	int subind_cnt = 0;

	assert(cond_var && mme_then && mme_else); //fine

	mld = new MLD_representation(globals);

	if (!translate_MLD_enabled) {
		return mld;
	} // else

	cond_var_expr = new Cast_log2real_expr(
		new Variable_expr((Var_symbol *) cond_var, globals));
	lhs_var_expr = new Variable_expr(lhs_var, globals);
	
	// (mme_else->min - mme_then->max)*(1-cond_var) - lhs_var +affine_then <= 0
	tmp1 = new Minus_expr(mme_else->get_min(), mme_then->get_max());
	tmp2 = new Minus_expr(
		new Number_expr(1.0, globals), cond_var_expr->clone());
	tmp3 = new Mult_expr(tmp1, tmp2);
	tmp4 = new Minus_expr(tmp3, lhs_var_expr->clone());
	ineq_expr = new Plus_expr(tmp4, affine_then->clone());
	aff = ineq_expr->compute_affine();
	aff_leq_zero_to_mld(aff, mld, & subind_cnt);
	delete aff;
	
	// (mme_then->min - mme_else->max)*(1-cond_var) + lhs_var -affine_then <= 0
	tmp1 = new Minus_expr(mme_then->get_min(), mme_else->get_max());
	tmp2 = new Minus_expr(
		new Number_expr(1.0, globals), cond_var_expr->clone());
	tmp3 = new Mult_expr(tmp1, tmp2);
	tmp4 = new Plus_expr(tmp3, lhs_var_expr->clone());
	ineq_expr = new Minus_expr(tmp4, affine_then->clone());
	aff = ineq_expr->compute_affine();
	aff_leq_zero_to_mld(aff, mld, & subind_cnt);
	delete aff;

	// (mme_then->min - mme_else->max)*cond_var - lhs_var + affine_else <= 0
	tmp1 = new Minus_expr(mme_then->get_min(), mme_else->get_max());
	tmp2 = new Mult_expr(tmp1, cond_var_expr->clone());
	tmp3 = new Minus_expr(tmp2, lhs_var_expr->clone());
	ineq_expr = new Plus_expr(tmp3, affine_else->clone());
	aff = ineq_expr->compute_affine();
	aff_leq_zero_to_mld(aff, mld, & subind_cnt);
	delete aff;

	// (mme_else->min - mme_then->max)*cond_var + lhs_var - affine_else <= 0
	tmp1 = new Minus_expr(mme_else->get_min(), mme_then->get_max());
	tmp2 = new Mult_expr(tmp1, cond_var_expr->clone());
	tmp3 = new Plus_expr(tmp2, lhs_var_expr->clone());
	ineq_expr = new Minus_expr(tmp3, affine_else->clone());
	aff = ineq_expr->compute_affine();
	aff_leq_zero_to_mld(aff, mld, & subind_cnt);
	delete aff;

	delete lhs_var_expr;
	delete cond_var_expr;

	return mld;
}

void DA_item::compute_minmaxeps() {
	Affine_func * aff;
	Min_max_eps * auto_mme;

	aff = affine_then->compute_affine();	
	try {
		auto_mme = compute_mme_from_aff(aff);
	} catch (Problem * p) {
		if (!mme_then) globals->problem_handler->process(p); else
			auto_mme = NULL;
	}
	if (mme_then && auto_mme) check_mme_tight(mme_then, auto_mme);
	if (!mme_then) {
	  mme_then = auto_mme;
	  then_min_computed=true;
	  then_max_computed=true;
	}
	if (auto_mme && mme_then != auto_mme) delete auto_mme;
	delete aff;

	aff = affine_else->compute_affine();
	try {
		auto_mme = compute_mme_from_aff(aff);
	} catch (Problem * p) {
		if (!mme_else) globals->problem_handler->process(p); else
			auto_mme = NULL;
	}
	if (mme_else && auto_mme) check_mme_tight(mme_else, auto_mme);
	if (!mme_else) {
	  mme_else = auto_mme;
	  else_min_computed=true;
	  else_max_computed=true;
	}
	if (auto_mme && mme_else != auto_mme) delete auto_mme;
	delete aff;
}

Min_max_eps * DA_item::compute_minmax() const {
	Expr * min, * max;
	Min_max_eps * mme_tmp;
	Expr * then_min, * then_max, * else_min, * else_max;
	Affine_func * aff;

	if (!mme_then) {
		aff = affine_then->compute_affine();
		mme_tmp = compute_mme_from_aff(aff);
		delete aff;
		then_min = mme_tmp->get_min();
		then_max = mme_tmp->get_max();
		delete mme_tmp;
	} else {
		then_min = mme_then->get_min()->clone();
		then_max = mme_then->get_max()->clone();
	}
	if (!mme_else) {
		aff = affine_else->compute_affine();
		mme_tmp = compute_mme_from_aff(aff);
		delete aff;
		else_min = mme_tmp->get_min();
		else_max = mme_tmp->get_max();
		delete mme_tmp;
	} else {
		else_min = mme_else->get_min()->clone();
		else_max = mme_else->get_max()->clone();
	}

	min = Expr::simpl(new Min_expr(then_min, else_min));
	max = Expr::simpl(new Max_expr(then_max, else_max));
	return new Min_max_eps(min, max, NULL, globals);
}

void DA_item::semantic_checks() {
	string msg;
	char buf[20];

	if (lhs_var->get_kind() != AUX_KIND) {
		sprintf(buf, "line %d: ", get_source_line());
		msg = buf;
		msg += string("left hand side variable ") +
			lhs_var->get_name() + string(" is not auxiliary");
		msg += string(" (") + lhs_var->get_name() +
			string(" declared at line ");
		sprintf(buf, "%d)", lhs_var->get_line_of_decl());
		msg += string(buf);
		globals->problem_handler->process(new Problem(ERROR, msg));
	}
	if (lhs_var->get_type() != REAL_TYPE) {
		sprintf(buf, "line %d: ", get_source_line());
		msg = buf;
		msg += string("left hand side variable ") +
			lhs_var->get_name() + string(" is not real");
		msg += string(" {") + lhs_var->get_name() +
			string(" declared at line ");
		sprintf(buf, "%d)", lhs_var->get_line_of_decl());
		msg += string(buf);
		globals->problem_handler->process(new Problem(ERROR, msg));
	}
	if (is_required_simu(lhs_var)) {
		sprintf(buf, "line %d: ", get_source_line());
		msg = buf;
		msg += string("recursive definition of variable ") +
			lhs_var->get_name();
		globals->problem_handler->process(new Problem(ERROR, msg));
	}

	logic->semantic_checks();
	assert(logic->is_logic()); //fine		

	affine_then->semantic_checks();
	if (!affine_then->is_affine()) {
		sprintf(buf, "line %d: ", get_source_line());
		msg = buf;
		msg += string("then-expression must be affine");
		globals->problem_handler->process(new Problem(ERROR, msg));
	}

	affine_else->semantic_checks();
	if (!affine_else->is_affine()) {
		sprintf(buf, "line %d: ", get_source_line());
		msg = buf;
		msg += string("else-expression must be affine");
		globals->problem_handler->process(new Problem(ERROR, msg));
	}

	if (mme_then) mme_then->semantic_checks();
	if (mme_else) mme_else->semantic_checks();
}

string DA_item::arg_range_check_matlab() const {
	string res;

	res += logic->arg_range_check_matlab();
	res += affine_then->arg_range_check_matlab();
	res += affine_else->arg_range_check_matlab();
	if (mme_then) res += mme_then->arg_range_check_matlab();
	if (mme_else) res += mme_else->arg_range_check_matlab();
	return res;
}

string DA_item::matlab_simu() const {
	string res;
	
	/* Note that the generation of the MLD matrix may be inibited, while 
	   the generation of the simulator is left */
	
	res += string("% ") + get_source() + string("\n");

	res += string("if ") + cond_var->to_matlab() + string("\n");
	res += string("\twithin(") + affine_then->to_matlab() + string(", ") +
		mme_then->get_min()->to_matlab() + string(", ") +
		mme_then->get_max()->to_matlab() + 
	  string(", ") + get_source_line_str() +
	  string(");\n");
	res += string("\t") + lhs_var->to_matlab() + string(" = ") +
		affine_then->to_matlab() + string(";\n");
	res += string("else\n");
	res += string("\twithin(") + affine_else->to_matlab() + string(", ") +
		mme_else->get_min()->to_matlab() + string(", ") +
		mme_else->get_max()->to_matlab() + 
	  string(", ") + get_source_line_str() +
	  string(");\n");
	res += string("\t") + lhs_var->to_matlab() + string(" = ") +
		affine_else->to_matlab() + string(";\n");
	res += string("end\n");
	res += string("\n");

	return res;
}


bool DA_item::minmax_known() const {
	return (mme_then && mme_else);
}