#!/bin/bash

# usage: naive_test.sh <program1.sm> <program2.sm> <models>

# (C) Emilia Oikarinen 2005

prog1=$1
prog2=$2
models=$3

DIR=../bin

if test -d tmp
then 
    true
else mkdir tmp
fi

rm -f tmp/test.model
touch tmp/test.model

echo 0 > tmp/test.cnt

# try finding a counter-example among the models
cat $models | fgrep Stable | while read a b model
do
  n=`expr $n + 1`
  $DIR/testsm $prog2 $model | $DIR/smodels 1 > tmp/test.out
  cnt=`fgrep Answer tmp/test.out | wc -l`
  if test $cnt -eq 0
  then
    echo "Counter Model: $model" > tmp/test.model
    echo $n > tmp/test.cnt 
    exit 0
  fi
done

# number of models needed to check, zero if no counter-example was found
read n < tmp/test.cnt
cat $prog1 | $DIR/smodels $n | fgrep points | awk '{print $5}'