Some NuSMV Experiments on the Mode Synchronization Protocol in DSAOCSS

Abstract

A non-exhaustive collection of files on NuSMV experiments on the mode synchronization protocol in DSAOCSS. The "input files" are mpbase.smv, split.sh, _split.sh, batch.sh, and inc.txt.The file btc.txt and and all lmp??.txt files have been produced by batch.sh that in turn needs mp??.smv files produced by split.sh.The mp??.smv files are not included in this archive because they are easily reproducible and because every mp??.smv is simply a concatenation of mpbase.smv and a single LTLSPEC line. The file gdbmp22.txt is an output of a debugging session and is included in order to support the conjecture that all segmentation fault messages in btc.txt are due to effective running out of memory in software where use of memory is not properly monitored.