Bug #678

Mcrl tests fail in testsuite

Added by Alfons Laarman over 7 years ago. Updated over 6 years ago.

Status:NewStart date:23 Nov 2012
Priority:NormalDue date:
Assignee:Jeroen Meijer% Done:

0%

Category:testingSpent time:-
Target version:ltsmin-2.1

Description

Must be some TCL string escape weirdness

starting /home/fmg/laarman/ltsmin-hre/testsuite/../src/pins2lts-mc/lpo2lts-mc -z6 --strategy=dfs --state=tree --procs=5 /home/fmg/laarman/ltsmin-hre/testsuite/../examples/hef_wrong.tbf
spawn /home/fmg/laarman/ltsmin-hre/testsuite/../src/pins2lts-mc/lpo2lts-mc -z6 --strategy=dfs --state=tree --procs=5 /home/fmg/laarman/ltsmin-hre/testsuite/../examples/hef_wrong.tbf^M
gmake2: * [all] Broken pipe^M
gmake2: *
[all] Broken pipe^M
MCRL grey box: File /tmp/gmake2: Entering directory `/home/fmg/laarman/ltsmin-hre/testsuite/alg_backends_lpo'.c cannot be opened^M

History

#1 Updated by Alfons Laarman over 7 years ago

  • Category set to testing
  • Assignee set to Alfons Laarman
  • Target version set to ltsmin-2.0

#2 Updated by Alfons Laarman over 7 years ago

  • Target version changed from ltsmin-2.0 to ltsmin-2.1

disabled Mcrl tests in test suite

Mcrl seems to parse the filename oncorrectly when called from tcl:
MCRL grey box: File /tmp/gmake2: Entering directory `/home/fmg/laarman/ltsmin-hre/testsuite/lang_frontends'.c cannot be opened^M

(from testrun.log)

#3 Updated by Alfons Laarman over 6 years ago

  • Assignee changed from Alfons Laarman to Jeroen Meijer

Also available in: Atom PDF