Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
The YASMINE (Yet Another Symbolic Modelling INteractive Engine) Project
tree: 15dce9e852

Fetching latest commit…

Cannot retrieve the latest commit at this time

Failed to load latest commit information.
3rdparty
doc
extra
m4
src
test
AUTHORS
COPYING
ChangeLog
Makefile.am
NEWS
README
configure.ac
gnusmv.pc.in

README

README
======

gnuSMV is 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 in FBK most - if not all - of my Software
Engineering education. Those people are really fantastic. It's
just that I've been wondering for years what that code would've
be like if one was completely free to redesign it all
from-the-scratch. This is exactly what this project is all about.

TODO
====

. Improve ANTLR build scripting in a portable fashion (easy)
. Add getopt support for arg parsing (easy)
. Embed ADDs for booleanization (hard)
. Port booleanization algorithms from NuSMV (easy)
. ZMQ-based workload distribuition workbench and control shell (fun!)

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.

gnuSMV is in no way related or endorsed by the NuSMV2 development
board and/or FBK.
Something went wrong with that request. Please try again.