After I performed the operation of Import project FSM by selecting the down arrow on the left and navigating to fret/caseStudies/FiniteStateMachine/FSM_reqts_and_vars.json, I cannot find the FSM project in the Projects pull-down menu at this step.

[zarrorapier]

The errors are as follows:
:14
(Use electron --trace-warnings ... to show where the warning was created)
(node:908446) UnhandledPromiseRejectionWarning: Unhandled promise rejection. This error originated either by throwing inside of an async function without a catch block, or by rejecting a promise which was not handled with .catch(). To terminate the node process on unhandled promise rejection, use the CLI flag --unhandled-rejections=strict (see https://nodejs.org/api/cli.html#cli_unhandled_rejections_mode). (rejection id: 7)
Warning: terminator_CreateInstance: Failed to CreateInstance in ICD 0. Skipping ICD.
^C/home/FRET/fret/fret-electron/node_modules/electron/dist/electron exited with signal SIGINT

[andreaskatis]

Hi @zarrorapier ,

Thank you for trying out FRET and posting this issue. For us to look into this we need more information on your end. Please let us know:

• The operating system that you are running FRET in, including its exact version (e.g. Ubuntu 20.04.6 LTS, macOS Sequoia, etc.);
• The version of NodeJS that you are running FRET with (Run node -v in a terminal);
• The Python 3 version that you installed FRET with (if you used whatever is installed on your machine, running python3 --version in your terminal should suffice).

Best,

Andreas

[zarrorapier]

Dr. Katis

Thank you for your reply. I have identified the cause of the issue: the folders fret-db and model-db could not be found. The problem was resolved after I created these folders manually using the following commands:
mkdir -p /home/Documents/fret-db
mkdir -p /home/Documents/model-db

I have another question to consult you. I noticed that in the paper The Ten Lockheed Martin Cyber-Physical Challenges: Formalized, Analyzed, and Explained, it is mentioned:

"As mentioned, we were not able to formalize requirement [TUI-004] that contains a temporal condition.
[TUI-004] Natural Language: After 10 seconds of computation at an execution frequency of 10 Hz, the output should equal 10 within a +/-0.1 tolerance, for a constant input (xin = 1.0) and the sample delta time TT = 0.1 seconds when in normal mode of operation.
This requirement could not be expressed directly in FRETISH. The 'After 10 seconds of computation at an execution frequency of 10 Hz' part of the requirement constitutes a condition that must persist for a time duration (10 seconds). Such conditions are not yet supported in FRETISH."

I would like to ask: Has this issue been resolved now? Specifically, can FRET support requirements like this: "When the yaw rate > MAX_YAW_RATE_UPPER (0.25 rad/s) for more than 10 seconds, the system state transitions from 'active' to 'passive'"?

Additionally, is it possible to generate Simulink models in .slx format using the JSON files exported from FRET requirements? My goal is to use FRET to automatically generate executable Stateflow state machine models (for state transitions between states such as "passive", "standby", and "active" based on the types of signals I mentioned earlier). The algorithm part will be written manually; I only want to use FRET to generate the .slx state machine model itself. Please let me know if this is achievable, as I am very eager to implement the automated generation of executable state machine models using FRET.

Thank you so much for your time and replies.

your sincerely

zarro

[andreaskatis]

Hi @zarrorapier ,

Thank you for your reply. I have identified the cause of the issue: the folders fret-db and model-db could not be found. The problem was resolved after I created these folders manually using the following commands:
mkdir -p /home/Documents/fret-db
mkdir -p /home/Documents/model-db

While it's good that you were able to identify the issue, it's still strange that the folders were not there in the first place. Normally, the folders would be created during the importing process. Did the Documents folder exist prior to your attempt at importing? If no (which is hinted by the fact that you used mkdir -p), this is the actual reason and it can happen if the folder was deleted by the user in the past, or when a WSL installation of FRET is used (that's why we explicitly require users to create the Documents folder in the WSL guide). On the other hand, if the Documents folder was there before you encountered your issue, we may need to look further into this to figure out why the folders were not created.

I would like to ask: Has this issue been resolved now? Specifically, can FRET support requirements like this: "When the yaw rate > MAX_YAW_RATE_UPPER (0.25 rad/s) for more than 10 seconds, the system state transitions from 'active' to 'passive'"?

I believe what you would like to express can be done using the persisted/persists temporal conditions. See Temporal Condition Documentation for further details. For example, one way to express your specific example in FRETish would be the following:

Whenever persisted(10, yaw_rate > MAX_YAW_RATE) & state_active the system shall at the next timepoint satisfy state_passive.

Please note there might be variations that fit your case better (e.g. using "Upon" instead of "Whenever" for the condition field).

Additionally, is it possible to generate Simulink models in .slx format using the JSON files exported from FRET requirements? My goal is to use FRET to automatically generate executable Stateflow state machine models (for state transitions between states such as "passive", "standby", and "active" based on the types of signals I mentioned earlier). The algorithm part will be written manually; I only want to use FRET to generate the .slx state machine model itself. Please let me know if this is achievable, as I am very eager to implement the automated generation of executable state machine models using FRET.

While FRET does not currently have such a feature, I think that the JSON file you get from exporting a FRET project could be used towards your goal, as it contains a lot of information you would need to write a MATLAB script that creates a Stateflow model. The main challenge would be on ensuring that the intended semantics are preserved in the generated models. If you are still interested in looking deeper, I would suggest starting with a small example (like the one above) and use the generated JSON file as a guide to write the MATLAB script that would generate a Stateflow representation of the transition.

Note: Consider exporting both requirements and variables as part of this process. In order to do this you would need to use the Variable Mapping tab in the Analysis Portal to assign data types to the variables involved in the project. The exported JSON file will then contain this information under the variables property (it typically is added after the "requirements" property, towards the end of the file).

If you have any further questions/developments on this, feel free to create a thread in our Discussions page, or send us an e-mail.

Best,

Andreas