C HTML C++ GAP Makefile Perl
Fetching latest commit…
Cannot retrieve the latest commit at this time.
|Failed to load latest commit information.|
README ====== YASMINE (Yet Another Symbolic Modelling INteractive Environment) started off in fall 2011 as a tentative and partial C++ reimplementation of the NuSMV2 model checker. As a former member of the NuSMV2 development (in the years from 2008 to 2011) team I was never happy with a few architectural choices that were inherited from the long history of the NuSMV model checker and/or were due to the amount of legacy code and tools that relied on it. Don't get me wrong, I really think NuSMV is a great piece of software. And I owe to the developers and researchers in FBK most - if not all - of my scientific and software engineering training. Those people are really fantastic. It's just that I have been wondering for years what that project would have been like, if one was completely free to redesign it all from-the-scratch. This is exactly why this project exists in the first place. Overtime, YASMINE has significantly diverged from the original goal of making a NuSMV re-implementation. I think of it as a full-fledged interactive environment for symbolic model verification among other things. The tool is designed and crafted with high flexibility requirements and coding standards, as a test bed for new ideas. Of course, feedback (and criticism too) is very welcome, expecially if constructive. The input language for YASMINE is a dialect of SMV which retains only partial compatibility with NuSMV's SMV. However, I think automatic tools could easily be designed to translate NuSMV's SMV models into YASMINE's. Hovewer, this is currently out of scope. According to my best knowledge, the main differences between the two systems are: 0. Technology YASMINE is 100% gnu++98 C++ code, using the CUDD library by C. Somenzi (add ref) and a custom Minisat solver. Checking technology is SAT-based, whereas NuSMV evolved overtime from a pure BDD system (also based on CUDD) to a hybrid BDD/SAT model checker. The CUDD library in YASMINE is used extensively in order to build the appropriate boolean encoding of formulae, in a format that is suitable for SAT processing. The parser for both the input model language and the interpreter shell is a LL(1) (with a few exceptions) top-down parser built with the ANTLR parser generator, using Jim Idle's back-end for C code generation. AFAIK, NuSMV uses a more standard bottom-up GNU LALR Bison parser. The well known C++ BOOST libraries are extensively used for high-performance hashtables, automated unit and integration testing, program options parsing and regular expression matching. 1. Input language 1.1. The type system and operator semantics has been carefully redesigned, to closely match standard C-like semanthics. In fact, main driving scenario of application for this design is software model checking. 1.1.1. No finite range integer types or int enumeratives allowed. Models should ordinary integer (either signed or unsigned) variables. 1.1.2. Enumeratives must be pure symbolic (all literals as identifiers) AND disjunct; 1.1.3. Integers can only be represented using signed(n) and unsigned(n) types; where n is the type width, expressed as the number of hexadecimal digits in its 2's complement representation; 1.1.4. All C standard notations for integers (octal, decimal, hexadecimal) are supported (e.g. 052, 42, 0x2a). 1.1.5. Non-determinism is supported using the ANY construct; (e.g. x = ANY(2, 3, 5, 7, 11, 13, 17, 19, 23)) (REVIEW, NOT SURE ABOUT THIS) 1.1.6. & --> &&, | --> ||, introduced standard C notation for ^ (xor) 1.2. NuSMV's INVAR, ASSIGN, and init keywords are not supported. There is only one way to express an FSM, that is using INIT (for initial states) and TRANS(for transition relation); 1.3. No INVARSPEC, LTLSPEC, CTLSPEC, (...) in input models. YASMINE models are just that, models (namely, FSM descriptions). Support is given at the command level in the interactive specify properties to be checked. 2. Interactive environment 2.1. YASMINE provides a fully Turing-complete interpreted language for process control: constructs are provided for result inspection (IF), looping (WHILE), and formatted output (PRINT) among other things. The tool is designed to be fully scriptable; 2.2. (...) DISCLAIMER ========== This code 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 Lesser General Public License for more details. YASMINE is in no way related to, or endorsed by, the NuSMV2 development board and/or FBK.