HTTPS clone URL
Subversion checkout URL
The YASMINE (Yet Another Symbolic Modelling INteractive Engine) Project
C HTML C++ GAP Makefile Perl
Fetching latest commit…
Cannot retrieve the latest commit at this time
|Failed to load latest commit information.|
README ====== The YASMINE (Yet Another Symbolic Modeling INteractive Engine) project started off in fall 2011 as a tentative and partial C++ re-implementation of the NuSMV2 model checker. As a former member of the NuSMV2 development team (in the years between 2008 and 2011) I was never completely happy with a few architectural choices, inherited from the long history of the NuSMV model checker and/or 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. The input language for YASMINE is a dialect of SMV which retains only partial compatibility with NuSMV's original SMV language. In this area, my interest is about making the language easy to use, while not giving up on expressiveness. The tool is designed and crafted with high flexibility requirements as a test bed for new ideas - knowing for sure some of them will prove quite unsatisfactory. Of course, feedback (and criticism too) is very welcome, especially if constructive. BUILD ===== The build system uses autools. The following packages are required to perform a build: The following packages are optional. 1. Input language 1.1. The type system and operator semantics has been carefully redesigned, to match standard C-like semantics as closely as possible. As stated above, main driving application scenario for this design is software model checking. *All* integer arithmetic is 2's complement as it would be performed by any C compiler. 1.1.1. NuSMV's finite range integer types and int enumeratives are not supported. Models should use ordinary integer types (either signed or unsigned). Users are encouraged to adopt c99 integer types: (u)int8_t, (u)int16_t, (u)int32_t, (u)int64_t; 1.1.2. Support for Fixed-point rational arithmetic; 1.1.3. Enumeratives must be pure symbolic (all literals as identifiers) AND disjunct; 1.1.4. All C standard notations for integers (octal, decimal, hexadecimal) are supported (e.g. 052, 42, 0x2a). NuSMV's special-purpose format for bit-vectors is *not* supported; 1.1.5. Non-determinism is supported using the ANY construct; (FUTURE) (e.g. x = ANY(2, 3, 5, 7, 11, 13, 17, 19, 23)) 1.2. 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 shell, in order to allow specifying properties to be checked. Currently only invariant checking is in scope; 2. Interactive environment 2.1. The YASMINE shell 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; (FUTURE) 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. YASMINE does not contain *a single* line of code coming from NuSMV's code base, with the possible exception of the custom MiniSAT solver that was part of *my* B. Sc. dissertation.