prism-accumulation/prism/src/jltl2dstar/Scheduler.java

/*
 * This file is part of a Java port of the program ltl2dstar
 * (http://www.ltl2dstar.de/) for PRISM (http://www.prismmodelchecker.org/)
 * Copyright (C) 2005-2007 Joachim Klein <j.klein@ltl2dstar.de>
 * Copyright (c) 2007 Carlos Bederian
 *
 * This program is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License version 2 as 
 *  published by the Free Software Foundation.
 *
 * This program 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 program; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */

package jltl2dstar;

/** @file
 * Implementation of LTL2DSTAR_Scheduler
 */
import java.util.Vector;
import java.io.PrintStream;

import jltl2ba.APSet;
import jltl2ba.SimpleLTL;
import prism.PrismException;

/**
 * Allows translation of LTL to DRA/DSA
 * in multiple ways and combines the basic building blocks to choose the most
 * efficient.
 */
public class Scheduler {

	/** The LTL2DRA wrapper for Safra's algorithm and the external LTL->NBA translator */
	private LTL2DRA _ltl2dra;

	/** Use limiting? */
	private boolean _opt_limits;

	/** The limiting factor */
	private double _alpha;

	/** Print stats on the NBA? */
	private boolean _stat_NBA;
	
	/** Base class for the building blocks for the scheduler */
	public abstract static class Tree {
		protected SimpleLTL _ltl;    
		protected Options_LTL2DRA _options;
		protected int priority;
		protected DRA _automaton;
		protected String _comment;
		protected Scheduler _sched;
		protected APSet _apset;

		protected Vector<Tree> children;

		/**
		 * Constructor 
		 * @param ltl The LTL formula
		 * @param options the LTL2DSTAR options
		 * @param sched a reference back to the scheduler 
		 */
		public Tree(SimpleLTL ltl, APSet apset, Options_LTL2DRA options, Scheduler sched) {
			_ltl = ltl;
			_apset = apset;
			_options = options;
			_sched = sched;
			children = new Vector<Tree>();
		}

		/** Print the tree on output stream (default level: 0) */
		public void printTree(PrintStream out, int level) {
			for (int i = 0; i < level; i++) {
				out.print(" ");
			}
			out.println(this.getClass().getName() + " = " + this + "(" + _ltl + ")");
			for (Tree child : children) {
				child.printTree(out, level + 1);
			}
		}

		/** Abstract virtual function for tree generation */
		public abstract void generateTree();

		/** Estimate the size of the automaton */
		public int guestimate() {
			return 0;
		}

		/** Hook that is called after calculate() finishes */
		public void hook_after_calculate() {};

		/** Calculate the automaton for this building block, by default
		 * calculate the automata for the children and then choose the smallest.
		 * (default level: 0, default limit: 0 */
		public void calculate(int level, int limit) throws PrismException {
			if (_options.verbose_scheduler) {
				System.err.println("Calculate (" + level + "): " + this.getClass().getName());
			}

			calculateChildren(level, limit);

			boolean first = true;
			for (Tree child : children) {
				if (child._automaton == null) {
					continue;
				}

				if (first) {
					_automaton = child._automaton;
					_comment = child._comment;
				} else {
					if (_automaton.size() > child._automaton.size()) {
						_automaton = child._automaton;
						_comment = child._comment;
					}
				}

				first = false;
			}

			hook_after_calculate();
		}

		/** Add a new child */
		public void addChild(Tree child) {
			if (child == null) {return;}

			children.add(child);
		}

		/** Calculate the automata for the children
		 *  (default level: 0, default limit: 0 */
		private void calculateChildren(int level, int limit) throws PrismException {
			if (_sched.flagOptLimits()) {
				DRA _min_automaton;
				int _min_size = 0;

				for (Tree child : children) {
					int child_limit;
					if (_min_size != 0) {
						if (limit > 0) {
							child_limit = _sched.calcLimit(_min_size) < limit ? _sched.calcLimit(_min_size) : limit;
						} else {
							child_limit = _sched.calcLimit(_min_size);
						}
					} else {
						child_limit = limit;
					}
					if (_options.verbose_scheduler) {
						System.err.println(" Limit (with alpha) = " + child_limit);
					}
					try {
						child.calculate(level + 1, child_limit);

						if (child._automaton != null) {
							if (_min_size == 0 || child._automaton.size() < _min_size) {
								_min_automaton = child._automaton;
								_min_size = _min_automaton.size();
							} else {
								// delete automaton as it is bigger
								// than necessary
								child._automaton = null;
							}
						}
					} catch (PrismException e) {
						child._automaton = null;
						throw e;
					}
				}
			} else {
				for (Tree child : children) {
					child.calculate(level + 1, limit);
				}
			}
		}
	}

	/** The root building block for the calculation of DRA/DSA */
	public static class Tree_Start extends Tree {
		/**
		 * Constructor 
		 * @param ltl The LTL formula
		 * @param options the LTL2DSTAR options
		 * @param sched a reference back to the scheduler 
		 */
		public Tree_Start(SimpleLTL ltl, APSet apset, Options_LTL2DRA options, Scheduler sched) {
			super(ltl, apset, options, sched);
			generateTree();
		}

		/** Generate the tree */
		public void generateTree() {
			Tree_Rabin rabin = null;
			Tree_Streett streett = null;

			if (_options.automata == Options_LTL2DRA.AutomataType.RABIN ||
					_options.automata == Options_LTL2DRA.AutomataType.RABIN_AND_STREETT) {
				rabin = new Tree_Rabin(_ltl, _apset, _options, _sched);
			}

			if (_options.automata == Options_LTL2DRA.AutomataType.STREETT ||
					_options.automata == Options_LTL2DRA.AutomataType.RABIN_AND_STREETT) {
				streett = new Tree_Streett(_ltl.negate().simplify(), _apset, _options, _sched);
			}

			if (rabin != null && streett != null) {
				int rabin_est = rabin.guestimate();
				int streett_est = streett.guestimate();

				if (_options.verbose_scheduler) {
					System.err.println("NBA-Estimates: Rabin: " + rabin_est + " Streett: " + streett_est);
				}

				if (rabin_est <= streett_est) {
					addChild(rabin);
					addChild(streett);
				} else {
					addChild(streett);
					addChild(rabin);
				}
			} else {
				if (rabin != null)
					addChild(rabin);
				if (streett != null) 
					addChild(streett);
			}


			/*			if (_options.opt_safra.stutter) {
				StutterSensitivenessInformation::ptr stutter_information(new StutterSensitivenessInformation);
				stutter_information->checkLTL(_ltl);

				if (!stutter_information->isCompletelyInsensitive() && _options.opt_safra.partial_stutter_check) {
					NBA_ptr nba, complement_nba;
					if (rabin) {
						nba=rabin->getNBA();
					} else if (streett) {
						nba=streett->getNBA();
					}

					if (rabin && streett) {
						complement_nba=streett->getNBA();
					}

					if (!nba) {
						stutter_information->checkPartial(*_ltl, _sched.getLTL2DRA());
					} else if (!complement_nba) {
						stutter_information->checkPartial(*nba, *_ltl->negate()->toPNF(), _sched.getLTL2DRA());
					} else {
						stutter_information->checkNBAs(*nba, *complement_nba);
					}
				}

				if (rabin) {
					rabin->setStutterInformation(stutter_information);
				}
				if (streett) {
					streett->setStutterInformation(stutter_information);
				}
			}
			 */
		}
	}

	/** A building block for the calculation of a Rabin automaton 
	 * (via Safra, Scheck or Union) */
	public static class Tree_Rabin extends Tree {

		private Tree_Safra _tree_normal;
		private Tree_Union _tree_union;

		// private StutterSensitivenessInformation::ptr _stutter_information;


		/**
		 * Constructor 
		 * @param ltl The LTL formula
		 * @param options the LTL2DSTAR options
		 * @param sched a reference back to the scheduler 
		 */
		public Tree_Rabin(SimpleLTL ltl, APSet apset, Options_LTL2DRA options, Scheduler sched) {
			super(ltl, apset, options, sched);
			_tree_normal = null;
			_tree_union = null;
			generateTree();
		}

		/** Estimate the size of the automaton (use the estimate of Safra's
		 * building block ) */
		public int guestimate() {
			if (_tree_normal != null) {
				return _tree_normal.guestimate();
			}
			return 0;
		}

		/** Hook after calculation */
		public void hook_after_calculate() {
			if (_tree_normal != null && _sched.flagStatNBA()) {
				_comment = _comment + "+NBAstd=" + guestimate();
			}
		}

		/** Generate the tree */
		public void generateTree() {
			/* if (_options.scheck_path!="") {
				if (LTL2DSTAR_Tree_Scheck::worksWith(*_ltl, _options.verbose_scheduler)) {
	  				addChild(new LTL2DSTAR_Tree_Scheck(_ltl, _options, _sched));
				}
				// add stuff for path. check here
      		}*/
			if (_options.allow_union &&	_ltl.kind == SimpleLTL.LTLType.OR) {
				_tree_union = new Tree_Union(_ltl, _apset, _options, _sched);
				addChild(_tree_union);
			}

			//	if (!((_options.only_union && _options.allow_union) || (_options.only_safety && _options.safety))) {
			if (!((_options.only_union && _options.allow_union))) {
				_tree_normal = new Tree_Safra(_ltl, _apset, _options, _sched);
				addChild(_tree_normal);
			}
		}

		public NBA getNBA() {
			if (_tree_normal != null) {
				return _tree_normal.getNBA();
			}
			return null;
		}

		/* public void setStutterInformation(StutterSensitivenessInformation::ptr stutter_information) {
			_stutter_information=stutter_information;
			if (_tree_normal) {
				_tree_normal->setStutterInformation(_stutter_information);
			}

			if (_tree_union) {
				_tree_union->setStutterInformation(_stutter_information);
			}
		}*/
	}


	/** Building block for the translation from LTL to DRA using Safra's algorithm */
	public static class Tree_Safra extends Tree {

		private NBA _nba;
		// private StutterSensitivenessInformation::ptr _stutter_information;

		/**
		 * Constructor 
		 * @param ltl The LTL formula
		 * @param options the LTL2DSTAR options
		 * @param sched a reference back to the scheduler 
		 */
		public Tree_Safra(SimpleLTL ltl, APSet apset, Options_LTL2DRA options, Scheduler sched) {
			super(ltl, apset, options, sched);
			generateTree();
		}

		/** Generate the tree */
		public void generateTree() {}

		/** Translate LTL -> NBA */
		public void generateNBA() {
			if (_nba == null) {
				try {
					_nba = _ltl.toNBA(_apset);
				}
				catch (PrismException e) {
					_nba = null;
					System.err.println("Scheduler.generateNBA() : " + e);
				}
			}
		}

		public NBA getNBA() {
			generateNBA();
			return _nba;
		}

		/** Estimate the size of the DRA (returns the size of the NBA) */
		public int guestimate() {
			generateNBA();
			if (_nba != null) {
				return _nba.size();
			}
			return 0;
		}

		/** Translate the LTL formula to DRA using Safra's algorithm */
		public void calculate(int level, int limit) throws PrismException {
			if (_options.verbose_scheduler) {
				System.err.println("Calculate (" + level + "): " + this.getClass().getName());
				System.err.println(" Limit = " + limit);
			}

			generateNBA();

			if (_nba == null) {
				throw new PrismException("Couldn't create NBA from LTL formula");
			}
			
			// _automaton = _sched.getLTL2DRA().nba2dra(_nba, limit, _options.detailed_states,	_stutter_information);
			_automaton = _sched.getLTL2DRA().nba2dra(_nba, limit, _options.detailed_states);
			_comment = "Safra[NBA=" + _nba.size() +	"]";

			if (_options.optimizeAcceptance) {
				_automaton.optimizeAcceptanceCondition();
			}

			if (_options.bisim) {
				DRAOptimizations dra_optimizer = new DRAOptimizations();
				_automaton = dra_optimizer.optimizeBisimulation(_automaton,	false, _options.detailed_states, false);
			}
		}

		/*public void setStutterInformation(StutterSensitivenessInformation::ptr stutter_information) {
			_stutter_information=stutter_information;
		}
		 */
	}


	/** Generate DRA by using the union construction on two DRAs */
	public static class Tree_Union extends Tree {

		/**
		 * Constructor 
		 * @param ltl The LTL formula
		 * @param options the LTL2DSTAR options
		 * @param sched a reference back to the scheduler 
		 */

		public Tree_Union(SimpleLTL ltl, APSet apset, Options_LTL2DRA options, Scheduler sched) {

			super(ltl, apset, options, sched);
			_left_tree = null;
			_right_tree = null;

			_left = _ltl.left;
			_right = _ltl.right;

			generateTree();
		}

		/**
		 * Generate the tree
		 */
		public void generateTree() {
			Options_LTL2DRA rec_opt = _options.clone();
			rec_opt.recursion();
			_left_tree = new Tree_Rabin(_left, _apset, rec_opt, _sched);
			addChild(_left_tree);
			_right_tree = new Tree_Rabin(_right, _apset, rec_opt, _sched);
			addChild(_right_tree);
		}

		/**
		 * Perform union construction
		 */
		public void calculate(int level, int limit) throws PrismException {
			if (_options.verbose_scheduler) {
				System.err.println("Calculate (" + level + "): " + this.getClass().getName());
			}

			try {
				children.get(0).calculate(level + 1, limit);
				children.get(1).calculate(level + 1, limit);
			} catch (PrismException e) {
				_automaton = null;
				throw e;
			}      

			if (children.get(0)._automaton == null || children.get(1)._automaton == null) {
				return;
			}

			boolean union_trueloop = _sched.getLTL2DRA().getOptions().union_trueloop;
			/* if (_sched.getLTL2DRA().getOptions().stutter) {
				_automaton=DRA_t::calculateUnionStuttered(*children[0]->_automaton,
			 *children[1]->_automaton,
						_stutter_information,
						union_trueloop,
						_options.detailed_states);
			} else {
			*/			
			_automaton = children.get(0)._automaton.calculateUnion(children.get(1)._automaton,	union_trueloop,	_options.detailed_states);
			/*      _automaton=DRAOperations::dra_union(*children[0]->_automaton, 
			 *children[1]->_automaton,
					  union_trueloop,
					  _options.detailed_states); */
			// }
			_comment = "Union{" + children.get(0)._comment + "," +	children.get(1)._comment + "}";

			if (_options.optimizeAcceptance) {
				_automaton.optimizeAcceptanceCondition();
			}

			if (_options.bisim) {
				DRAOptimizations dra_optimizer = new DRAOptimizations();
				_automaton = dra_optimizer.optimizeBisimulation(_automaton,	false, _options.detailed_states, false);
			}
			hook_after_calculate();
		}


		/* public void setStutterInformation(StutterSensitivenessInformation::ptr stutter_information) {
			_stutter_information=stutter_information;

			StutterSensitivenessInformation::ptr 
			left_stutter_info(new StutterSensitivenessInformation(*stutter_information));
			StutterSensitivenessInformation::ptr 
			right_stutter_info(new StutterSensitivenessInformation(*stutter_information));

			if (!stutter_information->isCompletelyInsensitive()) {
				left_stutter_info->checkLTL(_left);
				right_stutter_info->checkLTL(_right);
			}

			if (!left_stutter_info->isCompletelyInsensitive()) {
				left_stutter_info->checkPartial(*_left_tree->getNBA(), 
		 *_left->negate()->toPNF(), 
						_sched.getLTL2DRA());
			}

			if (!right_stutter_info->isCompletelyInsensitive()) {
				right_stutter_info->checkPartial(*_right_tree->getNBA(), 
		 *_right->negate()->toPNF(), 
						_sched.getLTL2DRA());
			}

			_left_tree->setStutterInformation(left_stutter_info);
			_right_tree->setStutterInformation(right_stutter_info); 
		}
		 */

		private Tree_Rabin _left_tree;
		private Tree_Rabin _right_tree;

		private SimpleLTL _left;
		private SimpleLTL _right;

		// private StutterSensitivenessInformation::ptr _stutter_information;
	}


	/**
	 * Generate Streett automaton by calculating the Rabin automaton
	 * for the negated formula
	 */  
	public static class Tree_Streett extends Tree {

		private Tree_Rabin _tree_rabin;
		// private StutterSensitivenessInformation::ptr _stutter_information;

		/**
		 * Constructor 
		 * @param ltl The LTL formula
		 * @param options the LTL2DSTAR options
		 * @param sched a reference back to the scheduler 
		 */

		public Tree_Streett(SimpleLTL ltl, APSet apset, Options_LTL2DRA options, Scheduler sched) {
			super(ltl, apset, options, sched);
			generateTree();
		}

		/** Estimate automaton size (use estimate of Rabin building block) */
		public int guestimate() {
			if (children.get(0) != null) {
				return children.get(0).guestimate();
			}
			return 0;
		}

		public NBA getNBA() {
			if (_tree_rabin != null) {
				return _tree_rabin.getNBA();
			}
			return null;
		}

		/** Generate tree */
		public void generateTree() {
			Options_LTL2DRA opt = _options;
			opt.automata = Options_LTL2DRA.AutomataType.RABIN;
			// opt.scheck_path=""; // disable scheck
			_tree_rabin = new Tree_Rabin(_ltl, _apset, opt, _sched);
			addChild(_tree_rabin);
		}    

		/** Calculate */
		public void calculate(int level, int limit) throws PrismException {
			if (_options.verbose_scheduler) {
				System.err.println("Calculate (" + level + "): " + this.getClass().getName());
			}

			try {
				children.get(0).calculate(level, limit);
			} catch (PrismException e) {
				_automaton = null;
				throw e;
			}

			_automaton = children.get(0)._automaton;
			_comment = "Streett{" +	children.get(0)._comment + "}";

			if (_automaton != null) {
				_automaton.considerAsStreett(true);
			}

			hook_after_calculate();
		}

		/* void setStutterInformation(StutterSensitivenessInformation::ptr stutter_information) {
			_stutter_information=stutter_information;
			_tree_rabin->setStutterInformation(stutter_information);
		}*/

	}

	/** Constructor
	 * @param ltl2dra the wrapper for LTL->NBA and NBA->DRA 
	 * @param opt_limits use limiting?
	 * @param alpha the limiting factor 
	 */
	public Scheduler(LTL2DRA ltl2dra, boolean opt_limits, double alpha) {
		_ltl2dra = ltl2dra;
		_opt_limits = opt_limits;
		_alpha = alpha;
		_stat_NBA = false;
	}



	/** Calculate the new limit using factor alpha (returns 0 if no limit) */
	public int calcLimit(int limit) {
		if (limit == 0) {return limit;}
		if (flagOptLimits()) {
			double new_limit = (limit * _alpha) + 1.0;
			if (new_limit > Integer.MAX_VALUE) {
				limit = 0;
			} else {
				limit = (int)new_limit;
			}
		}
		return limit;
	}

	/** 
	 * Generate a DRA/DSA for the LTL formula 
	 */
	public DRA calculate(SimpleLTL ltl, APSet apset, Options_LTL2DRA ltl_opt) throws PrismException {

		if (ltl_opt.verbose_scheduler) {
			System.err.println(ltl);
		}

		Tree root = new Tree_Start(ltl, apset, ltl_opt, this);

		if (ltl_opt.verbose_scheduler) {
			root.printTree(System.err, 0);
		}

		root.calculate(0,0);

		DRA result = root._automaton;
		if (result != null) {
			result.setComment(root._comment + getTimingInformation());
		}
		return result;
	}

	public String getTimingInformation() {
		/* if (StutterSensitivenessInformation::hasTimekeeping()) {
			unsigned long ms=StutterSensitivenessInformation::getTimeKeeper().getElapsedMilliseconds();
			return " TIME(stuttercheck)=:"+ 
			boost::lexical_cast<std::string>(ms)+
			":";
		} else {
		 */
		return "";
		// }
	}

	/** Get the LTL2DRA wrapper class */
	public LTL2DRA getLTL2DRA() {
		return _ltl2dra;
	}

	public boolean flagOptLimits() {return _opt_limits;}

	/** Get the state of the StatNBA flag */
	public boolean flagStatNBA() {return _stat_NBA;}

	/** Set the value of the StatNBA flag */
	public void flagStatNBA(boolean value) {_stat_NBA=value;}
	
}