Missing /Documents/fret-db directory on Fret 3 Install (via WSL)

[dbahu]

I had to add this manually for Fret to run correctly (LOCK file problem otherwise)

Minor issue but correcting it will give smoother new user experience

[HB-Stratos]

I also had this issue with WSL. Had to create the ~/Documents/fret-db folder and restart fret, otherwise it was impossible to import any projects

[andreaskatis]

Hi @dbahu , @HB-Stratos ,

Thank you for installing FRET and contributing to this thread. Could you please clarify whether your WSL installation already had a Documents folder or not? FRET normally creates the fret-db folder during the first time it is run, but assumes the existence of the Documents folder, which WSL Ubuntu installations do not come with by default. This is why we require the creation of Documents as part of our WSL guide.

If you already had a Documents folder, can you please specify which version of Ubuntu you are running? I cannot replicate this on 24.04 without first deleting Documents.

Best Regards,

Andreas

[HB-Stratos]

Hi @andreaskatis ! I ran it on Ubuntu 22.04. I did likely forget to create the documents folder as I was switching back and forth between the windows and linux guides to figure out which node version I had to have installed (not mentioned in the windows guide). This slipped through the cracks, sorry!

I did try to continue installing fret after fixing this, but I failed to get all the required solvers set up as most of their download pages do not come with set up instructions. I manually downloaded jkind, but when z3 failed to build using vcpkg, I gave up on the endeavor and moved to testing other RE tools. Inbuilt downloading for all dependencies necessary for the program to function would be nice. Without them fret doesn't work properly (clicking test case generation completely breaks the UI and everything locks up).

[andreaskatis]

Thank you for the feedback, @HB-Stratos. One (perhaps easier) way to install Z3 would be to 1) download a pre-built x64-glibc binary release from here, 2) extract it to a location of your choice inside WSL and 3) add the full path to the bin folder in the extracted folder to your PATH variable.

As an example, if you extract the contents of the folder to ~/z3, you need to add /home/your_username/z3/bin in your PATH. To do the latter you need to follow the steps below:

1. Open ~/.profile
2. Add export PATH=$PATH:/home/your_username/z3/bin in a new line at the end of the file.
3. Save and close file.
4. Run . ~/.profile in the terminal.
5. Verify that Z3 has been installed by running z3 -h in the terminal.

Other core dependencies such as jkind (Realizability Checking only), kind2 and NuSMV can be installed through this way (assuming the corresponding binary has been downloaded). The Realizability Checking and Test Case Generation manuals specify which dependencies are relevant for each feature and have pointers to where each dependency can be downloaded from.

The issue you have faced in Test Case Generation has already been fixed internally and should be addressed in our next public release. In the meantime, you should be able to circumvent this by installing kind2, Z3 and NuSMV (version 2.6 or older).

If you encounter other issues, or have questions in general, please do not hesitate to ask. We appreciate your feedback and are always happy to assist!

Best,

Andreas

[HB-Stratos]

Hi Andreas!

Thank you for taking the time to respond. I'll try to follow your tips in a moment. I chose vcpkg at first because it seemed the easiest as I wasn't quite sure which of the many compiled binaries I should download. From your response I gather I likely need the .tar.gs and in that I need to target the bin folder.

I do actually have a few more bits of feedback and issues I noticed testing that I'll write out here before I forget. Do feel free to send me somewhere else if this is not the right place to put this.

• I really like the general foundation here. I can see how more strictly formalizing what a requirement should be can make verifying then far easier.
• However, I do not like the current visualization too much.
  Take for example when emergency_button the liquid_mixer shall immediately satisfy ! valve_2 . As a programmer I can sorta read this. If I gave this to a seasoned engineer who never touched a line of code in their time (of which I know many) they could not read this. And even I struggle to parse this. What on earth is valve_2? Where do I find more about where on the machine valve_2 is? Is emergency_button a boolean? etc.
  This is very much the opinion of a newbie and someone not used to this style of writing, but I would have perhaps tried to generate the output like this: when emergency_button is active, then the liquid_mixer shall immediately satisfy valve_2 off I do realize this gets harder for more complex logic expressions, but I do think there is value in having an easily human readable version. More clear distinction of which things are booleans vs system elements etc would help here.
• How do I version manage requirements? It seems they are stored in some sort of internal DB, how would I use git here? I personally would much prefer to see a clear file structure of requirements I can easily version manage with git instead of 000015.ldb which I can not easily throw into git. Manually exporting and version managing the export feels... suboptimal. Not having proper version control and ideally platform independent requirement storage in easily readable files really is a dealbreaker for me.
• It feels strange that a requirement can only have one parent. In the RE documents I have worked on this far I've frequently had to deal with requirements that were caused by three or four higher level requirements. In general, I haven't really seen much of the traceability aspect I am looking for in a RE program. Did I just miss it or is that not really the focus?
• The structured language is useful for many things, but how would I encode a top level requirement such as 'The System shall not endanger any personnel during normal operation'?
• On the main menu the ball overview, the text does not scale properly, leading to hundreds of overlapping labels in a large project such as the LMCPS case study. The menu is entirely unreadable and makes the software look broken.

• Very much a nitpick, but why take precious home page space to state requirements size in bytes? What value does this provide for the reader?
• Another nitpick: when viewing more lines than there are requirements in the requirements viewer, there is just a large empty space.
• The fretish grammar seems nice, but the introduction links to a place to learn more about it... that place is just a long pdf document of unexplained, pixelated flow charts. Not something that helps a new user gather their bearings.
• The WSL approach is really not excellent. I realize how annoying it is to build software for multiple OS's and I'm happy to see linux support, but WSl Gnome really doesn't look great, has low frame rate, and gestures like dragging a window against the top of the screen to full-screen it do not work.
• I do really like the inbuilt help screens with big explanatory images to quickly see where one has to go.
• I'm not sure if this can even work with the display output, but a docker container that automatically gets all optional dependencies etc would be very useful as a quickstart, and good reference for how to set it up bare metal if necessary.
• The requirements page in general feels really basic. 10 requirements shown by default, really? in a project with hundreds of requirements in many different groups and dependencies, this feels like very little. The next page and rows per page buttons are buried at the bottom, making it a little annoying from a user perspective to browse the requirements of an unfamiliar project.
• A graph view of requirements would be really cool to have, and a great visual aid for how top level requirements cascade down into lower levels.
• I really like the separated rationale and comments fields for each requirement.
• The glossary and helpers in the requirement creation menu are great.
• Why is the create new requirement button next to the projects dropdown? To me that looks like I'd use that button to create a new project, not a requirement.
• What is the purpose of being able to load multiple projects at once?
• The requirements list resizes both horizontally and vertically depending on content of the fields, making quickly flicking through pages difficult.
• A nomenclature definition of some kind would be useful. A place where standardized terms are stored together with an explanation of what exactly they refer to, documentation links, etc.

Overall, I really like the stability and constraints the fretish language gives and I can see the advantages that come with such a system. It does feel though like this is not quite yet a full Requirements Engineering tool as I would have expected it to work. I feel like I am missing a good few features that I would have liked to see, and the overall UI feels like a proof of concept. Still, a solid foundation that I will follow closely!

[anmavrid]

Hi @HB-Stratos,

Thank you for such detailed feedback! This is exactly the kind of user perspective that helps improve tools like FRET.

You have touched on a critical distinction between Requirements Management tools (which prioritize text, traceability, and versioning) and FRET (which prioritizes automated formalization, unambiguous semantics, formal analysis, and test case generation). The latter (formalization, analysis, etc) are capabilities that standard Requirements Management tools do not typically support, and that distinction shapes many of the design decisions behind FRET.

Let me address your points one by one.

1. Installation and Environment (WSL, Solvers, Docker)
Regarding the ~/Documents folder our manual has an explicit mkdir step for WSL users.

For solvers, we recommend always using pre-compiled binaries. Compiling Z3 from source via vcpkg on WSL is often overkill and prone to toolchain errors. The pre-compiled .tar.gz binaries and targeting the bin folder is the path of least resistance here.

Note also that we do provide a Docker image for creating a complete FRET executable on Unix-based systems.

Here is also a reply from @andreaskatis:
We are not sure what you are referring to with "WSL GNOME". Our installation guide depends on running FRET using WSLg which comes with every WSL installation and enables the use of Linux GUI apps without the need of a desktop environment in the WSL instance. If by "WSL GNOME" you mean that you were trying to use FRET within a GNOME desktop environment that you installed on top of your WSL instance, then it is reasonable to experience worse performance (e.g. low frame rates) since it would be heavier resource-wise and it does not seem to be a feature officially supported by Windows. If you are relying on WSLg instead, we recommend installing the latest graphic drivers for the machine that you are running (as suggested in the Linux GUI apps guide link). Other than that it may be an issue that should be reported to WSLg developers, as we have not experienced frame rate issues in using WSL on our end so far.

2. Readability vs. Formalism (The 'valve_2' Issue)
This is the central tradeoff of FRETish. It is not free-text, but it is also not a purely symbolic formal language: it is a controlled natural language augmented with Boolean and arithmetic expressions that most engineers with a technical background will already be familiar with.

The formalism is intentional: it eliminates the ambiguity of natural language requirements as complexity grows, and it is precisely what enables automated formal verification and test case generation.

That said, there is more flexibility in how you write requirements than may have been apparent. The requirement you found hard to read can be expressed in more readable ways. E.g., see the following two options:

• when emergency_button_active the liquid_mixer shall immediately satisfy valve_2_off
• when emergency_button = active the liquid_mixer shall immediately satisfy valve_2 = off

The tool requires you to be explicit about whether something is a variable, a state, or a value. So ! valve_2 implies valve_2 is a Boolean, while valve_2 = off treats off as a value. Once that convention clicks, the language reads quite naturally. FRET also generates a natural language rendering of each requirement alongside the formal syntax, which is useful for communicating with stakeholders less comfortable with formal notation.

3. Version Control
FRET uses an internal PouchDB to maintain real-time consistency, but it does fully support JSON import and export of requirement sets.

The exported JSON is human-readable, diff-friendly, and git-compatible.

Here is the intended workflow for version management:

• Commit: Export your project to JSON → commit to Git.
• Pull: Check out the repo → import JSON into FRET.

We acknowledge this is less seamless than a native file-based system, however it ensures database integrity.

4. Single Parent Limit
The single parent limit is intentional, and it reflects a constraint of formal analysis. It ensures that the formal semantics remain well-defined and traceable in a way that automated tools can reason about reliably.

That said, we recognize this can be limiting when coming from a traditional Requirements Management background, where a requirement being motivated by or related to multiple higher-level requirements is common.
A few things worth noting here:

• The parent-child relationship in FRET is specifically about formal derivation and it is not the only mechanism for expressing relationships between requirements. For example, all requirements that use the same component level also have a semantic relationships in FRET. I can expand more on this, if you are interested.
• If a requirement genuinely satisfies multiple higher-level obligations, it is worth examining whether those higher-level requirements are truly distinct or whether they share a common abstraction that could serve as the single formal parent, with the others captured as related context.
• We are considering extending the parent-child relations in FRET to reflect different relationships between requirements in the future.

5. High-Level Non-Formal Requirements
FRET does not require every requirement to be expressed in FRETish. High-level requirements that resist formalization , such as "The system shall not endanger any personnel during normal operation”, can be entered as free English text using quotes in the requirement editor. This allows you to create an entry, capture the intent, and then link it to lower-level formal requirements using the parent-child relationship, preserving traceability without forcing artificial formalization.

6. UI Improvements
Thanks for the feedback! We will consider your suggestions.

Last I want to note that FRET is an open-source tool. Thus, if you would contribute to its codebase, we can do that through an agreement. If you are interested in this, please let us know and we can provide more information.

Thanks!
Anastasia

[HB-Stratos]

Hello Anastasia!

First of all, thank you so much for taking the time to reply! I did dump quite the wall of text, frankly never expecting a reply, and it's really cool to see my thoughts were heard.

It does seem I had a bit of a misconception going into looking at FRET. I ended up here when searching for an open source requirements engineering program that is a little better than a word document with manually maintained traces that I've previously had the displeasure of working with. FRET appears to be related, but distinct. At the end of the day I unfortunately think that FRET is not the tool for my problem of just wanting to manage personal and contracting projects better, but I do still think that many ideas presented here carry a lot of value. I think even 'standard' requirements engineering programs could benefit from the more strict syntax FRET requires. It really helps to avoid unspecific or otherwise not fully defined requirements. Speaking of 'standard' requirements engineering programs, I haven't really been able to find much else in the open source world, most other options I tested were either very limited or half broken. Do you happen to know any open source solution for classic RE?

1. Installation

Yep, the documents folder was my mistake. Had to switch between the linux and wsl docs to figure out node version and ended up missing a step.

For solvers I just wasn't familiar enough with installing binaries under linux, otherwise being used to apt, and frankly didn't think to check the tar.gz. So vcpkg seemed the easiest and most reliable at first glance as its install seemed pretty simple. But it did not work out as we saw.

I must have also missed the docker image, that would have made things easier for sure.

I was indeed referring to the gnome window opened up by WSLg. In my opinion, it just looks a bit strange on windows, and as I said windows spawned by WSL into the normal windows desktop don't quite behave right, see the full screening gesture.

2. Readability

Your explanation indeed makes it a little more clear. I would still argue that there is a middleground here where displayed text could be adapted to be more easily comprehensible without changing the background logic definition.
Regarding valve_2 I was thinking more of maybe a link to a diagram that showed me where on the machine this valve might be. This may be more of a variable name issue, bowl_outlet_valve would be more obvious.

3. Version Control

In my experience, export tools like these have not been useful for version control. This is because machine serialization often doesn't pay attention to export order, so things like git that pay attention to changes on a line by line basis get really confused when a bunch of entries swapped places during the export. I haven't tested it with fret, if it is indeed stable git would be usable, though having to constantly use export and import instead of git being the source of truth is not ideal in my opinion.

4. Single Parent

That is fair. I am frankly not knowledgeable enough in the formal side to know what issues could arise out of multiple parents.

5. Non-Formal Reqs

Noted, good to know that that is possible.

I am aware that FRET is an open source tool. I do appreciate your offer to contribute. Unfortunately I do not think I am equipped to handle this job, neither in theoretical knowledge about formal requirements verification nor in web development, so I unfortunately can not offer to contribute for the time being. Speaking of theoretical knowledge, where could I learn more about why one would want formal verification? I can see how checking no requirements conflict could be useful, but beyond that it isn't a topic I've thought much about this far.

[anmavrid]

Hi @HB-Stratos,

Thanks for your detailed answers!

Regarding the analysis capabilities of FRET, you can have a look at these papers: FRET Consistency Analysis and FRET Tool They demonstrate how analysis and validation can be helpful for requirements elicitation.

All the best,
Anastasia