#!/bin/sh

awk '
$2=="states," && $3=="stored" 	{	stored = $1	}
$4=="depth"	{	depth = $6	}
$2=="transitions"	{	trans = $1	}
$4=="memory" || $2=="memory"	{	mem = $1	}
$1=="State-vector"&&$3=="byte,"	{	sv = $2 }
$2=="too"&&$3=="big"	{ fail = 1 }
$2=="elapsed"	{ tm = $4 }
$2=="rate"	{ rt = $3 }
END	{
		if (fail) {
			printf("failed\n")
		} else {
			printf("D= %6d\tS= %8d\tT= %8d\tM= %s\tSV= %s\tt=%s\tR=%s\n",
				depth, stored, trans, mem, sv, tm, rt)
		}
}'