Hi, all. I've read the paper Bridging the Gap Between Requirements and Model Analysis and want to run an example of fret-cocosim workflow but I dont know how to combine them. Like how can I use the exported zip file? Is there any interface on the front-end in cocosim to import? I would appreciate it if there is any tutorial.

I know my fretish has a problem with the use of 'after n time unit '. It seems not to work if "after n time unit" holds for many times within interval n , for RTGIL semantics of "after n time unit" requires !RES holds within n time unit. However, I do not understand the diagnosis since output variable C is always false. And is there any way to require RES to be true only after 2s? (At other time points, values of RES are non-deterministic)

fretish I wrote:

data types and id types of variables:

result of "diagnose":

Hello,Recently, I have been using FRET to describe some of the requirments, and I am facing some difficulties.The simple description is the following.When Compressor is started, the signal needs to stay off for a period of time and then enter the toggled state. The toggled state means that signal turns on and false alternates continuously.We can assume that compressor is the input and signal is the output. I want to ask if there is a description of this requirement.The following picture is the concrete description.The time can be any number.

Hello，I'm a student. I'm interested in the path generation template in FRET, but I haven't found it for a long time. Can you provide it? Finally, thank you very much for providing such good software as fret.

Hello , I am having problems with fret usage. I have installed the binaries of the NuSMV file in the environment variable, but in unbuntu 64-bit, FRET does not find NuSMV, causing SIMULATE to be unusable. I used the same method to be able to use under Windows installation.

Another problem is that when I use the Realizity function, related dependencies have been installed normally, but when I check, solver error occurs, I do not know how to solve it

hi，recently, we've been using your tools FRET, and we have some problems writing requirements,therefore we'd like to offer you some suggestions for improvement. 1.As for scope,sometimes we need to use the operation of the corresponding mode，such as when we want to describe a res happen in the intersection of mode1 and mode2 in FRET，we want to describe in FRET: in mode1&mode2 the system shall satisfy res.but in mode1&mode2 is a Syntax violation. 2.As for timing,sometimes we need a variable that represents a time constant.such as in mode1 the system shall for time1 satisfy res.Time1 is a variable.However,time1 is a Syntax violation. 3.As for simulation,sometimes we need to simulate two or more requirement.Such as requirement1:when signal1 the system shall always sastisfy res . Requirement2:when signal2 the system shall immediately satisfy res. We want to simulate the traces of signal1,signal2,res and two requirement.

Thank you for providing such excellent software.

Hi all,

I want to know if the meaning of 'at the next time point' is equivalent to 'at the next time unit', that is, equivalent to 'for 1 time unit'.

Thanks!

Hi all,

I'm experimenting with FRET, and running into trouble using the realizability checker. When I try to run the checker on a component, I only see "SOLVER ERROR," but no other output to help me diagnose the problem.

I think I've installed all the dependencies, but it's possible something is misconfigured.

Do you have any ideas for what I might try to narrow down the problem? That could be additional flags, debug print statements, etc.

On an Apple M1 machine I get the following error when trying to start the application:

App threw an error during load
Error: dlopen(/Users/thomasflinkow/Downloads/fret-2.3/fret-electron/app/node_modules/leveldown/build/Release/leveldown.node, 0x0001): tried: '/Users/thomasflinkow/Downloads/fret-2.3/fret-electron/app/node_modules/leveldown/build/Release/leveldown.node' (mach-o file, but is an incompatible architecture (have (x86_64), need (arm64e)))
    at process.func [as dlopen] (electron/js2c/asar_bundle.js:5:1812)
    at Object.Module._extensions..node (internal/modules/cjs/loader.js:1203:18)
    at Object.func [as .node] (electron/js2c/asar_bundle.js:5:1812)
    at Module.load (internal/modules/cjs/loader.js:992:32)
    at Module._load (internal/modules/cjs/loader.js:885:14)
    at Function.f._load (electron/js2c/asar_bundle.js:5:12633)
    at Module.require (internal/modules/cjs/loader.js:1032:19)
    at require (internal/modules/cjs/helpers.js:72:18)
    at load (/Users/thomasflinkow/Downloads/fret-2.3/fret-electron/app/node_modules/node-gyp-build/index.js:20:10)
    at Object.<anonymous> (/Users/thomasflinkow/Downloads/fret-2.3/fret-electron/app/node_modules/leveldown/binding.js:1:43)

I have attached the full output of running npm start -dd in file start.txt.

I have the required prerequisites installed:

thomasflinkow@Thomass-MacBook-Pro fret-2.3 % node --version
v16.16.0
thomasflinkow@Thomass-MacBook-Pro fret-2.3 % python --version
Python 3.10.6

and the installation seems to be successful too (attached is a file installation.txt containing the output of running npm run fret-install -dd).

I would appreciate any help in getting FRET to work on my machine and thank you in advance.

Please let me know if you need any other information.

Hello, I got some unexpected error when I was trying to run an install of this application. My node version is 10.15.0, npm version is 6.4.1. I have tried both "npm run fret-install" and "npm run fret-reinstall". But None of them works.

my Errol log and complete log are as follows [fret.log.txt](https://github.com/NASA-SW-Vn

fret.log.txt

2022-06-22T05_33_05_434Z-debug.log

Thanks

Hello, I try to use fret to describe the following requirements:

After the user presses the start button, the light flashing cycle begins, that is, the light L1 turns on and turns off after 1s; then the light L2 turns on and turns off after 1s; then the light L3 turns on and turns off after 1s; then the light L1 turns on... Keep going.

Here is one idea for my case:

• when start_btn the sys shall until stop_btn satisfy toggled_state=on.

• In toggled mode the sys shall after 1 seconds satisfy !L1.

• In toggled mode unless L1 the sys shall after 1 seconds satisfy !L2.

• In toggled mode unless L2 the sys shall after 1 seconds satisfy !L3.

• In toggled mode unless L3 the sys shall after 1 seconds satisfy !L1.

(the toggled mode is associate with the toggled_state variable; start_btn and stop_btn are inputs, and L1/2/3 are outputs)

But because of the semantic of unless, if L2 and L3 is false at the first point in toggled mode, the wrong behavior of toggled mode will be as follows:

I don’t know whether my understanding is wrong. Is there a valid description of this requirement ?

I would appreciate it if you could give me an answer.

I looked at the exported JSON file and I see that the status field is not present. I'd prefer to make the export feature more configurable with customizable fields to select in the export dialog. This would help the integration of FRET with other tools and also easy to filter requirements with approved status from those that are not.

When NuSMV is downloaded, the file in the folder bin is "NuSMV", so it fails to find "nusmv" after including that folder in the PATH variable. Another option could be to look for both NuSMV and nusmv.

Hi,

I'd like to be able to specify the variable mappings for a project/component to accompany the exported requirements, so that a user can import both & check realizability themselves without providing the mappings. However, I can't quite figure out how to use the 'Import' feature in the 'Variable Mapping' pane of the Analysis Portal.

Thanks!

Hi all,

I'm wondering if anyone has any ideas for how to effectively tackle the following problem. I have a system with several instances of a single type of subcomponent. If a single instance has, say, N requirements, then that means if I have C copies, I need to produce N*C requirements (almost identical, but changing some identifiers here and there, like X1, ...,XN.

(You can imagine a system with N identical sensor units that all feed in to a single 'logic' subcomponent that makes some kind of decision based on these sensor values -- in this case you really need to talk about each sensor unit)

I'm wondering if anyone can suggest a way that I might avoid so much repetition in providing the requirements, especially given that if changes are discovered later, they will have to be propagated to each near-duplicate requirement.

As an example, one idea is to simplify give requirements for each type of component only (in the example above, just give the Nrequirements for a sensor unit, plus for a logic subcomponent with C inputs) . I think this would work, but then checking realizability wouldn't be checking the realizability of the composition of the C sensors and so on.

I think the problem wouldn't be so much of an issue if there were an easy way to use a standard text editor to produce the requirements. I think the CSV format is close to this, but it seems importing the frettish sentences wraps them in quotes (e.g. as "FSM shall always Foo"), which means they don't get semantics generated for them.

Thanks!

1. Comment out notice and disclaime;
2. Add error message to fopen(), because sometimes it failed to create the file in my Ubuntu OS and Matlab gave me inaccurate error message.