TLSF model checker using IIMC

mc.sh

#!/usr/bin/bash

# This script model checks a given AIGER file wrt. TLSF specification:
# @return: 0 on success, non-zero on failure

# Convert TLSF to AIGER monitor:
#   syfco --format smv -m fully example.tlsf | smvtoaig > monitor.aag

# Combine monitor with implementation:
#   combine-aiger monitor.aag implementation.aag > combined.aag

# Then model check `combined.aag` using the IIMC model checker of AIGER
# Dependencies:
# combine_aiger="/home/art/software/combine-aiger/combine-aiger"
# syfco="syfco"
# smvtoaig="smvtoaig"
# model_checker="/home/art/software/iimc/iimc"

set -e  # stop on error
set -o pipefail  # stop on error for pipelined commands

# define colors for pretty printing
RED='\033[1;31m'
# '\[\e[32;1m\]
GREEN='\033[1;32m'
DC='\033[0m' # default color

die () {
  echo "*** [mc.sh] $*" 1>&2
  exit 1
}

msgGreen () {
  echo -e "${GREEN}$* ${DC}"
}

msgRed () {
  echo -e "${RED}$* ${DC}"
}

msg () {
  echo -e "$*"
}

# tools
combine_aiger="/home/art/software/combine-aiger/combine-aiger"
syfco="syfco"
smvtoaig="smvtoaig"
model_checker="/home/art/software/iimc/iimc"

# script internal variables
model=""
tlsf=""
verbose=no
tmpdir=""

while [ $# -gt 0 ]
do
  case $1 in
    -v) verbose=yes;;  # it is set correctly, but it is not used
    -h)
cat << EOF
usage: mc.sh [-h] <model> <tlsf>
-h      print this command line option summary
<model> model in AIGER format
<tlsf>  property in TLSF format
EOF
exit 0
;;
    -*) die "invalid command line option '$1'";;
    *)
        [ -f "$1" ] || die "invalid file '$1'"
        if [ x"$model" = x ]
        then
            model=$1
        elif [ x"$tlsf" = x ]
        then
            tlsf=$1
        else
            die "more than model and/or tlsf file"
        fi
       ;;
  esac
  shift
done

if [ x"$model" = x ]
then
  die "model is not given"
fi

if [ x"$tlsf" = x ]
then
  die "TLSF property is not given"
fi

msg "model checking model '$model' against specification '$tlsf'..."
tmpdir=$(mktemp -d)
msg "using temporary directory '$tmpdir'"

# SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )"


#$syfco --format smv -m fully "$tlsf" | $smvtoaig > $tmpdir/monitor.aag
$syfco --format smv -m fully "$tlsf" -o $tmpdir/spec.smv
$smvtoaig $tmpdir/spec.smv $tmpdir/monitor.aag

$combine_aiger $tmpdir/monitor.aag $model > $tmpdir/combined.aag

$model_checker -v 1 $tmpdir/combined.aag | tee $tmpdir/iimc.log

mc_result=$(tail -n 1 $tmpdir/iimc.log)
if [ "$mc_result" = "1" ]
then
  msgRed "MC failed: the circuit is buggy!"
  msg "See files in $tmpdir"
  exit 1
else
  msgGreen "MC: passed!"
  rm -rf $tmpdir
  exit 0
fi