mCRL2
mCRL2 copied to clipboard
mCRL2org
Include statement
Issue migrated from trac ticket # 751
component: General | priority: minor
2010-06-29 10:19:08: [email protected] created the issue
'nuff said, probably. Simple include functionality would greatly help a lot of people.
- Include statement can be used in any mCRL2 native file, such as mCRL2 files, LPS files, µ-calculus formulae and PBES files.
- Inclusion respects some environment variable MCRL2_INCLUDE_PATH that defines which additional paths are scanned. When set to
~/.mcrl2/include:/usr/share/mcrl2/include, then mCRL2 scans, the current directory first, then~/.mcrl2/include, and then/usr/share/mcrl2/include. - The -v switch should cause the parser to print the full paths of the included files.
- Circular references should not be allowed.
-Proposed syntax:*
Current directory contains bitvector.mcrl2 and bitvector.bak.
include("bitvector")
includes "bitvector.mcrl2"
include("bitvector.mcrl2")
includes "bitvector.mcrl2"
include("bitvector.bak")
includes "bitvector.bak"
2010-06-29 11:26:20: @jkeiren commented
The idea seems like a large improvement in usability to me. One topic that will at least need to be addressed is the way in which an environment is considered for platforms other than Linux (especially Windows).
2010-06-29 14:43:52: @twillems commented
I concur. The usability would definitely improve.
Would you advocate creating monolithic LPS files from modular process specifications, or advocate modular LPS files as well, with include directives for data specification only?