Examples

In this page you can find the collection of examples that you can run inside NuSMV and that you can find in the NuSMV distribution.

All examples work since NuSMV 2.5.1, where a strong distinction between integers and boolean types has been introduced. The same examples that work with previous versions of NuSMV can be found in the older versions of NuSMV binary and source packages.

AuthorDescriptionFiles
NuSMV sourceNuSMV order file
Sergey Berezin () Shuttle Digital Autopilot engines out (3E/O) contingency guidance requirements.
Armin Biere () The alternating bit protocol for different length of the DATA in bits. For instance abp4.smv has the data field of length 4 bits.
Sergio Campos A model for the PCI Bus protocol.
Sergio Campos Different version of the model of the PCI Bus protocol.
Sergio Campos A data driven pipeline example.
  • No ordering file
Sergio Campos A model of a robotics controller.
William Chan () A model of part of a preliminary version of the system requirements specification of TCAS II (Traffic Alert and Collision Avoidance System II). TCAS II is an aircraft collision avoidance system required on most commercial aircraft in United States.
James Corbett () Deadlock detection for a communication protocol of an complex Ada program.
James Corbett () Deadlock detection for dining philosophers with dictionary.
James Corbett () Deadlock detection for dining philosophers with host.
James Corbett () Deadlock detection for a file transfer protocol.
James Corbett () Deadlock detection for a remote furnace program.
James Corbett () Deadlock detection for a gas station (non-queuing).
James Corbett () Deadlock detection for a keyboard/screen interaction in a window manager.
James Corbett () Deadlock detection for a distributed memory manager.
James Corbett () Deadlock detection for an automated highway system overtake protocol
Edelweis Helena Ache Garcez A priority queue example.
Edelweis Helena Ache Garcez A model of a producer consumer.
Klaus Havelund () A bounded retransmission protocol (communication protocol).
  • No ordering
Scott T. Probst Batch reactor system models.
Kirsten Winter () The production cell control model.
Unknown A synchronous three bit counter.
  • No ordering file
Unknown An asynchronous three bit counter.
  • No ordering file
Unknown A synchronous version of a distributed mutual exclusion algorithm with three cells. (Use -f option).
Unknown A synchronous version of a distributed mutual exclusion algorithm with sixteen cells. (Use -f option).
Unknown A asynchronous version of a distributed mutual exclusion algorithm with three cells. (Use -f option).
Unknown A asynchronous version of a distributed mutual exclusion algorithm with sixteen cells. (Use -f option).
Unknown A model of the GIGAMAX cache coherence protocol.
  • No ordering file
Unknown A simple mutual exclusion algorithm.
  • No ordering file
Unknown Another simple mutual exclusion algorithm.
  • No ordering file
Unknown A model of two processes synchronized using a semaphore.
  • No ordering file
Unknown The well known "short.smv" example.
  • No ordering file
Unknown A model of a synchronous arbiter with 5 and 10 elements.
  • No ordering file
Unknown A model of a queue.
  • No ordering file