Sorry for the delay.

Something broke!

My plan to evaluate this was to update the contracts in the "Full Security Example" https://code.sei.cmu.edu/bitbucket/projects/ETMAC/repos/security/browse/Full_Security_Example to use the new operator. But the baseline test fails.

1. Instantiate Secure_System::TheSystem.Impl
2. Execute the verification plans on it

When I do this on the main branch, the verification is successful. When I do this on the branch for change, it fails:

Global variables:
info0
error0
to_java
/Users/aarong/eclipses/osate2_2023-12-master-etmac/ws/.metadata/.plugins/org.eclipse.pde.core/.install_folders/1706124045002/../../../../../../../../.p2/pool/plugins/org.eclipse.ease.lang.python.py4j_0.9.0.I202206141122/pysrc/ease_py4j_main.py:414: DeprecationWarning: setDaemon() is deprecated, set the daemon attribute instead
thread.setDaemon(True)
org.eclipse.ease.ScriptExecutionException: Traceback (most recent call last):
File "/Library/Frameworks/Python.framework/Versions/3.10/lib/python3.10/ast.py", line 50, in parse
return compile(source, filename, mode, flags,
File "", line 120
compLevels = { s:Int('Subject' + str(s)) for s in }

compLevels is from BLContract.aadl:

				# Level for each component
				compLevels = { s:Int('Subject' + str(s)) for s in ${systems$} }

The problem is that ${systems$} is empty for some reason. It is defined by

				val rootSystemsToCheck = root.subcomponents.map {
					ci -> (ci, ci#VerificationProperties::CheckBellLaPadula)
				}.filterTupleElementsPresent.filter {
					(ci, checkBLP) -> checkBLP
				}.map { (ci, x) -> ci };
				
				val systems = rootSystemsToCheck.flatMap {
					ci -> ci.subcomponents.filter {
						s -> s.isSystem
					}
				};

I think maybe you broke flatMap somehow?