Skip to content
This repository

The YASMINE Project

tree: a462f6e344
README
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.
Something went wrong with that request. Please try again.