NASA-SW-VnV/fret

the path generation

Closed this issue · 8 comments

SoftPro commented

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.

anmavrid commented

Hello SoftPro and thanks for your interest in FRET.

What do you mean by path generation template? What would you like to do?

SoftPro commented

Hello,I want to study how to verify the key. I see generate in the semanticstestgeneration.js file under the path of FRET master \ FRET electron \ test \ semantics_ Tests method, which automatically generates random intervals, but I don't know how it is associated with keys. I saw an architecture in the 2021 automated formalization of structured natural language requirements paper. The above expression means to transfer the template key and the generated path to Oracle, and then obtain e according to rtgil semantic analysis. What's the key_ Where is the generator code implemented? If I understand wrong, you can also put it forward. Thank you.

tpressburger commented

I am not sure I understand your question. However, I give below an annotated
SemanticsTestGeneration call-graph with some comments, maybe it will help?

Note you can run tests as follows:

% cd fret/fret-electron/test/semantics
% node SemanticsTestGeneration.js

You'll need nuXmv (or NuSMV if you change callNuSMV; see below) and you need
to set the environment variable nuXmv_HOME (or NuSMV_HOME). It generates
files in /tmp such as /tmp/temp1, which I have attached (as temp1.txt)

runSettings (line 94)
  generate_tests
    // This creates a testCase object which has:
    //   fields containing the intervals for mode, precondition, stop
    //     condition and response, and an integer for duration;
    //   a field named testFormulas that has, for every key, a triple of
    //     key; // There is a product iterable (see line 20) that enumerates through
    //             all keys. Which values for each template key field will be
    //             enumerated for each test option is in testingOptions.js;
    //             for example, line 95. An example key is the string
    //             "in,regular,within,satisfaction"
    //             (see line 236 of SemanticsTestGeneration.js).
    //     semantics object; // This has past- and future-time LTL formalizations.
    //     the expected value from the oracle // see line 239.
  executeTestCase(testCase, tool)
    generateSMVInfo(triple, duration)
      // Generate SMV format for each key's past and future formalizations.
    runTraceAnalyzer(tool,testCase,formulae,keys)
      CallNuSMV.js:testNuSMV
        CallNuSMV.js:createSMV // Create SMV spec as string.
        CallNuSMV.js:writeSMV  // Write the SMV spec string to a file.
        CallNuSMV.js:callNuSMV // Invoke nuXmv or NuSMV on the file.

Did this help? Let us know if you have further questions.
temp1.txt

SoftPro commented
  • 👍1
anmavrid commented

I am closing this issue. @SoftPro please let us know if you have any other questions.

SoftPro commented
SoftPro commented
andreaskatis commented

Hello,

there is no attached picture in your posts. I guess you are referring to the error icon in realizability portal indicating that a dependency is missing. The message should say precisely which of the three dependencies (jkind, z3, aeval) is not detected.

To make sure that you have successfully added the binary paths of each dependency in your environment variable, please see if you can successfully call the following commands from the Ubuntu terminal:

  • jrealizability : This is the JKind command for realizability options. It should display the list of available options for the tool.
  • z3 -h : This is the command to call z3 from the terminal, and it should return a list of options for it.
  • aeval : This is the AE-VAL call and, like the rest, should display the list of available options for it.