Howdy all,
I know that the solver is still in the Labs category. I find the solver tool to be great for exploring a specification’s behavior. I’d like to ask that its functionality be expanded. Currently, the Syside 1.0.0 Beta 1 doesn’t advertise any expanded functionality. I’d use this tool a lot more if it had more capability.
I’ve included sample source. I’m as sure as I can be that this input is correct, but as always, I may have made a user error. Apologies in advance if that is true.
My setup:
- Windows 10
- syside-solver 0.10.3
First observation (error?), the invocation
CMD> syside solver check -i
can only handle one input file at a time and does not have the ability to take a list of files as input. To import a local package, you must create a single combined file to use as input. There may be a way to use other tools in the environment, but I haven’t seen any hints on how to do this. Please redirect me if I’ve missed the reference.
My input file is a combination of two packages, DataUnits and Communication_System which I’ve named combo.sysml.
package DataUnits {
doc /* Package to hold the bits per second definitions and RPM definition */
private import ScalarValues::*;
private import ISQ::*;
private import SI::*;
attribute def BitRateValue :> ISQ::FrequencyValue;
attribute bps = SI::Hz;
attribute Kbps : ISQ::FrequencyUnit = 1e3 * bps;
attribute Mbps : ISQ::FrequencyUnit = 1e6 * bps;
// RPM: revolutions per minute
attribute RPM : ISQ::FrequencyUnit = (1.0/60.0) * SI::Hz;
}
package Communication_System {
doc /* Communication channels split by control and data functions. */
private import ScalarValues::*;
private import DataUnits::*;
// ==========================================
// 1. Math / Verification Constraint Definitions
// ==========================================
constraint def MaxBandwidthCheck {
in rateA : BitRateValue;
in rateB : BitRateValue;
in limit : BitRateValue;
// Logical expression that must hold true during simulation/verification
rateA + rateB <= limit
}
// ==========================================
// 2. Behavioral / Action Sequence Definitions
// ==========================================
action def ProcessPacket {
doc /* Corrected behavioral sequence matching the normative OMG control node grammar. */
// 1. Declare all action step usages and control nodes exactly once
action receivePacket;
action decryptHeader;
action validateChecksum {
out isChecksumValid : ScalarValues::Boolean;
}
// Declare the decision control node as an explicit step in the action body
decide evaluateChecksum;
action extractCommand;
action executeInstruction;
action logChecksumError;
action discardPacket;
// ==========================================================
// 2. Linear Flow routing directly into the declared control node
// ==========================================================
succession first receivePacket
then decryptHeader;
succession first decryptHeader
then validateChecksum;
succession first validateChecksum
then evaluateChecksum; // Feeds the timeline sequence directly into the decision node
// ==========================================================
// 3. Conditional Pathways branching out from the node
// ==========================================================
first evaluateChecksum if validateChecksum.isChecksumValid
then extractCommand;
first evaluateChecksum if not validateChecksum.isChecksumValid
then logChecksumError;
// ==========================================================
// 4. Downstream linear execution strings for both pathways
// ==========================================================
succession first extractCommand
then executeInstruction;
succession first executeInstruction
then done;
succession first logChecksumError
then discardPacket;
succession first discardPacket
then done;
}
// ==========================================
// System Architecture Configurations
// ==========================================
part def CommSuite {
doc /* Integrated suite validating total combined system bandwidth. */
part controlLink : ControlLink;
part dataPayloadLink : DataPayloadLink;
// Maximum safety margin allocated to the entire avionics bay
attribute maxSystemLimit : BitRateValue = 200.0 [Mbps];
// Structural Connection
connect controlLink.syncPort to dataPayloadLink.triggerPort;
// Constraint Instantiation: Binds system properties directly to verification inputs
assert constraint bandwidthVerification : MaxBandwidthCheck {
in rateA = controlLink.dataRate;
in rateB = dataPayloadLink.dataRate;
in limit = maxSystemLimit;
}
}
// ==========================================
// Subsystem Components
// ==========================================
part def ControlLink {
attribute frequency : ISQ::FrequencyValue = 2.4e9 [SI::Hz];
attribute dataRate : BitRateValue = 115.2 [Kbps];
attribute encryptionEnabled : Boolean = true;
port rfInterface : Base_Interfaces::RF_Port;
port syncPort : Base_Interfaces::Digital_Port;
// Subsystem Hardware running the concrete behavioral loop
item commandProcessor : Hardware::MCU {
// Evaluates/runs our packet pipeline sequentially
action processIncomingTelemetry : ProcessPacket;
}
item transceiver : Hardware::RF_Transceiver;
}
part def DataPayloadLink {
attribute frequency : ISQ::FrequencyValue = 8.1e9 [SI::Hz];
attribute dataRate : BitRateValue = 150.0 [Mbps];
attribute compressionRatio : Integer = 4;
port opticalInterface : Base_Interfaces::Optical_Port;
port triggerPort : Base_Interfaces::Digital_Port;
item highSpeedStorage : Hardware::NVMe_Drive;
item payloadModem : Hardware::FPGA_Modem;
}
// ==========================================
// Supporting Domain Placeholders
// ==========================================
package Base_Interfaces {
port def RF_Port;
port def Digital_Port;
port def Optical_Port;
}
package Hardware {
item def MCU;
item def RF_Transceiver;
item def NVMe_Drive;
item def FPGA_Modem;
}
}
The invocation of solver on this combo.sysml file results in:
CMD> syside solver check -i combo.sysml
{
"error": {
"code": "Load",
"span": null,
"message": "the model uses a construct this analysis does not support: assertion \"Communication_System::CommSuite::bandwidthVerification\" has no predicate"
},
"exit_code": 2
}
Here is output that leads me to believe that it may
- May not yet be capable of function evaluation (99.9% this is the real issue)
- Have a scoping issue
- Have an indirection issue
Although I’d expect the function call to MaxBandwidthCheck would be followed for the computation to be evaluated:
constraint def MaxBandwidthCheck {
in rateA : BitRateValue;
in rateB : BitRateValue;
in limit : BitRateValue;
// Logical expression that must hold true during simulation/verification
rateA + rateB <= limit
}
Thanks for all your hard work!
V/r, @Richard_Wallace
