#!/bin/bash

LOGDIR=logs-pvs
mkdir -p $LOGDIR

SIZES2=(10 20 30) # 40)

for SIZE2 in "${SIZES2[@]}"
do
    SIZE1=$((SIZE2 * 4))
    echo $SIZE1 $SIZE2
    
    LOGFILE=erlangen"$SIZE1"_"$SIZE2".ss.prism.log
    echo $LOGFILE
    prism -s -gs -maxiters 1000000 -nossdetect erlangen.prism -const l_init=1,mu2=2,delta2=0.0007,size1="$SIZE1",size2="$SIZE2",alpha=48,beta=0.01 erlangen.props -prop avail_ss >| $LOGDIR/$LOGFILE
    LOGFILE=erlangen"$SIZE1"_"$SIZE2".ss.storm.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
	
	TIMES=(500 1000) # 1500)
	for TIME in "${TIMES[@]}"
	do
		echo "$TIME"
		LOGFILE=erlangen"$SIZE1"_"$SIZE2".tr"$TIME".prism.log
		echo $LOGFILE
    	prism -s -gs -maxiters 1000000 -nossdetect erlangen.prism -const l_init=1,mu2=2,delta2=0.0007,size1="$SIZE1",size2="$SIZE2",alpha=48,beta=0.01,T="$TIME" erlangen.props -prop avail_tr >| $LOGDIR/$LOGFILE
		LOGFILE=erlangen"$SIZE1"_"$SIZE2".tr"$TIME".storm.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
	done
	
done

grep "States:" $LOGDIR/*prism*

grep "Time for model construction" $LOGDIR/*prism*
grep "Time for model checking" $LOGDIR/*prism*
grep "wallclock time" $LOGDIR/*storm*