Ciao amici,

ho un file di testo contenente l'elaborazione di circa un migliaio di files scritti in linguaggio Lustre; questi file sono elaborati da dei tools, ne uso 3 e ognuno di essi mi scrive il responso della sua elaborazione nel file di testo, sotto il nome del file Lustre elaborato:

++ ***** FIREFLY_5_e1_2552_e7_1169.lus *****
cannot prove the invariant _OK_ = 1 IN main_call_top is true or false : the induction failed

KIND KILLED
LUKE KILLED


++ ***** FIREFLY_5_e2_2229.lus *****
invariant _OK_ = 1 IN main_call_top is true


+++ 2 step is Valid.

LUKE KILLED


++ ***** FIREFLY_5_e2_2884_e1_2678.lus *****
invariant _OK_ = 1 IN main_call_top is true


+++ 2 step is Valid.

LUKE KILLED
Il file preso in considerazione è racchiuso tra asterischi, con i ++ davanti.
Sotto ho il responso del primo tool.
GLi altri 2 possono metterci troppo tempo, nel qual caso li interrompo. Si chiamano Kind e Luke.

Premesso che il primo dei tre tools (NuSMV) riesce sempre a dare un responso, io dovrei selezionare tutti quei nomi di file per i quali o Luke o Kind sono stati interrotti. Per poi riprocessarli un'altra volta con dei timeout più lunghi!

So che AWK lavora riga per riga, quindi non so se si possa fare una cosa del genere!