#!/bin/bash

LOGDIR=logs-bisim
mkdir -p $LOGDIR

SIZES2=(10 20 30 40)

for SIZE2 in "${SIZES2[@]}"
do
    SIZE1=$((SIZE2 * 4))
    echo $SIZE1 $SIZE2
    
    LOGFILE=erlangen"$SIZE1"_"$SIZE2".ss.nobisim.log
    echo $LOGFILE
	storm -v --timemem --prism erlangen.prism -pc --constants l_init=1,mu2=2,delta2=0.0007,size1="$SIZE1",size2="$SIZE2",alpha=48,beta=0.01 --prop erlangen.props avail_ss >| $LOGDIR/$LOGFILE
    LOGFILE=erlangen"$SIZE1"_"$SIZE2".ss.bisim.log
    echo $LOGFILE
	storm -bisim -v --timemem --prism erlangen.prism -pc --constants l_init=1,mu2=2,delta2=0.0007,size1="$SIZE1",size2="$SIZE2",alpha=48,beta=0.01 --prop erlangen.props avail_ss >| $LOGDIR/$LOGFILE
	
	TIMES=(500 1000 1500)
	for TIME in "${TIMES[@]}"
	do
		echo "$TIME"
		LOGFILE=erlangen"$SIZE1"_"$SIZE2".tr"$TIME".nobisim.log
		echo $LOGFILE
		storm -v --timemem --prism erlangen.prism -pc --constants l_init=1,mu2=2,delta2=0.0007,size1="$SIZE1",size2="$SIZE2",alpha=48,beta=0.01,T="$TIME" --prop erlangen.props avail_tr >| $LOGDIR/$LOGFILE
		LOGFILE=erlangen"$SIZE1"_"$SIZE2".tr"$TIME".bisim.log
		echo $LOGFILE
		storm -bisim -v --timemem --prism erlangen.prism -pc --constants l_init=1,mu2=2,delta2=0.0007,size1="$SIZE1",size2="$SIZE2",alpha=48,beta=0.01,T="$TIME" --prop erlangen.props avail_tr >| $LOGDIR/$LOGFILE
	done
	
done

grep "States:" $LOGDIR/*
grep "Time for model preprocessing" $LOGDIR/*
grep "Time for model checking" $LOGDIR/*
grep "wallclock time" $LOGDIR/*