From 3a12bcbf2012824a91cf8e3ce1250ca5eb3547b8 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Fri, 12 Oct 2018 14:25:35 +0200 Subject: [PATCH] imported patch rewardcounter-MDPProductOperator.patch --- prism/src/explicit/MDPProductOperator.java | 55 ++++++++++++++++++++++ 1 file changed, 55 insertions(+) create mode 100644 prism/src/explicit/MDPProductOperator.java diff --git a/prism/src/explicit/MDPProductOperator.java b/prism/src/explicit/MDPProductOperator.java new file mode 100644 index 00000000..908d4a89 --- /dev/null +++ b/prism/src/explicit/MDPProductOperator.java @@ -0,0 +1,55 @@ +//============================================================================== +// +// Copyright (c) 2015- +// Authors: +// * Joachim Klein (TU Dresden) +// +//------------------------------------------------------------------------------ +// +// This file is part of PRISM. +// +// PRISM 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. +// +// PRISM 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 PRISM; if not, write to the Free Software Foundation, +// Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA +// +//============================================================================== + +package explicit; + +import prism.PrismException; + +/** Interface for a product operator for a MDP -> MDP product */ +public interface MDPProductOperator +{ + /** Get the product state when considering some initial state in the MDP */ + public ProductState getInitialState(Integer MDP_state) throws PrismException; + + /** + * Get the successor state for the ProductState when going to mdp_to_state in the MDP + * via choice_i + */ + public ProductState getSuccessor(ProductState from_state, int choice_i, Integer mdp_to_state) throws PrismException; + + /** + * Notifies the Operator that state is assigned index in the product. + * Guaranteed to be called exactly once during the product construction for every + * ProductState. + */ + public void notify(ProductState state, Integer index) throws PrismException; + + /** Notifies the Operator that the product construction is finished */ + public void finish() throws PrismException; + + /** Get the underlying MDP */ + public MDP getGraph(); +}