# Murphi

**Repository Path**: twohaha/murphi

## Basic Information

- **Project Name**: Murphi
- **Description**: Murphi model checking tool (3.1)
- **Primary Language**: Unknown
- **License**: Not specified
- **Default Branch**: master
- **Homepage**: None
- **GVP Project**: No

## Statistics

- **Stars**: 0
- **Forks**: 1
- **Created**: 2024-04-18
- **Last Updated**: 2026-02-06

## Categories & Tags

**Categories**: Uncategorized

**Tags**: None

## README

# Murphi 3.1 

This is simply a home for the classic Murphi model checking tool (3.1) from David Dill's Stanford group.


Original Repository: https://github.com/tyler-utah/Murphi2019


## Requirements

yacc, flex, flex-old

install flex-old if undefined reference to `yylex' error occurs.

## Quick Start

```bash

make
cd /to/your/directory/of/xxx.m
../../bin/mu -b -c xxx.m
./xxx -m2000 -pr -tv -p5 -sym3 -d ./

```

## Compiler Options

```bash
>> mu -h
The options are shown as follows:

        -h                      help
        -l                      print license
        -b                      use bit-compacted states
        -c                      use hash compaction

An argument without a leading '-' is taken to be the input filename,
        which must end with '.m'
```

## Verifier Options

```bash
>>  ./MI_example -h
Options:
1) General:
        -h            help.
        -l            print license.
2) Verification Strategy: (default: -v)
        -s            simulate.
        -v or -vbfs   verify with breadth-first search.
        -vdfs         verify with depth-first search.
        -ndl          do not check for deadlock.
3) Others Options: (default: -m8, -p3, -loop1000)
        -m<n>         amount of memory for closed hash table in Mb.
        -k<n>         same, but in Kb.
        -loop<n>      allow loops to be executed at most n times.
        -p            make simulation or verification verbose.
        -p<n>         report progress every 10^n events, n in 1..5.
        -pn           print no progress reports.
        -pr           print out rule information.
4) Error Trace Handling: (default: -tn)
        -tv           write a violating trace (with default -td).
        -td           write only state differences from the previous states.
                      (in simulation mode, write only state differences in
                       verbose mode.)
        -tf           write full states in trace.
                      (in simulation mode, write full states in verbose mode.)
        -ta           write all generated states at least once.
        -tn           write no trace (default).
5) Reduction Technique: (default: -sym3 with -permlimit 10 and multiset
                                  reduction)
        -nosym        no symmetry reduction (multiset reduction still effective)
        -nomultiset   no multiset reduction
        -sym<n>       reduction by symmetry
        -permlimit<n> max num of permutation checked in alg 3
                      (for canonicalization, set it to zero)
                      n | methods
                      -----------------------------------
                      1 | exhaustive canonicalize
                      2 | heuristic fast canonicalization
                          (can be slower or faster than alg 3 canonicalization)
                          (use a lot of auxiliary memory for large scalarsets)
                      3 | heuristic small mem canonicaliztion/normalization
                          (depends on -permlimit)
                      4 | heuristic fast normalization (alg 3 with -permlimit 1)
6) Hash Compaction: (default: hash compaction with 40 bits)
        -b<n>         number of bits to store.
        -d dir        write trace info into file dir/MI_example.trace.
```

## Contributors

- Xuezheng (xuezhengxu@126.com)
- Tyler Sorensen (tyler.sorensen@outlook.com)