nasa-sw-vnv/fret

A framework for the elicitation, specification, formalization and understanding of requirements.

fret's Issues

Suggestions

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.

How to understand the result of diagnose?

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":

Electron GPU initialization fails on Ubuntu 22.04

This seems to be a common issue with electron-builder: Automattic/simplenote-electron#3096. The error message I see is the same as listed in that issue.

I have been able to work around the problem by adding --no-sandbox to the electron invocation made by npm start.

Templates Lack Syntax Highlighting and Structure Uneditable

We've just started looking at the templates, which seem quite useful and are (helpfully) extendible too.

But if I use a template to build a requirement, it has no syntax highlighting, which makes it hard for me to parse the requirement.

Also, after saving the requirement and coming back to it, it is still 'a template' so it is uneditable (e.g. I cannot change the if..then.. structure of Change State's response). I'm in two minds about if they should be editable, after saving (i.e. once saved it becomes a normal requirement) but I sort of expected it to become a 'normal' text requirement after it was saved.

Bug: All Caps "Immediately" keyword causes blank screen

If I type IMMEDIATELY as the timing keyword (as opposed to "immediately") I get a blank screen and a bunch of TypeErrors if the dev log is running.

I found this while using Mu-FRET, but tested it in FRET (in a version pulled today from the FRET repo).

The brief original issue is in our Mu-FRET repo: valu3s-mu#25 but the error doesn't depend on it being a new requirement like I though initially.

Steps

1. In the Edit Requirement dialogue add/edit the fretish text to include the timing keyword "IMMEDIATELY" (in all caps)
2. Press "Semantics"
3. See the blank screen.

Error on Install: regex.h no such file or directory

Hello,

When trying to install fret, I receive errors that appear to be due to gcc not being able to find the regex.h file.

I am running:

• Windows 10
• Node 16.14.1
• NPM 9.3.1
• NuSMV 2.6.0
• GNU Make 4.3
• gcc 12.2.0

When running npm run fret-install I receive the following error (full log here)

$ npm run fret-install



> [email protected] fret-install
> npm --prefix ../tools/LTLSIM/ltlsim-core install ../tools/LTLSIM/ltlsim-core && npm install

npm ERR! code ENOENT
npm ERR! syscall open
npm ERR! path C:\Users\jweidoka\fret\tools\LTLSIM\ltlsim-core\node_modules\tools\LTLSIM\ltlsim-core/package.json
npm ERR! errno -4058
npm ERR! enoent ENOENT: no such file or directory, open 'C:\Users\jweidoka\fret\tools\LTLSIM\ltlsim-core\node_modules\tools\LTLSIM\ltlsim-core\package.json'
npm ERR! enoent This is related to npm not being able to find a file.
npm ERR! enoent

npm ERR! A complete log of this run can be found in:
npm ERR!     C:\Users\jweidoka\AppData\Local\npm-cache\_logs\2023-02-02T20_30_11_021Z-debug-0.log

To try to get to the root of this, I did an npm install inside of the fret/tools/LTLSIM/ltlsim-core directory and got the following error (full log here)

MINGW64 ~/fret/tools/LTLSIM/ltlsim-core (master)
$ npm install

> [email protected] install
> make -C "./simulator" && make -C "./simulator" clean

make: Entering directory 'C:/Users/jweidoka/fret/tools/LTLSIM/ltlsim-core/simulator'
gcc -c -o ltlsim_commands.o ltlsim_commands.c -I. -g -Wall -DWINDOWS
In file included from ltlsim_commands.c:1:
ltlsim_commands.h:10:10: fatal error: regex.h: No such file or directory
   10 | #include <regex.h>
      |          ^~~~~~~~~
compilation terminated.
make: *** [Makefile:25: ltlsim_commands.o] Error 1
make: Leaving directory 'C:/Users/jweidoka/fret/tools/LTLSIM/ltlsim-core/simulator'
npm ERR! code 2
npm ERR! path C:\Users\jweidoka\fret\tools\LTLSIM\ltlsim-core
npm ERR! command failed
npm ERR! command C:\WINDOWS\system32\cmd.exe /d /s /c make -C "./simulator" && make -C "./simulator" clean

npm ERR! A complete log of this run can be found in:
npm ERR!     C:\Users\jweidoka\AppData\Local\npm-cache\_logs\2023-02-02T20_32_08_586Z-debug-0.log

I am not very familiar with compiling C code, is there something else I need to install to make the regex.h file available? Or would this be caused by something else?

Any help you can provide is greatly appreciated!

Repeated Requirements

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!

Unsuccessful Installation

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

Verification Problem?

Hello, @anmavrid
If some mode variables are not involved in the model, will it cause problems for verification?

could not install fret

Dear,

I install fret under ubuntu 20.04, node version is 16.11.0, npm version is 8.0.0, nusmv version is 2.6.0, I follow the instruction but get errors as following:
npm ERR! code 1
npm ERR! path /home/cocosim/fret/fret-electron/node_modules/electron
npm ERR! command failed
npm ERR! command sh -c node install.js
npm ERR! RequestError: connect ECONNREFUSED 223.75.236.241:443
npm ERR! at ClientRequest. (/home/cocosim/fret/fret-electron/node_modules/got/source/request-as-event-emitter.js:178:14)
npm ERR! at Object.onceWrapper (node:events:510:26)
npm ERR! at ClientRequest.emit (node:events:402:35)
npm ERR! at ClientRequest.origin.emit (/home/cocosim/fret/fret-electron/node_modules/@szmarczak/http-timer/source/index.js:37:11)
npm ERR! at TLSSocket.socketErrorListener (node:_http_client:447:9)
npm ERR! at TLSSocket.emit (node:events:390:28)
npm ERR! at emitErrorNT (node:internal/streams/destroy:157:8)
npm ERR! at emitErrorCloseNT (node:internal/streams/destroy:122:3)
npm ERR! at processTicksAndRejections (node:internal/process/task_queues:83:21)

npm ERR! A complete log of this run can be found in:
npm ERR! /home/cocosim/.npm/_logs/2023-01-12T02_51_02_716Z-debug.log

the path generation

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.

Unable to run executable built with Docker on Ubuntu 22.04

Hi,
I am having trouble with installing FRET on Ubuntu desktop (both 22.04 and 23.10).

If I try to install it with the node method (using node 16.16)

Here are the steps to install and start FRET:

1. cd fret-electron
2. npm run fret-install (please do 'npm run fret-reinstall' instead if you already have a FRET installation)
3. npm start

It does work, but if I try to use the docker method, it generates the executable successfully, but when I try to run it this error shows:

A JavaScript error occurred in the main process
Uncaught Exception:
Error: Cannot find module "../../analysis/connected_components"
    at /home/user/Desktop/fret-desktop/FRET-linux-x64/resources/app/main.prod.js:1:1546319
    at Object../model/realizabilitySupport/realizabilityUtils.js (/home/user/Desktop/fret-desktop/FRET-linux-x64/resources/app/main.prod.js:1:1546423)
    at t (/home/user/Desktop/fret-desktop/FRET-linux-x64/resources/app/main.prod.js:1:124)
    at Object../model/FretModel.js (/home/user/Desktop/fret-desktop/FRET-linux-x64/resources/app/main.prod.js:1:1508006)
    at t (/home/user/Desktop/fret-desktop/FRET-linux-x64/resources/app/main.prod.js:1:124)
    at Object../app/main.dev.js (/home/user/Desktop/fret-desktop/FRET-linux-x64/resources/app/main.prod.js:1:692)
    at t (/home/user/Desktop/fret-desktop/FRET-linux-x64/resources/app/main.prod.js:1:124)
    at module.exports../app/main.dev.js (/home/user/Desktop/fret-desktop/FRET-linux-x64/resources/app/main.prod.js:1:472)
    at Object.<anonymous> (/home/user/Desktop/fret-desktop/FRET-linux-x64/resources/app/main.prod.js:1:499)
    at Module._compile (internal/modules/cjs/loader.js:1152:30)

Description of Flashing Light

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.

Realizability GUI issue

  Hello, the GUI of FRET on my centos become a white screen after I click the REALIZABILITY and nothing is outputed on the  terminal. Could you tell me what happen? Thanks.

Originally posted by @kaci2002 in #28 (comment)

Trailing bit of requirement after a colon

Hi

If I have a variable name with a colon ":" in it (in this case the variable was a ratio) FRET will save it ok and say that it's fomalised, but checking the Temporal Logic output shows that anything after the colon is lost.

The only hint to this in FRET is that the text after the colon is not highlighted, but that's a very subtle hint that it's ignoring the remainder of the requirement. It would be nice if this still showed in the UI as an error.

How to combine fret and cocosim to a fret-cocosim workflow?

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.

Solver Error in Realizability Checking

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.

Unsuccessful installation of NuSMV path and the use of realizity use

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

Description of complex requirements

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.

I get this error when I run npm start

Discussed in #74

^{Originally posted by EliasH-NMBU February 7, 2024}
[67656:0207/142004.066829:ERROR:gl_surface_presentation_helper.cc(260)] GetVSyncParametersIfAvailable() failed for 1 times!

Does anyone know why this error happens or how to fix it?

Search Bar Doesn't Respond to Enter Key

Hi,

I really like the new search bar, but for me it doesn't respond to the Enter key to search. Instead, I have to click the magnifying glass icon. This is a minor inconvenience but happens a lot!

This happens with v3.0, running on Ubuntu 20.04.6

Error "incompatible architecture (have (x86_64), need (arm64e))" trying to start FRET on an M1 machine

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.

Broken link in docs

The 7th link Using the simulator in the user manual is broken -- https://github.com/NASA-SW-VnV/fret/blob/v2.0/fret-electron/docs/_media/userManual.md

It should probably be pointing to https://github.com/NASA-SW-VnV/fret/blob/v2.0/fret-electron/docs/_media/UsingTheSimulator/ltlsim.md

Difference between 'at the next time point' and 'for 1 time unit'

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!

Installation on Mac M1 Monterey throwing webpack/native dependency errors

Hi,

I am having trouble installing FRET on my M1 Mac. When running npm run fret-install, there seems to be a webpack issue that prohibits the dependencies from being installed. Below is the full error message generated.

npm run fret-install 

> [email protected] fret-install
> npm --prefix ../tools/LTLSIM/ltlsim-core install ../tools/LTLSIM/ltlsim-core && npm install


> [email protected] install
> make -C "./simulator" && make -C "./simulator" clean

gcc -c -o ltlsim_commands.o ltlsim_commands.c -I. -g -Wall
gcc -c -o ltlsim_smvutils.o ltlsim_smvutils.c -I. -g -Wall
In file included from ltlsim_smvutils.c:2:
./ltlsim_smvutils_private.h:85:13: warning: unused function '_prepFormula' [-Wunused-function]
static void _prepFormula(char *f_expr, const char *expr);
            ^
1 warning generated.
gcc -c -o ltlsim_types.o ltlsim_types.c -I. -g -Wall
gcc ltlsim.c ltlsim_commands.o ltlsim_smvutils.o ltlsim_types.o -o ltlsim -I. -g -Wall
rm -f *.o

up to date, audited 11 packages in 506ms

found 0 vulnerabilities
npm WARN deprecated @types/[email protected]: This is a stub types definition. puppeteer provides its own type definitions, so you do not need this installed.
npm WARN deprecated [email protected]: See https://github.com/lydell/source-map-url#deprecated
npm WARN deprecated [email protected]: flatten is deprecated in favor of utility frameworks such as lodash.
npm WARN deprecated [email protected]: request-promise-native has been deprecated because it extends the now deprecated request package, see https://github.com/request/request/issues/3142
npm WARN deprecated [email protected]: Please see https://github.com/lydell/urix#deprecated
npm WARN deprecated [email protected]: Use String.prototype.trim() instead
npm WARN deprecated [email protected]: this library is no longer supported
npm WARN deprecated [email protected]: https://github.com/lydell/resolve-url#deprecated
npm WARN deprecated [email protected]: This is probably built in to whatever tool you're using. If you still need it... idk
npm WARN deprecated [email protected]: Browserslist 2 could fail on reading Browserslist >3.0 config used in other tools.
npm WARN deprecated [email protected]: Browserslist 2 could fail on reading Browserslist >3.0 config used in other tools.
npm WARN deprecated [email protected]: Browserslist 2 could fail on reading Browserslist >3.0 config used in other tools.
npm WARN deprecated [email protected]: Browserslist 2 could fail on reading Browserslist >3.0 config used in other tools.
npm WARN deprecated [email protected]: Browserslist 2 could fail on reading Browserslist >3.0 config used in other tools.
npm WARN deprecated [email protected]: See https://github.com/lydell/source-map-resolve#deprecated
npm WARN deprecated [email protected]: use String.prototype.padStart()
npm WARN deprecated [email protected]: Browserslist 2 could fail on reading Browserslist >3.0 config used in other tools.
npm WARN deprecated [email protected]: Use your platform's native performance.now() and performance.timeOrigin.
npm WARN deprecated [email protected]: CircularJSON is in maintenance only, flatted is its successor.
npm WARN deprecated [email protected]: some dependency vulnerabilities fixed, support for node < 10 dropped, and newer ECMAScript syntax/features added
npm WARN deprecated [email protected]: The v1 package contains DANGEROUS / INSECURE binaries. Upgrade to safe fsevents v2
npm WARN deprecated [email protected]: Chokidar 2 does not receive security updates since 2019. Upgrade to chokidar 3 with 15x fewer dependencies
npm WARN deprecated [email protected]: The v1 package contains DANGEROUS / INSECURE binaries. Upgrade to safe fsevents v2
npm WARN deprecated [email protected]: Chokidar 2 does not receive security updates since 2019. Upgrade to chokidar 3 with 15x fewer dependencies
npm WARN deprecated [email protected]: The v1 package contains DANGEROUS / INSECURE binaries. Upgrade to safe fsevents v2
npm WARN deprecated [email protected]: The querystring API is considered Legacy. new code should use the URLSearchParams API instead.
npm WARN deprecated [email protected]: This package has been deprecated in favour of @sinonjs/samsam
npm WARN deprecated [email protected]: Deprecated. Please use https://github.com/webpack-contrib/mini-css-extract-plugin
npm WARN deprecated [email protected]: Please upgrade  to version 7 or higher.  Older versions may use Math.random() in certain circumstances, which is known to be problematic.  See https://v8.dev/blog/math-random for details.
npm WARN deprecated [email protected]: babel-eslint is now @babel/eslint-parser. This package will no longer receive updates.
npm WARN deprecated [email protected]: Use uuid module instead
npm WARN deprecated [email protected]: request has been deprecated, see https://github.com/request/request/issues/3142
npm WARN deprecated [email protected]: Please use @electron/osx-sign moving forward. Be aware the API is slightly different
npm WARN deprecated @babel/[email protected]: 🚨 This package has been deprecated in favor of separate inclusion of a polyfill and regenerator-runtime (when needed). See the @babel/polyfill docs (https://babeljs.io/docs/en/babel-polyfill) for more information.
npm WARN deprecated [email protected]: Switch to the `bfj` package for fixes and new features!
npm WARN deprecated [email protected]: support for ECMAScript is superseded by `uglify-js` as of v3.13.0
npm WARN deprecated [email protected]: This SVGO version is no longer supported. Upgrade to v2.x.x.
npm WARN deprecated [email protected]: Please use @electron/rebuild moving forward.  There is no API change, just a package name change
npm WARN deprecated @material-ui/[email protected]: Material UI v4 doesn't receive active development since September 2021. See the guide https://mui.com/material-ui/migration/migration-v4/ to upgrade to v5.
npm WARN deprecated @material-ui/[email protected]: Material UI v4 doesn't receive active development since September 2021. See the guide https://mui.com/material-ui/migration/migration-v4/ to upgrade to v5.
npm WARN deprecated [email protected]: Support has ended for 9.x series. Upgrade to @latest
npm WARN deprecated [email protected]: core-js@<3.23.3 is no longer maintained and not recommended for usage due to the number of issues. Because of the V8 engine whims, feature detection in old core-js versions could cause a slowdown up to 100x even if nothing is polyfilled. Some versions have web compatibility issues. Please, upgrade your dependencies to the actual version of core-js.
npm WARN deprecated @material-ui/[email protected]: Material UI v4 doesn't receive active development since September 2021. See the guide https://mui.com/material-ui/migration/migration-v4/ to upgrade to v5.
npm WARN deprecated [email protected]: mdn-browser-compat-data is deprecated. Upgrade to @mdn/browser-compat-data. Learn more: https://github.com/mdn/browser-compat-data/blob/v1.1.2/UPGRADE-2.0.x.md

> [email protected] postinstall
> node -r babel-register internals/scripts/CheckNativeDep.js && npm run flow-typed && npm run build-dll && electron-builder install-app-deps && node node_modules/fbjs-scripts/node/check-dev-engines.js package.json



Webpack does not work with native dependencies.
@material-ui/core, @material-ui/icons, @material-ui/lab, antlr4, archiver, babel-plugin-flow-react-proptypes, classnames, command-exists, csvtojson, d3-svg-annotation, d3, devtron, ejs-compiled-loader, ejs, electron-debug, electron-is-dev, font-awesome, hex-to-rgba, history, html-loader, immutable, jest-each, jest-junit, ltlsim-core, mathjs, node-html-parser, node-uuid, product-iterable, raw-loader, react-color, react-dom, react-json-view, react-markdown, react-mathjax2, react-redux, react-router-dom, react-router-redux, react-router, react-stars, react, recharts, redux-thunk, redux, slate-history, slate-react, slate, source-map-support are native dependencies and should be installed inside of the "./app" folder.


First uninstall the packages from "./package.json":
npm uninstall your-package

Then, instead of installing the package to the root "./package.json":
npm install your-package --save

Install the package to "./app/package.json"
cd ./app && npm install your-package --save


Read more about native dependencies at:
https://github.com/chentsulin/electron-react-boilerplate/wiki/Module-Structure----Two-package.json-Structure



npm ERR! code 1
npm ERR! path /Users/yuna_hwang/Documents/Wisconsin/Research/resources/fret/fret-electron
npm ERR! command failed
npm ERR! command sh /var/folders/zd/dxn2cgtj5jsdnvh3nzcrnfw40000gn/T/postinstall-aa3336f3.sh

npm ERR! A complete log of this run can be found in:
npm ERR!     /Users/yuna_hwang/.npm/_logs/2023-05-18T19_41_49_606Z-debug-0.log

Thanks in advance.

pmLTL and fmLTL don't seem to be equivalent

Hi，

When I used the FRET tool to simulate the protocol run, I found that the PmLTL execution results were different from the FmLTL execution results.

For the following FRETish Requirement: in m1 when i1 the system shall at the next timepoint satisfy o1. The execution trace of pmltl is as follows:

Fmltl execution trace is as follows:

Follow A Compositional Proof Framework for FRETish Requirements paper, it seems that only pmltl conforms to the trigger function. I'm not sure and would like to ask this question.

Yours Frankly,
SoftPro

Unsucccessful Installation

Hello,

I seem to be having some recurring issues with trying to run an install of this application. Part of the problem appears to be deprecated dependencies and peer dependencies which need to be manually installed, but there is also a regular warning about a valid SPDX license expression. This is definitely not as straightforward nor as simple as running the four commands stated in the README.

I've tried installing this on a Mac (10.15.6) as well as on a Linux system (Amazon Linux 2), both of which have a GUI client. I've not tried on a PC, but I'd also prefer not to install on that OS either.

I have tried prior to the update regarding "npm run fret-install" as well as after. Neither works.

Can someone try to do a fresh install and possibly provide further details on what may be missing. I'm attaching the latest stdout from running "npm run fret-install"

fret.log

Export requirements status field in json format

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.

Requirement Description Text Box Stops Various Keys (and highlighting) from Working

When typing in the Requirements Description text box, various keys do not work.
E.G.:

• Home
• End
• CTRL+SHIFT+left arrow (should accumulate highlight, but it only highlights a word/part and then loses the highlight to highlight the next word/part)

Also, trying to highlight with the mouse (click and drag) only works from the front (first word) to the back (last word) of the string. If I try to highlight from the end of the string, going towards the front I get the same problem as with trying to highlight using CTRL+SHIFT+left arrow .

This is v3.0, running on Ubuntu 20.04.6.

Variable Mapping Import

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!