__color__	__group__	ticket	summary	component	version	milestone	type	owner	status	created	_changetime	_description	_reporter
3	Active Tickets	23	Add SVN notifications	SVN Repository		MRMC future	defect	ngyuen	new	2008-06-27T14:27:08+0200	2008-09-18T22:12:37+0200	I know that it is possible to have notifications in case of changes in the SVN repository. It would be nice to configure SVN to sending them to the mrmc-stuff mailing list.	ivan.zapreev
3	Active Tickets	28	PRCTL, lumping: The E operator problem.	Core	1.2.2	MRMC future	defect	ivan.zapreev	new	2008-06-27T15:15:10+0200	2008-06-27T15:36:15+0200	"PRCTL, E operator gives different results with and without formula independent lumping, compare tests:

{{{
test/functional_tests/dtmrm/prctl/syntax/prctl_general_input_02
}}}
and
{{{
test/functional_tests/dtmrm/prctl/syntax/prctl_general_input_01
}}}"	ivan.zapreev
3	Active Tickets	32	The probabilities comparison in the Bisimulation engine.	Bisimulation Engine	1.3	MRMC future	enhancement	christinajansen	new	2008-06-27T15:39:37+0200	2010-11-20T13:37:15+0100	"Somewhere in probabilistic bisimulation we test that probability values are equal. At present this is done up to some error margin, smth like 1e-6. I believe that this parameter has to be available for the user to manage. At least it should be clearly visible that we do probability comparison up to certain error. Also this has to be states in the manual. I suggest:

1. make this parameter a manageable MRMC runtime option
2. Update the MRMC manual correspondingly.
"	ivan.zapreev
3	Active Tickets	33	Improve and unify the error/warning/info messages.	Core	1.3	MRMC future	enhancement	ivan.zapreev	new	2008-06-27T15:41:03+0200	2008-06-27T15:50:25+0200	"Should be done as a part of Architectural change of MRMC.
Make a clear distinctions between [WARNING], [ERROR], [INFO] message logging."	ivan.zapreev
3	Active Tickets	34	Add a possibility to dump the model-checking results	Core	1.3	MRMC future	enhancement	christinajansen	new	2008-06-27T15:41:55+0200	2008-06-27T15:46:32+0200	"Add a possibility to dump the model-checking results into a file from the MRMC command prompt. It should be useful in case we have ""set print off"" and after of checking results with
{{{
$RESULT[i] and $STATE[i]
}}}
we want to store the rest on the hard drive."	ivan.zapreev
3	Active Tickets	35	Improving $RESULT and $STATE commands	Core	1.3	MRMC future	enhancement	christinajansen	new	2008-06-27T15:43:51+0200	2008-06-27T15:46:53+0200	"In the command prompt of MRMC, add a possibility to get not just the $RESULT[i] but $RESULT[i..j, ..., k-p] etc. The same goes for $STATE{}.

This way users will be able to get resulting probabilities and etc for  some set of states, they have interest in."	ivan.zapreev
3	Active Tickets	36	Add simulation engine for PCTL.	Simulation Engine	1.3	MRMC future	enhancement	ivan.zapreev	new	2008-06-27T15:45:55+0200	2008-06-27T15:45:55+0200	In principle all algorithms developed for model-checking CSL properties apply for PCTL. We need to extend MRMC to be able to model check PCTL with the use of discrete event simulation.	ivan.zapreev
3	Active Tickets	39	Unify source-code comments	Source Code	1.3	MRMC future	enhancement	christinajansen	new	2008-06-27T16:35:56+0200	2008-06-27T16:35:56+0200	"Make method comments look alike, e.g.:
{{{
/**
* The method does this and that ...
* @param <name> this parameter is ...
* @return this method returns this and that ...
*/
}}}"	ivan.zapreev
3	Active Tickets	40	Error bounds and the numerical model-checking engine	Core	1.3	MRMC future	defect	ivan.zapreev	new	2008-06-27T16:40:47+0200	2008-06-27T16:40:47+0200	"Error bounds are not properly computed and used! For nested formulas it is not even known how to derive error bounds. For plain steady-state operator it is known but is not done:

 * Since probabilistic results are computed with a certain error bound for the steady-state (long-run) operators of PRCTL, PCTL, CSL and CSRL, we have to check +- error bound bound. '''WARNING''': Here the provided error bound is not quite correct, it is tighter than it should be but at least it is something!
{{{
 S{<=>p}[phi], err = get_error_bound()

 1. In case of ergodic MC we have to take:
         error_bound = err * | phi |
 2. In case of Non ergodic MC it should be:
         error_bound = \Sum_j (y_j * err +
                      x_ij * err * | phi_j | + err^2 * | phi_j |)
    Where \Sum_j ( (x_ij +- err)*(y_j +- err * | phi_j |) )
    is the way the probability is computed for the state i.
    x_ij  - the probability to reach BSCC_j from state i
    y_j   - the the total steady state probability of phi
            states in BSCC_j
    phi_j - the phi states in BSCC_j 
}}}

 * Imagine nested Until formulas, on every level there are computational errors. Now what if one one level due to such an error we include a wrong state / exclude a needed state, how does this affect the error bound of the formulas on the outer level?!
		
We should be able to set an error bound once and then to derive sub error bounds for sub formulas in such a way that the overall error remains the one the user wants. Right now the same error bound is just used everywhere.
"	ivan.zapreev
3	Active Tickets	41	Improving the architecture of MRMC.	General Architecture	1.3	MRMC future	enhancement	ivan.zapreev	new	2008-06-27T16:44:14+0200	2008-06-27T16:44:14+0200	" * May be the MRMC/src/runtime.c file is not such a good idea, since sometimes the matrix and/or vector of exit rates you work with gets replaced there. Perhaps everything but the runtime settings of MRMC should be passed only as function arguments.
 * Change an architecture in such a way that adding new algorithms and/or models, logics would become easy. Also algorithms such as lumping (bisimulation) should be easily addable. Since I expect that we may have to add Symmetry reduction.
 * Add a possibility for checking special conditions on the input models. For example in some cases we expect the "".tra"" file to be properly ordered but in fact it is not always needed. We need to add optional checks for such conditions.
 * New data structures should be easily addable, we need some universal interface, currently we work only with sparse matrices, we may and will need others.
 * Move the MRMC Core into a separate static library.
 * Add Java Native interface for the MRMC Core. This way MRMC could be used from a java-based GUI.
 * Improve error handling, now it is a mess, sometimes we just exit, sometimes we return 1, sometimes we return NULL. All in all it is not uniform and is unacceptable if someone wants to use MRMC as a library.
"	ivan.zapreev
4	Active Tickets	44	Additions to web page	Web Pages			task	nguyen, ivan.zapreev, christinajansen	new	2008-07-03T13:39:48+0200	2008-07-03T14:43:07+0200	"- Mention that mrmc-tool is hosted by rwth aachen / moves group

- add a disclaimer in the spirit of http://www.rwth-aachen.de/go/id/lwb
(perhaps just link to it, that should be sufficient)
"	henrik
4	Active Tickets	47	Adding a test-run report to the test-suite.	Test Suite	1.3.1	MRMC future	enhancement		new	2008-08-06T18:58:56+0200	2008-08-06T19:00:42+0200	"I would suggest to add the accumulated survey (log) on the passed/failed tests at the end of the testing process. This log should also include all the .diff data for the failed tests.

It might be a god idea to have separate log files for internal, functional and performance tests:

=======INTERNAL TESTS=======
   TESTS PASSED: ??
   TESTS FAILED: ??
 ------------------
 TESTS IN TOTAL: ??

 -----FAILED TESTS DIFFS------
        .out vs .golden

 --- internal/bitset
 <The diff file content goes here>
 .....

The same kind of file should be present for the functional tests

For the performance tests, the format should be different, something like the following:

==========PERFORMANCE TESTS==========
  --- <Full test case name>
   TESTS PASSED: ??
   TESTS FAILED: ??
  --- <Full test case name>
   TESTS PASSED: ??
   TESTS FAILED: ??
 .......
 -----FAILED CASE TEST NAMES ------
 <Full test case name>
 <Full test case name>
 <Full test case name>
 .......

Note that for performance tests:
1. The diff outputs are not necessary.
2. The test case is repeted several times, so if there is at least one failure of this test case, it should be present in the list of failed test cases."	ivan.zapreev
3	Active Tickets	48	Download archives for MRMC distributions	Web Pages	1.3	MRMC future	defect	nguyen, ivan.zapreev, christinajansen	new	2008-08-07T19:07:08+0200	2008-08-07T19:08:21+0200	"I've noticed that rather often people have troubles downloading MRMC distributions because the main servers, due to security reasons, reject e-mail with .zip attachments.

It seems to be that we should change the release scripts and the download scripts (also the old MRMC distributions) to produce and work with other archive types, I am not sure if it is the best choice but .tar.gz might be an option. We need a further investigation here. Also, we might introduce another download mechanism, that will involve sending a generated secure link in the e-mail, via which users can download MRMC."	ivan.zapreev
3	Active Tickets	49	uCTMDPi: 0-vector for timebound 0	Numerical Engine	1.3.1	MRMC future	defect		new	2008-09-30T13:32:33+0200	2008-10-03T08:20:53+0200	"Daniel discovered a bug in the uCTMDPi implementation, where the state vector is zero for a timebound 0.  See output below:

STATES 6
#DECLARATION 
@
reply.request.@
reply
reply.@
request
request.@
#END 
1 @
* 1 0.80
* 2 0.20
1 @
* 1 0.900
* 2 0.100
2 request.@
* 3 0.100
* 4 0.100
* 5 0.80
2 request.@
* 3 0.1500
* 4 0.0500
* 5 0.80
3 @
* 3 0.100
* 4 0.100
* 5 0.80
3 @
* 3 0.1500
* 4 0.0500
* 5 0.80
4 @
* 4 0.200
* 6 0.80
5 reply.@
* 1 0.80
* 2 0.20
5 reply.@
* 1 0.900
* 2 0.100
6 reply.request.@
* 3 0.100
* 4 0.100
* 5 0.80
6 reply.request.@
* 3 0.1500
* 4 0.0500
* 5 0.80
P{<1}[tt U[0,0.0] goal] 
P{<1}[tt U[0,10.0] goal] 
P{<1}[tt U[0,20.0] goal] 
P{<1}[tt U[0,30.0] goal] 
P{<1}[tt U[0,40.0] goal] 
P{<1}[tt U[0,50.0] goal] 
P{<1}[tt U[0,60.0] goal] 
P{<1}[tt U[0,70.0] goal] 
P{<1}[tt U[0,80.0] goal] 
P{<1}[tt U[0,90.0] goal] 
P{<1}[tt U[0,100.0] goal] 
quit 
#DECLARATION 
init 
goal 
#END 

1 init 
6 goal 
4 goal 
------------------------------------------------------------------- 
|                    Markov Reward Model Checker                    |
|                         MRMC version 1.3                          |
|         Copyright (C) The University of Twente, 2004-2007.        |
|               Copyright (C) RWTH-Aachen, 2006-2008.               |
|                            Authors:                               |
|    Ivan S. Zapreev (since 2004), Christina Jansen (since 2007),   |
|     David N. Jansen (since 2007), E. Moritz Hahn (since 2007),    |
|           Sven Johr (2006-2007), Tim Kemna (2005-2006),           |
|                    Maneesh Khattri (2004-2005)                    |
|           MRMC is distributed under the GPL conditions            |
|           (GPL stands for GNU General Public License)             |
|          The product comes with ABSOLUTELY NO WARRANTY.           |
|  This is a free software, and you are welcome to redistribute it. |
------------------------------------------------------------------- 
Logic			 = CSL
Loading the 'closed_Server_![reply,_request]!_![]!^2_abstr(Client0_U_Client1_U_Client2_U_Client3_U_Client4,_{rec=[1,_3,_8,_11,_13],_req=[0,_5,_6,_9,_14],_rd=[2,_4,_7,_10,_12]}).ctmdpi' file, please wait.
Loading the 'closed_Server_![reply,_request]!_![]!^2_abstr(Client0_U_Client1_U_Client2_U_Client3_U_Client4,_{rec=[1,_3,_8,_11,_13],_req=[0,_5,_6,_9,_14],_rd=[2,_4,_7,_10,_12]}).lab' file, please wait.
The Occupied Space is 776 Bytes.
Type 'help' to get help.
ERROR: Fox-Glynn: lambda = 0, terminating the algorithm
$ERROR_BOUND: 1.000000e-06
$MAX_RESULT: ( 0.0000000, 0.0000000, 0.0000000, 0.0000000, 0.0000000, 0.0000000 )
$STATE: { 1, 2, 3, 4, 5, 6 }

The Total Elapsed Model-Checking Time is 0 milli sec(s).
Fox-Glynn: ltp = 0, rtp = 153, w = 9.391435518908349e+296
$ERROR_BOUND: 1.000000e-06
$MAX_RESULT: ( 0.1543761, 0.2325637, 0.2325637, 1.0000000, 0.1543761, 1.0000000 )
$STATE: { 1, 2, 3, 5 }

The Total Elapsed Model-Checking Time is 0 milli sec(s).
Fox-Glynn: ltp = 0, rtp = 163, w = 1.241487345595022e+297
$ERROR_BOUND: 1.000000e-06
$MAX_RESULT: ( 0.2971468, 0.3621351, 0.3621351, 1.0000000, 0.2971468, 1.0000000 )
$STATE: { 1, 2, 3, 5 }

The Total Elapsed Model-Checking Time is 0 milli sec(s).
ERROR: Fox-Glynn: lambda >= 25, underflow. The results are UNRELIABLE.
Fox-Glynn: ltp = 0, rtp = 173, w = 1.430626769619844e+297
$ERROR_BOUND: 1.000000e-06
$MAX_RESULT: ( 0.4158131, 0.4698291, 0.4698291, 1.0000000, 0.4158131, 1.0000000 )
$STATE: { 1, 2, 3, 5 }

The Total Elapsed Model-Checking Time is 0 milli sec(s).
ERROR: Fox-Glynn: lambda >= 25, underflow. The results are UNRELIABLE.
Fox-Glynn: ltp = 6, rtp = 183, w = 1.613492625231256e+297
$ERROR_BOUND: 1.000000e-06
$MAX_RESULT: ( 0.5144444, 0.5593406, 0.5593406, 1.0000000, 0.5144444, 1.0000000 )
$STATE: { 1, 2, 3, 5 }

The Total Elapsed Model-Checking Time is 0 milli sec(s).
ERROR: Fox-Glynn: lambda >= 25, underflow. The results are UNRELIABLE.
Fox-Glynn: ltp = 12, rtp = 193, w = 1.763338686962057e+297
$ERROR_BOUND: 1.000000e-06
$MAX_RESULT: ( 0.5964232, 0.6337394, 0.6337394, 1.0000000, 0.5964232, 1.0000000 )
$STATE: { 1, 2, 3, 5 }

The Total Elapsed Model-Checking Time is 0 milli sec(s).
ERROR: Fox-Glynn: lambda >= 25, underflow. The results are UNRELIABLE.
Fox-Glynn: ltp = 19, rtp = 203, w = 1.899618880330600e+297
$ERROR_BOUND: 1.000000e-06
$MAX_RESULT: ( 0.6645612, 0.6955770, 0.6955770, 1.0000000, 0.6645612, 1.0000000 )
$STATE: { 1, 2, 3, 5 }

The Total Elapsed Model-Checking Time is 0 milli sec(s).
ERROR: Fox-Glynn: lambda >= 25, underflow. The results are UNRELIABLE.
Fox-Glynn: ltp = 25, rtp = 213, w = 2.007768695115810e+297
$ERROR_BOUND: 1.000000e-06
$MAX_RESULT: ( 0.7211950, 0.7469743, 0.7469743, 1.0000000, 0.7211950, 1.0000000 )
$STATE: { 1, 2, 3, 5 }

The Total Elapsed Model-Checking Time is 0 milli sec(s).
ERROR: Fox-Glynn: lambda >= 25, underflow. The results are UNRELIABLE.
Fox-Glynn: ltp = 33, rtp = 223, w = 2.123485373742082e+297
$ERROR_BOUND: 1.000000e-06
$MAX_RESULT: ( 0.7682671, 0.7896939, 0.7896939, 1.0000000, 0.7682671, 1.0000000 )
$STATE: { 1, 2, 3, 5 }

The Total Elapsed Model-Checking Time is 0 milli sec(s).
ERROR: Fox-Glynn: lambda >= 25, underflow. The results are UNRELIABLE.
Fox-Glynn: ltp = 40, rtp = 233, w = 2.217029960763284e+297
$ERROR_BOUND: 1.000000e-06
$MAX_RESULT: ( 0.8073918, 0.8252010, 0.8252010, 1.0000000, 0.8073918, 1.0000000 )
$STATE: { 1, 2, 3, 5 }

The Total Elapsed Model-Checking Time is 0 milli sec(s).
ERROR: Fox-Glynn: lambda >= 25, underflow. The results are UNRELIABLE.
Fox-Glynn: ltp = 47, rtp = 243, w = 2.300971995732339e+297
$ERROR_BOUND: 1.000000e-06
$MAX_RESULT: ( 0.8399108, 0.8547132, 0.8547132, 1.0000000, 0.8399108, 1.0000000 )
$STATE: { 1, 2, 3, 5 }

The Total Elapsed Model-Checking Time is 0 milli sec(s).
"	nguyen