models="car_fm.xml aircraft_fm.xml movies_app_fm.xml REAL-FM-12.xml stack_fm.xml Graph-product-line-fm.xml connector_fm.xml fame_dbms_fm.xml Apl.m TightVNC.m smart_home_fm.xml Gg4.m arcade_game_pl_fm.xml Berkeley.m Violet.m Eshop-fm.xml ecos-icse11.dimacs freebsd-icse11.dimacs 2.6.28.6-icse11.dimacs"

models[1]="car_fm.xml aircraft_fm.xml movies_app_fm.xml REAL-FM-12.xml stack_fm.xml Graph-product-line-fm.xml connector_fm.xml fame_dbms_fm.xml Apl.m TightVNC.m smart_home_fm.xml Gg4.m arcade_game_pl_fm.xml Berkeley.m Violet.m Eshop-fm.xml ecos-icse11.dimacs"
models[2]="car_fm.xml aircraft_fm.xml movies_app_fm.xml REAL-FM-12.xml stack_fm.xml Graph-product-line-fm.xml connector_fm.xml fame_dbms_fm.xml Apl.m TightVNC.m smart_home_fm.xml Gg4.m arcade_game_pl_fm.xml Berkeley.m Violet.m Eshop-fm.xml"
models[3]="car_fm.xml aircraft_fm.xml movies_app_fm.xml REAL-FM-12.xml stack_fm.xml Graph-product-line-fm.xml connector_fm.xml fame_dbms_fm.xml Apl.m TightVNC.m smart_home_fm.xml Gg4.m arcade_game_pl_fm.xml Berkeley.m Violet.m"
models[4]="car_fm.xml aircraft_fm.xml movies_app_fm.xml REAL-FM-12.xml stack_fm.xml Graph-product-line-fm.xml connector_fm.xml fame_dbms_fm.xml Apl.m TightVNC.m smart_home_fm.xml Gg4.m"

SPLCATool="java -jar SPLCATool-v0.2-MODELS2011.jar"

for fm in $models; do
	echo $fm
	$SPLCATool -t sat_time -fm $fm | grep "Features"
	$SPLCATool -t sat_time -fm $fm | grep "Constraints"
done

for fm in $models; do
	echo $fm
	$SPLCATool -t sat_time -fm $fm | grep "SAT done"
done

for fm in $models[3]; do
	echo $fm
	$SPLCATool -t count_solutions -fm $fm | grep Solutions
done

for t in 1 2 3 4; do
	for fm in $models[t]; do
		echo $fm, t=$t
		$SPLCATool -t t_wise -fm $fm -s $t | grep Done
		$SPLCATool -t verify_solutions -fm $fm -check $fm.ca${t}.csv | grep Reason
		$SPLCATool -t calc_cov -fm $fm -s $t -ca $fm.ca${t}.csv | grep Coverage
	done
done
