****************************************************************** DEVELOPERS GUIDE FOR: Markov Reward Model Checker (MRMC) ****************************************************************** By Ivan S. Zapreev. In this file you will find general guidelines for how to perform all stages of MRMC development. ----------------------------------------------------------------- Contents ----------------------------------------------------------------- 1. Version control system 1.1 Work cycle 1.2 Working with branches 2. MRMC development 2.1 Changing Make files 2.2 Changing MRMC's output 2.3 Changing data structures 2.4 Adding new algorithms 2.5 Changing internal interfaces 2.6 Adding new source files 3. Test-suite development 3.1 Adding new internal/functional tests 3.2 Adding new performance tests 3.3 Modifying/Adding/Moving test scripts 4. Making a release 4.1 The release cycle 4.2 Using release scripts 4.3 Updating the web pages ----------------------------------------------------------------- 1. Version control system ----------------------------------------------------------------- From after MRMC v1.3 the tool development moves from CVS to SVN. Therefore, it is important that everyone has a good knowledge of this version control software. The best read, for learning SVN is http://svnbook.red-bean.com/ ******************************************** * 1.1 Work cycle: * Basic information on how to work with SVN can be found in Chapters 1. and 2. of the book recommended above. Working with any version control system, such as SVN or other, we recommend MRMC developers to use the following simple rules: - Every time you start working with the sources make sure you have the latest version of them, i.e. do update from the branch you work on. - Before committing sources, make sure to update your local files from the repository. - Only commit changes that are compilable and were tested using the test suite. - Never commit large chunks of changes. - Always provide valid and clear comments to the committed files. - If you want to make a major change in MRMC sources or you are not a member of MRMC team in Aachen, create your own branch in SVN and carry out your development there. ******************************************** * 1.2 Working with branches: * Information on how to use SVN for Branching and Tagging can be found in Chapter 4. of the book recommended above. When working on a separate branch of MRMC sources follow the following rules: - Periodically update from the main branch, to keep your sources up-to-date. - Never merge your changes into the main MRMC branch, unless: -- You updated your sources from the main branch, -- You thoroughly tested your sources, -- You got a merge approval from the team leader in Aachen. - Merging into the main MRMC branch is recommended to be done at the moments when the development there is finalized, i.e the main branch version is: -- tagged as a pre-merge version for your branch, -- known to be compilable, -- was thoroughly tested. ----------------------------------------------------------------- 2. MRMC development ----------------------------------------------------------------- When working with the main MRMC branch, please remember that, it is a big responsibility to do it. Please, keep in mind that any changes you make should be sound and complete. The former means, that you should not commit modifications, such as hacks, that are only meaningful for you. For this, please use your own branch. Also, never live debug outputs in the committed sources, unless it is commented out. The latter means that before you have to take care about keeping MRMC repository consistent. For example, changing MRMC output might affect the test suite (the tests will start failing), also parts of the MRMC manual might become obsolete or incorrect or will need to be extended. Do not think that someone will do this work for you. Always do things yourself and do your best. Note that, any changes of MRMC, that will go into the next release, should be reflected in the file: ./RELEASENOTES The following will help you to keep MRMC sources consistent. ******************************************** * 2.1 Changing Make files: * When changing MRMC makefiles, remember that ./makefile.def is also used by the MRMC test suite. For example, internal and performance test use this file in the following make files: ./test/internal_tests/makefile ./test/performance_tests/scripts/gcc/makefile Thus, after changing MRMC makefiles, always check that both, internal and performance tests work fine. ******************************************** * 2.2 Changing MRMC's inputs/outputs: * Changing MRMC inputs/outputs is likely to affect the following parts of MRMC repository: - The functional and/or performance test suites - The MRMC manual Therefore, after changing MRMC inputs/outputs make sure that: - All functional tests run without failures. If failures occur, check the *.diff files for the output changes. If the changes are valid, then update the golden files. - All performance tests run without failures. Changing MRMC output can affect: (i) statistics gathering, (2) functional part of lumping-performance tests. - If there are no functional tests that check the new output then extend the test suite with new tests. - The content of MRMC manual is up to date, i.e. check the examples, the inputs/outputs descriptions, and etc. For more details on the MRMC test-suite, see it's manual in the ./doc folder. ******************************************** * 2.3 Changing data structures: * If you are to change the data structures such as: - sparse matrices, - bit sets, - and etc. Make sure that: - The data structures and algorithms that work on them are well documented, see Section 2.6. - All the old internal tests PASS, - You add internal tests for the new functionality, - You thoroughly test MRMC sources with and without valgrind on functional tests. (See Section 3.1 of the test-suite manual) Note that, in this case it is strongly recommended to run all performance tests under valgrind as well. Not all the flaws can be detected with the functional sub-suite. The lumping- performance tests can be run with the zero number of performance repetitions, for the simulations-performance tests the number of repetitions should be set to one. (See Section 2.3 of the test-suite manual) ******************************************** * 2.4 Adding new algorithms: * If you add new algorithms make sure that you: - The algorithms are well documented, see Section 2.6. - Add proper help messages and parameters printing: ./include/help.h, ./src/runtime.c, and etc. - Add new functional and internal tests that test them, - Test MRMC on internal and functional test with and without valgrind. If new algorithms alter inputs/outputs of MRMC, follows the rules of Section 2.2. ******************************************** * 2.5 Changing internal interfaces: * If you change the MRMC's internal interfaces then follow the rules given in Sections 2.3, 2.4 and 2.6. ******************************************** * 2.6 Adding new source files: * If you add new source files then make sure that: - A proper location for these files is chosen in the directory tries of ./include and ./src. ./storage - data structures and operations on them, ./algorithms - low-level algorithms, such as numerical methods, graph analysis, random-number generators, and etc, ./modelchecking - model checking algorithms, ./lumping - algorithms for model minimization, ./io - methods for managing MRMC inputs and outputs, ./io/parser - methods for parsing and interpreting MRMC command-prompt inputs. - Files have a standard header for MRMC files, see for example ./src/runtime.c - Methods and data structures contain proper comments in a proper format. The best way is to take the style used for: -- SFTypeRes structure in: ./include/io/parser/parser_to_tree.h -- modelCheckStatesCommon(...) method in: ./src/modelchecking/simulation_common.c NOTE: Avoid meaningless comments that do not add any information to what one can easily deduce looking at the commented piece of code. For example, having a method parameter pBitSet commented as .... * @param pBitSet the bitset pointer .... void method( bitset* pBitSet); makes no sense, since it is it is trivial. In this case you have to write what kind of information pBitSet should hold and what are it's allowed values, e.g.: .... * @param pBitSet should contain the enabled states in the model, we should have pBitSet != NULL, otherwise the method crashes, also if pBitSet is empty, the method's behavior is undefined. .... void method( bitset* pBitSet); - The variable- and function-naming convention is preserved. There are no strict guidelines here, but an example of a well written source code is the modelCheckStatesCommon(...) method in: ./src/modelchecking/simulation_common.c Yet, note the following rules: -- Variable names should be self descriptive. They have to reflect whether it is a pointer (or some other data type) and to indicate what kind of value the variable stores, e.g.: bitset *pPhiStateBitset = NULL; defines a pointer to the bitset that contains states that satisfy formula Phi. -- The method names should indicate what the methods do. For example, the method: int convert( double a); has a dumb name, it is meaningless and if one meets the method's invocation inside the source code, (s)he can not deduce what the method does from it's name. In this case a proper method name could be (assuming that the method converts double to int): int convertDoubleToInt( double dValue); Also note that, the variable name "a" was substituted with "dValue" indicating that it is a value of type double. - If new sources add algorithms, follow the rules of Section 2.4. - If new sources add data structures, follow the rules of Section 2.3. - If new sources alter MRMC's inputs/outputs, follow the rules of Section 2.2. ----------------------------------------------------------------- 3. Test-suite development ----------------------------------------------------------------- Testing MRMC sources is of an utmost importance. This ensures that tool stays reliable and helps to verify the tool's modifications, as well as analyze it's performance. Details on how to use the MRMC test- suite and also information about its structure can be found in the test-suite manual: ./doc/TS_Manual.pdf Note that, any changes of the test-suite, that will go into the next MRMC release, should be reflected in the file: ./test/RELEASENOTES ******************************************** * 3.1 Adding new internal/functional tests: * Adding internal and functional tests is a relatively simple task. One just has to follow the general patterns that can be easily deduced from the structure of: ./test/internal_tests ./test/functional_tests Some general information about this structure can be found in Section 3.3.1 and Chapter 4. of the test-suite manual. Adding new test here, should not affect other parts of the MRMC repository. A simplest way of adding new tests in the existing sub-suites is copying. In this case be careful not to copy SVN's data. ******************************************** * 3.2 Adding new performance tests: * Adding performance tests is a relatively simple task. One just has to follow the general patterns that can be easily deduced from the structure of: ./test/performance_tests ./test/performance_tests/lumping ./test/performance_tests/simulations Some general information about this structure can be found in Sections 3.3.2, 3.3.2 and Chapter 5. of the test-suite manual. It is important to note that, lumping test, although having common scripts and some other similarities, are different from simulations test. A simplest way of adding new tests in the existing sub-suites is copying. In this case be careful not to copy SVN's data. If one has to add new performance sub suite, on the level of lumping and simulations sub suites, then it is better to reuse the structure and/or scripts of the simulations sub-suite, since this one is more powerful. Note that, in this case all common parts (scripts) have to be unified and moved from .performance_tests/simulations/scripts into .performance_tests/scripts Doing so, make sure that simulation performance scripts still run correctly. In case a new sub-suite is added, make sure that the corresponding changes are reflected in the test-suite manual. ******************************************** * 3.3 Modifying/Adding/Moving test scripts: * When modifying/adding/moving test scripts make sure that: - The new scripts location agrees with the used test-suite structure. See the test-suite manual for more details. - The dependent sub suites still run. - The script files have proper comments, such as in: ./performance_tests/scripts/shell/generate_eps.sh It is important to describe the script's usage, parameters and to comment its content. - If you work on Mac OS and/or Windows note that the performance tests were not designed for this platforms. Thus, if you made them work there and want to commit the changes to the main MRMC branch, test that all your changes are sure to work on a Linux machine! The latter can only be done bu letting all the performance test run with the number of performance repetitions set to 2 (See Sections 2.3 and 3.1 of the test-suite manual.). - The corresponding are be reflected in the test-suite manual. ----------------------------------------------------------------- 4. Making a release ----------------------------------------------------------------- This section contain information about how to make a new MRMC release. Before reading further remember that: Preparations for the next release start at the moment of the current one. ******************************************** * 4.1 The release cycle: * Typically preparations for the MRMC release consist of the following stages: - MRMC development: This might include development of some MRMC features in different branches and then merging them back into the main one. - MRMC testing: No new features are allowed to be added, i.e. the MRMC functionality is not changing any more. At this moment: -- We perform a thorough testing of MRMC using internal and functional tests, with and without valgrind, is done. -- If bugs are found, then they are fixed and the regression tests are added to the internal- or functional- test suite. -- We check the quality of MRMC sources and, if needed, add comments, fix improper implementations and etc. This process requires repetitive testing of the tool changes. -- We make sure that MRMC is still compilable on: Max OS X, Linux and Windows XP (Vista?) - Test-suite testing: no new tests or tests scripts are allowed to be added. The test suite outputs should remain impact. -- We make sure that internal and functional tests have up-to-date golden files. -- We make sure that performance test have up-to-date golden files. -- We make sure that all test- scripts run properly. (performance tests should collect correct statistics.) -- We make sure that internal and functional tests still run: Max OS X, Linux and Windows XP (Vista?) - Updating documentation: -- We make sure that the MRMC manual is up to date. -- We make sure that the test-suite manual is up to date. -- We update information on the MRMC web-pages, see Section 4.3 -- Make sure that all changes to the distribution structure are reflected in the ./README and ./test/README files. -- Make sure that the release notes are up to date: ./RELEASENOTES and ./test/RELEASENOTES - Checking release scripts: check that the release scripts produce correct distributions, on Mac OS X, Linux, and Windows. This means that source and binary distributions have to contain all needed files and should not contain any temporary files, and other files that should not appear in the distributions. The release scripts have to be checked for MRMC itself (all platforms and all modes) and for its test suite (all platforms). - Preparing the release files for MRMC and its test suite. - Placing the release files on the MRMC web pages. - Checking that the MRMC and test-suite distributions can be downloaded and contain the proper content. - Sending a "New release" notification letter to the mrmc-users mailing list. ******************************************** * 4.2 Using release scripts: * In order to create MRMC and its test-suite distributions one has to use the ./release.sh script. When run without parameters this script produces the following output. >>release.sh INFO: Verifying the script parameters .... FAILED ERROR: Incorrect script arguments. USAGE: ./release.sh #1 #2 #3 This is an automated distribution script, where: #1 - the distribution target, one of: {mrmc, test} #2 - a version, can be something like '1.3' or '2.1b'. #3 - the distribution kind, one of: {src, win, lin, mac} NOTE: The parameter #3 has to be provided only when #1=mrmc This output implies that: - For releasing the MRMC-source distribution one has to run: >>release.sh mrmc src on any (Mac, Windows or Linux) machine. - For releasing the MRMC binary distribution one has to run: >>release.sh mrmc win on a Windows machine, >>release.sh mrmc lin on a Linux machine, >>release.sh mrmc mac on a Max OS X machine. The binary distribution, in addition to the MRMC sources will include the content of the ./bin directory. - For releasing the test-suite one has to run >>release.sh test on any (Mac, Windows or Linux) machine. Note that, the version number of the test suite should be the same as for the released MRMC version. The release.sh script uses the following files: - release.mrmc.bin.files: the list of files and folders that should be present in the binary distribution of mrmc release. - release.mrmc.src.files: the list of files and folders that should be present in the source distribution of mrmc release. - release.test.files: the list of files and folders that should be present in the distribution of test-suite release. Since folders listed in the files above can contain some undesirable files or sub folders, the release.sh script uses the files: - exclude.mrmc.lst: the list of files and folders that should be ignored when making the mrmc-release archive. - exclude.test.lst: the list of files and folders that should be ignored when making the test-suite release archive. which allow to indicate what content, in the folders that have to be present in the release distribution, should be ignored. Due to the differences in shell and/or zip utility implementations on different platforms, it is important to check the content of resulting release archives before putting them online. The MRMC distribution files should be located in: - Test suite: www.mrmc-tool.org/downloads/MRMC/TestSuite - MRMC: www.mrmc-tool.org/downloads/MRMC/Distrib The latter one is protected by the .htaccess file and is accessible only from the www.mrmc-tool.org/downloads.php script. To which the new MRMC and Test suite versions have to be added in a straight forward manner. Please see the comments inside downloads.php. Also note that the new version of the MRMC and Test suite manuals have to be placed into www.mrmc-tool.org/downloads/MRMC/Specs and linked from the "Specifications" page in Trac/Wiki. ******************************************** * 4.3 Updating the web pages: * Keeping MRMC web-pages up to date is important. Below we provide a list of web pages/sites that have to be kept up-to-date. These sources of information should be updated, at least, prior to every new release of MRMC. - www.mrmc-tool.org This is the MRMC home site, here we should be updating: -- News section: our visitors have to see that MRMC activities are not halted, otherwise they can loose their interest in the tool. -- Specs section: Put MRMC manuals there and other things such as posters and etc. This way people can learn about MRMC by suddenly finding its manual in google results. -- Bibliography section: Put all papers on MRMC and related research there. Note that, at least one of the paper authors has to be from the MRMC team. -- Related section: Put all sort of third-party projects, papers and etc, that use or at least mention MRMC. -- Downloads section: The new MRMC and its test-suite release files have to be accessible from this page. -- There are other sections on the web-page which in our opinion might need a bit less maintenance. - www.mrmc-tool.org/downloads.php When the Track pages are changed, make sure that the downloads.php is still consistent with the rest of the site. The html header and footers, for the general page layout are respectively located in downloads_h.html and downloads_f.html. - http://en.wikipedia.org/wiki/Markov_Reward_Model_Checker_%28MRMC%29 This is a (well known) wikipedia page for MRMC. Of course www.mrmc-tool.org has its own WiKi pages, but they are much less powerful and one can not be accessed from www.wikipedia.org. Thus we have to keep this www.wikipedia.org pages up to date. - http://anna.fi.muni.cz/yahoda/ This is a list of various available model-checking tools. MRMC is present there and after you register, it is possible to update its description. In the Yahoda list, tools that recently had a new release are highlighted. This is why it is important to keep the MRMC entry up to date.