added first version of long run rewards

Author: buschko

Makefile

@@ -105,7 +105,7 @@ SRCDIR		=	src
 BINDIR		=	bin
 LIBDIR		=	lib
 INCLUDEDIR	=	include
-LIBOBJ		=	read_file.o read_file_imc.o  sparse.o unbounded.o expected_time.o expected_reward.o bounded_reward.o sccs.o sccs2.o long_run_average.o debug.o bounded.o
+LIBOBJ		=	read_file.o read_file_imc.o  sparse.o unbounded.o expected_time.o expected_reward.o bounded_reward.o sccs.o sccs2.o long_run_average.o debug.o bounded.o long_run_reward.o
 BINOBJ		=	main.o
 
 NAME		=	imca

imca/imca.xcodeproj/project.pbxproj

@@ -38,6 +38,8 @@
 		B96D6AE61664FDFB00B9A9BE /* LICENSE */ = {isa = PBXFileReference; fileEncoding = 4; lastKnownFileType = text; name = LICENSE; path = ../LICENSE; sourceTree = "<group>"; };
 		B98752501704446800F35D50 /* sccs2.h */ = {isa = PBXFileReference; fileEncoding = 4; lastKnownFileType = sourcecode.c.h; path = sccs2.h; sourceTree = "<group>"; };
 		B9B5298916CBA3E100E6A0DD /* sccs2.cpp */ = {isa = PBXFileReference; fileEncoding = 4; lastKnownFileType = sourcecode.cpp.cpp; path = sccs2.cpp; sourceTree = "<group>"; };
+		B9CFFDFD1861DD1100A58492 /* long_run_reward.cpp */ = {isa = PBXFileReference; fileEncoding = 4; lastKnownFileType = sourcecode.cpp.cpp; path = long_run_reward.cpp; sourceTree = "<group>"; };
+		B9CFFDFE1861DD1900A58492 /* long_run_reward.h */ = {isa = PBXFileReference; fileEncoding = 4; lastKnownFileType = sourcecode.c.h; path = long_run_reward.h; sourceTree = "<group>"; };
 /* End PBXFileReference section */
 
 /* Begin PBXGroup section */
@@ -55,6 +57,7 @@
 		B96D6ACC1664FDDC00B9A9BE /* src */ = {
 			isa = PBXGroup;
 			children = (
+				B9CFFDFD1861DD1100A58492 /* long_run_reward.cpp */,
 				B9B5298916CBA3E100E6A0DD /* sccs2.cpp */,
 				B96D6ACD1664FDDC00B9A9BE /* .kdev_include_paths */,
 				B96D6ACE1664FDDC00B9A9BE /* bcg2imca.c */,
@@ -78,6 +81,7 @@
 		B96D6AD91664FDE200B9A9BE /* include */ = {
 			isa = PBXGroup;
 			children = (
+				B9CFFDFE1861DD1900A58492 /* long_run_reward.h */,
 				B98752501704446800F35D50 /* sccs2.h */,
 				B96D6ADA1664FDE200B9A9BE /* bcg2imca.h */,
 				B96D6ADB1664FDE200B9A9BE /* bounded.h */,
@@ -118,7 +122,7 @@
 		B96D6AC11664FCFB00B9A9BE /* Project object */ = {
 			isa = PBXProject;
 			attributes = {
-				LastUpgradeCheck = 0460;
+				LastUpgradeCheck = 0500;
 				ORGANIZATIONNAME = "Dennis Guck";
 			};
 			buildConfigurationList = B96D6AC41664FCFB00B9A9BE /* Build configuration list for PBXProject "imca" */;
@@ -161,7 +165,7 @@
 				GCC_WARN_ABOUT_RETURN_TYPE = YES;
 				GCC_WARN_UNINITIALIZED_AUTOS = YES;
 				GCC_WARN_UNUSED_VARIABLE = YES;
-				MACOSX_DEPLOYMENT_TARGET = 10.8;
+				MACOSX_DEPLOYMENT_TARGET = 10.9;
 				ONLY_ACTIVE_ARCH = YES;
 				SDKROOT = macosx;
 			};
@@ -184,7 +188,7 @@
 				GCC_WARN_ABOUT_RETURN_TYPE = YES;
 				GCC_WARN_UNINITIALIZED_AUTOS = YES;
 				GCC_WARN_UNUSED_VARIABLE = YES;
-				MACOSX_DEPLOYMENT_TARGET = 10.8;
+				MACOSX_DEPLOYMENT_TARGET = 10.9;
 				SDKROOT = macosx;
 			};
 			name = Release;

include/long_run_average.h

@@ -20,7 +20,7 @@
 * 
 * 
 * @file long_run_average.cpp
-* @brief Compute the expected time for an MA
+* @brief Compute the long-run average for an MA
 * @author Dennis Guck
 * @version 1.0
 *
@@ -43,7 +43,7 @@ using namespace soplex;
 *
 * @param ma file to read MA from
 * @param max identifier for min or max
-* @return expected time 
+* @return long-run average
 */
 extern Real compute_long_run_average(SparseMatrix*, bool);
 

include/long_run_reward.h

@@ -0,0 +1,51 @@
+/**
+* IMCA is a analyzing tool for unbounded reachability probabilities, expected-
+* time, and long-run averages for Interactive Markov Chains and Markov Automata.
+* Copyright (C) RWTH Aachen, 2012
+*				UTwente, 2013
+* 	Author: Dennis Guck
+*
+* This program 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 3 of the License, or
+* (at your option) any later version.
+*
+* 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, see <http://www.gnu.org/licenses/>.
+* 
+* 
+* @file long_run_reward.cpp
+* @brief Compute the long-run reward for an MA
+* @author Dennis Guck
+* @version 1.0
+*
+*/
+
+#ifndef LONG_RUN_REWARD_H
+#define LONG_RUN_REWARD_H
+
+
+#include "sparse.h"
+
+#ifdef __SOPLEX__
+#include "soplex.h"
+#endif
+
+using namespace soplex;
+
+/**
+* Computes long-run reward for MA.
+*
+* @param ma file to read MA from
+* @param max identifier for min or max
+* @return long-run reward
+*/
+extern Real compute_long_run_reward(SparseMatrix*, bool);
+
+
+#endif

src/bounded.cpp

@@ -435,6 +435,7 @@ Real compute_time_bounded_reachability(SparseMatrix* ma, bool max, Real epsilon,
 		// value iteration
 		cout << "iterations: " << (unsigned long) ceil((tb - ta) / tau) + (unsigned long) ceil(ta / tau) << endl;
 		printf("step duration for interval [%g,%g]: %g\n", ta, tb, current_tau);
+		cout << "iterations: " << (unsigned long) ceil((tb - ta) / tau) << endl;
 
 		for(unsigned long i=0; i < steps; i++){
 			// compute v for Markovian states: from b dwon to a, we make discrete model absorbing
@@ -482,7 +483,7 @@ Real compute_time_bounded_reachability(SparseMatrix* ma, bool max, Real epsilon,
 		SparseMatrix_free(discrete_ma);
 
 		steps = (unsigned long) ceil( (ta + current_tau) / tau); // calculating the number of steps for interval [0,a]
-		current_tau = (ta + current_tau) / steps;                                // recalculate tau based on the number of steps
+		current_tau = (ta + current_tau) / steps;                // recalculate tau based on the number of steps
 
 		// discretize model with respect to the current value of tau 'current_tau'
 		dbg_printf("discretize model for interval [0,%g] ... \n", ta);
@@ -491,8 +492,9 @@ Real compute_time_bounded_reachability(SparseMatrix* ma, bool max, Real epsilon,
 		//print_model(discrete_ma);
 
 		printf("step duration for interval [0,%g]: %g\n", ta, current_tau);
+		cout << "iterations: " << (unsigned long) ceil( (ta + current_tau) / tau) << endl;
 
-		for(unsigned long i=0; i < steps; i++){
+		for(unsigned long i=0; i < steps; ++i){
 			// compute v for Markovian states: shift up to a, we don't make discrete model absorbing
 			compute_markovian_vector(discrete_ma,v,u, false);
 			// compute u for Probabilistic states
@@ -615,8 +617,10 @@ Real compute_time_bounded_reachability(SparseMatrix* ma, bool max, Real epsilon,
 	else
 		prob=1;
 	bool *initials = ma->initials;
+	printf("vector(%d) [",num_states);
 	for (unsigned long state_nr = 0; state_nr < num_states; state_nr++) {
 		//cout << (ma->states_nr.find(state_nr)->second).c_str() << ": " << u[state_nr] << endl;
+		printf(" %lf,",u[state_nr]);
 		if(initials[state_nr]){
 			if(max){
 				if(prob<u[state_nr])
@@ -627,6 +631,7 @@ Real compute_time_bounded_reachability(SparseMatrix* ma, bool max, Real epsilon,
 			}
 		}
 	}
+	printf(" ]\n");
 
 
 	return prob;