mbeddr/mbeddr.formal

FASTEN: FormAl SpecificaTion ENvironment - a set of DSLs to experiment with rigorous systems and safety engineering.

mbeddr.formal's Issues

safety.gsn: Cannot connect strategy to goal

GSN: show text of referenced goal in away goal

When creating a GSN and adding an away goal, it would be beneficial to see the description of the referenced goal in the away goal directly.
@norro as discussed, please take over from here.

Textgen for ocra language

Currently the ocra language (see feature/ocra) is missing textgen. Add textgen aspects for all concepts used in the sandbox examples.

Attributes in Assemblies

Our components have internal state, for example, a failure_count. This is used in contracts. RIght now it looks as if it is not possible to have properties/variables/attributes in assemblies. Is this planned?

Gradle Exception: Could not set unknown property 'archiveBaseName'

On commit:
42ef418 (master)

When running:
gradle

Full Exception:
Could not set unknown property 'archiveBaseName' for task ':packageNuSMV' of type org.gradle.api.tasks.bundling.Zip.

Relevant code:
task packageNuSMV(type: Zip, dependsOn: build_smv_languages) {
archiveBaseName = 'com.mbeddr.formal.nusmv'
from artifactsDir
include 'com.mbeddr.formal.nusmv/**'
}

Please let me know what other information is required.

Edit: Gradle version
Gradle 4.4.1

Build time: 2012-12-21 00:00:00 UTC
Revision: none

Groovy: 2.4.16
Ant: Apache Ant(TM) version 1.10.6 compiled on July 11 2019
JVM: 11.0.5-ea (Ubuntu 11.0.5-ea+10-post-Ubuntu-0ubuntu1)
OS: Linux 5.3.0-23-generic amd64

Second Edit:
Seems to be caused by the Gradle version < 5. Note that this is on Ubuntu 19.10.

Missing type inference for PortRef

base.arch.cbd.assembly.connections.PortRef is missing a type inference rule, breaking analysis of one of our use cases.

FASTEN reports SUCCESS if it does not find the NuSMV binary

We're running FASTEN's Run NuSMV action on Ubuntu 18.04. We had no NuSMV installed, the binary was not found. However, the result table in MPS it shows "SUCCESS - no verification conditions found".

Instead it should fail with an error.

changes in core analyes

I'm not sure if you are using the infrastructure from core analyses to run your tools. If so I introduced a change in some of the classes related to the tool runners to be able to pass the repository down to the part of the code that loads the text gen traces. That code was still using global model access. I removed that usage and hat to change some method signatures. This is required for MPS 2020.3 but was introduced in master today as part of the 2020.2 migration.

mbeddr/mbeddr.core@9415437

Safety.GSN: Enable creating connections from strategy to goals

Add unix nusmv

Currently mbeddr.formal/rcp_resources/external_tools/ only contains nusmw.exe. We should add unix nusmv as well

Safety.GSN: The direction of the connections is wrong

• argument over hazard
  

• connection from smv.spec goal to context is missing arrow
  

Snapshot 2020-07-28 zip contains paths that are too long

Getting errors reported with unzipping Snapshot 2020-07-28 sources. Filepath too long.

On windoze 10.

Enum type for ocra

The ocra language currently doesn't support an enum type, but only allows inline definition of enum-like types, which breaks MPS type inference.

Documentation error for enabling FSM visualization

The _040_state_machines file states that the visualization of the FSM can be enabled through Projection > State-machine Diagram View. This is not correct, it is Notations > State-machine Diagram View.

Generation issue with CBD

Hello,

I'm having an issue with a small system defined as a component-based design in FASTEN Snapshot 2020-05-14. Below is a minimal working example.

After this system is created, I cannot check AG or build the model. When I build the model, the error messages are:

Generator language is applied to a model TestSolution.test_model not from generator module (actual module is TestSolution), aborted.
Unexpected null value. Transform function of MAP-SRC didn't produce any result. Please check the function and make sure it always supplies a node

The error points to this reduction rule.

concept FunctionMacroCall --> <T  $MAP_SRC$0  T> 
inheritors false                                  
condition <always>                                

Perhaps the error is due to the chained function calls of the deriv and abs_diff functions?
Let me know if you require any other information.

TestSystem                                                    
model   TestSolution.test_model 
------------------------------                       
#FUNCTION deriv(p) = (next(p) - p);                           
#FUNCTION abs_diff(p1, p2) = ((p1 >= p2)?(p1 - p2):(p2 - p1));
                                                              
interface AInter                                              
  a_in : 5..24 => no output                                   
contract:                                                     
  pre(1) suff_in : G (a_in = 5);                              
                                      
interface BInter                                              
  b_in : -510..510  => no output                              
  b_in2 : -510..510                                           
contract:                                                     
  post(1) b_check : G ((deriv(abs_diff(b_in, b_in2)) > 0));   
                                                              
assembly ExampleAssem                                         
  no input => no output                                       
contract:                                                     
  no contract                                                 
  body: AInter a;                                             
        BInter b;

Signed and unsigned word not permitted as type

I was trying to extend the _010_traffic_lights_controller_baseLang example with additional variables and noticed that FASTEN doesn't seem to accept variables of type unsigned word [N] and signed word [N]. Is this a user error or does FASTEN limit the allowed types for state machines?

  VAR {                                                                       
    state variable traffic : {Green, Yellow, Red};                            
    pedestrian : {Walk, DontWalk};                                            
    timer : 0..10;                                                            
    abc : signed word [5];                                                    
  }

Error message on hover:
Abstract concept instance detected. Use one of sub-concepts instead. Concept: Type

Apologies if this is a trivial mistake caused by my inexperience with FASTEN and NuSMV.

Errors in Spin Module

There are numerous errors in com.mbeddr.formal.spin, preventing its building from the Gradle file.

Edit: Building the module within MPS directly produces the two errors in SpinCexTableModel.

[generate] 22 errors during generation:
 [generate] Compilation problems
 [generate] com/mbeddr/formal/spin/runner/SpinRunner.java : The local variable panFileFullyQualifiedName may not have been initialized (line: 38)
 [generate] com/mbeddr/formal/spin/runner/SpinRunner.java : The local variable panFileFullyQualifiedName may not have been initialized (line: 41)
 [generate] com/mbeddr/formal/spin/runner/SpinRunner.java : The local variable panFileFullyQualifiedName may not have been initialized (line: 43)
 [generate] com/mbeddr/formal/spin/runner/SpinRunner.java : The local variable panFileFullyQualifiedName may not have been initialized (line: 45)
 [generate] com/mbeddr/formal/spin/runner/SpinRunner.java : The local variable panFileFullyQualifiedName may not have been initialized (line: 52)
 [generate] com/mbeddr/formal/spin/runner/SpinRunner.java : The local variable panFileFullyQualifiedName may not have been initialized (line: 60)
 [generate] com/mbeddr/formal/spin/runner/SpinRunner.java : The local variable panFileName may not have been initialized (line: 70)
 [generate] com/mbeddr/formal/spin/runner/SpinRunner.java : The local variable panFileName may not have been initialized (line: 78)
 [generate] Compilation problems
 [generate] com/mbeddr/formal/spin/ui/SpinCexTableModel.java : The type com.mbeddr.formal.base.tooling.results_model.IWhitnessEntry cannot be resolved. It is indirectly referenced from required .class files (line: 8)
 [generate] com/mbeddr/formal/spin/ui/SpinCexTableModel.java : Bound mismatch: The type ISpinWitnessEntry is not a valid substitute for the bounded parameter <T extends IWhitnessEntry> of the type WhitnessTableModelBase<T> (line: 8)
 [generate] Compilation problems
 [generate] com/mbeddr/formal/spin/analyzer/SpinAssertionsAnalyzer.java : The local variable slr may not have been initialized (line: 39)
 [generate] com/mbeddr/formal/spin/analyzer/SpinAssertionsAnalyzer.java : The local variable slr may not have been initialized (line: 40)
 [generate] Compilation problems
 [generate] com/mbeddr/formal/spin/testing_utils/SpinTestingUtils.java : The local variable aa may not have been initialized (line: 36)
 [generate] com/mbeddr/formal/spin/testing_utils/SpinTestingUtils.java : The local variable sba may not have been initialized (line: 47)

These errors may come from a problem with text generation of safe read actions.

For example, in the SpinAssertionsAnalyzer:

safe read action with modelRepository : { 
  slr = SpinResultLifter.lift(srr, config, modelRepository); 
} end action

In the generated Java file:

/* error: statement w/o textGen:safe read action */

Let me know if any other information is required.

Integer keyword undefined for nusmv

Hello,

I defined the simple system in FASTEN:

TestSystem                     
model   TestSol.test_model                          
------------------------------ 
interface TestInter            
  a : integer => b : integer   
contract:                      
  no contract                  
                               
assembly TestAssembly          
  no input => no output        
contract:                      
  no contract                  
  body: TestInter one;         
        TestInter two;         
        connect one.b to two.a;

When I right-click the assembly, and hit Check AG, I receive the following error message from nusmv:

solutions/TestSol/source_gen/TestSol/test_model/TestAssembly___flattenedSystem.smv: line 3: "integer" undefined

Here is the generated artifact:

MODULE TestAssembly___flattened
  VAR
    one_DOT_a : integer;
    one_DOT_b : integer;
    two_DOT_a : integer;
    two_DOT_b : integer;
    
  DEFINE
    arch_wiring := (one_DOT_b = two_DOT_a);
  
MODULE main
  VAR
    flattened : TestAssembly___flattened;

The nusmv manual says that integer is a valid keyword, so I don't understand what is the issue here.

I also noticed that none of the tutorial examples in FASTEN use the integer keyword. Perhaps there is an issue here that's not being tested in the tutorial examples?

Thanks for any help you can give.

Build error when running gradlew on Ubuntu 20.04

I specified the paths in gradle,properties according to the installation instruction. When I ran the gradlew, it exit with the following the error:

BUILD FAILED
**/mbeddr.formal/build/scripts/build_all_scripts.xml:150: Could not create type generate due to java.lang.N
oClassDefFoundError: org/jdom/JDOMException
at jetbrains.mps.build.ant.MpsLoadTask.(MpsLoadTask.java:51)
at jetbrains.mps.build.ant.generation.GenerateTask.(GenerateTask.java:24)
at java.base/jdk.internal.reflect.NativeConstructorAccessorImpl.newInstance0(Native Method)
at java.base/jdk.internal.reflect.NativeConstructorAccessorImpl.newInstance(NativeConstructorAccessorImpl.java:62)
at java.base/jdk.internal.reflect.DelegatingConstructorAccessorImpl.newInstance(DelegatingConstructorAccessorImpl.java:45)
at java.base/java.lang.reflect.Constructor.newInstance(Constructor.java:490)
at org.apache.tools.ant.AntTypeDefinition.innerCreateAndSet(AntTypeDefinition.java:318)
at org.apache.tools.ant.AntTypeDefinition.createAndSet(AntTypeDefinition.java:264)
at org.apache.tools.ant.AntTypeDefinition.icreate(AntTypeDefinition.java:219)
at org.apache.tools.ant.AntTypeDefinition.create(AntTypeDefinition.java:206)
at org.apache.tools.ant.ComponentHelper.createComponent(ComponentHelper.java:286)
at org.apache.tools.ant.ComponentHelper.createComponent(ComponentHelper.java:264)
at org.apache.tools.ant.UnknownElement.makeObject(UnknownElement.java:427)
at org.apache.tools.ant.UnknownElement.maybeConfigure(UnknownElement.java:165)
at org.apache.tools.ant.Task.perform(Task.java:349)
at org.apache.tools.ant.Target.execute(Target.java:449)
at org.apache.tools.ant.Target.performTasks(Target.java:470)
at org.apache.tools.ant.Project.executeSortedTargets(Project.java:1391)
at org.apache.tools.ant.Project.executeTarget(Project.java:1364)
at org.apache.tools.ant.helper.DefaultExecutor.executeTargets(DefaultExecutor.java:41)
at org.apache.tools.ant.Project.executeTargets(Project.java:1254)
at org.apache.tools.ant.Main.runBuild(Main.java:830)
at org.apache.tools.ant.Main.startAnt(Main.java:223)
at org.apache.tools.ant.launch.Launcher.run(Launcher.java:284)
at org.apache.tools.ant.launch.Launcher.main(Launcher.java:101)
Caused by: java.lang.ClassNotFoundException: org.jdom.JDOMException
at org.apache.tools.ant.AntClassLoader.findClassInComponents(AntClassLoader.java:1383)
at org.apache.tools.ant.AntClassLoader.findClass(AntClassLoader.java:1338)
at org.apache.tools.ant.AntClassLoader.loadClass(AntClassLoader.java:1093)
at java.base/java.lang.ClassLoader.loadClass(ClassLoader.java:522)
... 25 more

Process 'command '**/mbeddr.formal/build/jbrDownload/jbr/bin/java'' finished with non-zero exit value 1

Omitting the local path with **. For a first go, it looks like a Java error but I couldn't figure out what causes it. Is there a workaround to this issue?

Array access

While it is possible to define arrays, it is not possible to access elements of arrays. Also, the nary AND and nary OR do not work as expected for arrays.
Example:
Legal mbedder.formal SMV:

MODULE main {                                 
  VAR {                                       
    x : array 0..5 of boolean;                
  }                                           
  DEFINE {                                    
    y := [TRUE, TRUE, TRUE, TRUE, TRUE, TRUE];
  }                                           
  LTLSPEC x = y;                              
  LTLSPEC [& x ] = TRUE;                      
}

Generated is the following plain SMV, which leads to a "TYPE ERROR file system.smv: line 7 : illegal operand types of "=" : array 0..5 of boolean and boolean; ERROR: Property "x = TRUE" is not correct or not well typed.":

MODULE main
  VAR
    x : array 0..5 of boolean;
  DEFINE
    y := [TRUE, TRUE, TRUE, TRUE, TRUE, TRUE];
  LTLSPEC x = y
  LTLSPEC x = TRUE

What I would like to have is

1. to be able to write LTLSPEC x[0] = y[0]; in mbedder.formal being translated to the same in plain SMV (2) and
2. the [& x ] = TRUE in mbedder.formal to be expanded to (x[0] & x[1] & x[2] & x[3] & x[4] & x[5]) = TRUE in plain SMV.

Include testing in github actions

Currently only seems to build + assemble.

Build failure with message "Could not get unknown property 'gpr.user' for root project 'mbeddr.formal'"

I clone the repo and started to build by executing ./gradlew at the terminal and the build fails with the following message:

Configure project :
Local build detected, version will be SNAPSHOT

FAILURE: Build failed with an exception.

• Where:
  Build file '<Local_PATH_omitted>/mbeddr.formal/build.gradle.kts' line: 128

• What went wrong:
  Could not get unknown property 'gpr.user' for root project 'mbeddr.formal' of type org.gradle.api.Project.

• Try:

Run with --stacktrace option to get the stack trace.
Run with --info or --debug option to get more log output.
Run with --scan to get full insights.

• Get more help at https://help.gradle.org

BUILD FAILED in 328ms_

Request for Adding Support for NuXMV

Hello,

An industry partner on my side is interested in using FASTEN, but has a requirement of using reals and integers instead of ranges in their solutions.

As far as I understand, this is possible if NuXMV is used as the FASTEN backend, instead of NuSMV.

Right now, I believe using NuXMV is done by replacing the NuSMV binary. However, this still allows the user to use NuXMV keywords, which will fail (as in my issue #27). And the real keyword would not be available.

Kindly, could there be a NuXMV option provided within FASTEN? Such that toggling it switches to "NuXMV mode", where a) the nuxmv binary is used, and b) both the integer and real keywords be allowed?

Please let me know if this is not feasible. Thanks.

Mapping of connections while flattening does not work for structs

(Sorry for creating the next issue instead of fixing it and creating a pull request. I know it's a bad excuse but I still couldn't acquire the necessary open source contribution rights.)
Here is a minimal example in FASTEN:

struct struct1 {                
  b : boolean;                  
}                               
                                
interface iin                   
  in : struct1 => no output     
contract:                       
  no contract                   
interface iout                  
  no input => out : struct1     
contract:                       
  no contract                   
assembly a                      
  no input => no output         
contract:                       
  no contract                   
  body: iin i1;                 
        iout i2;                
        connect i2.out to i1.in;

This is translated to

MODULE a___flattened
  VAR
    i1_DOT_in : struct1_struct;
    i2_DOT_out : struct1_struct;
    
  DEFINE
    arch_wiring := (i2_DOT_out = i1_DOT_in);
  

MODULE main
  VAR
    flattened : a___flattened;

MODULE struct1_struct
  VAR
    b : boolean;

which results in a file a___flattenedSystem.smv: line 7: "flattened.i2_DOT_out" undefined in definition of flattened.arch_wiring at line 12.
I think, should be arch_wiring := (i2_DOT_out.b = i1_DOT_in.b);, so the flattening needs to map all individual elements of the struct / the MODULE.

Error: cannot find exported languages in dependencies: com.mbeddr.formal.req.tl_patterns.arch

The error in the title appears in the com.mbeddr.formal.languages build script in the com.mbeddr.formal.safety project. Specifically, it appears in these lines:

mps group com.mbeddr.formal.req.devkit 
  devkit fasten.requirements 
    load from $mbeddr.formal.req.code/devkits/fasten.requirements/fasten.requirements.devkit 
  

During the Gradle build this error appears:

[generate] 7 errors during generation:
 [generate] cannot find exported languages in dependencies: com.mbeddr.formal.req.tl_patterns.arch
 [generate] -- -- was input node: [modules] BuildMps_DevKit "fasten.requirements"[8380800190201521718] in com.mbeddr.formal.safety.build@0

MPS 2021.3.5 based release from 2022-01-09 desn't run

Hello,

I tried to open latest release after unzipping using fasten.bat and there was no sign of program's respond. It simply doesn't run.

I will be appreciated for a help.

Best regards,
Oleg.

Recursive flattening of connections with structs

Follow-up of #34:
Flattening of connections with structs need to be recursive to handle situations where struct members are again structs. This happens in one of our use-cases.

safety.GSN: Missing relationship from Strategy to Context

Constraining ocra expressions

Add constraints for ocra expressions (some of them redundant to nusmv expressions), to exclude them from polluting nusmv models. That is:

• Allow ocra expressions only in ocra roots (can be child of)
• Disallow redundant nusmv expressions in ocra

Add safety (gsn, req, spin) to FASTEn distribution

Currently, build-fasten-distribution.xml only bundles nuSMV languages and devkit. This is misleading, so I suggest to

• rename current build-fasten-distribution.xml to build-nusmv-distribution.xml and
• add real FASTEN distribution build that encompasses nusmv, spin, req, safety, etc.

Gradle exception: org.codehaus.groovy.runtime.GStringImpl cannot be cast to java.lang.String

Gradle build of master fails with error message Execution failed for task ':build_allScripts'. java.lang.ClassCastException: org.codehaus.groovy.runtime.GStringImpl cannot be cast to java.lang.String, see https://build.mbeddr.com/viewLog.html?buildId=269833&tab=buildResultsDiv&buildTypeId=Mbeddr2_Mbeddr_Gradle_Fasten_Build

Can't locate it more precisely, yet. Seems to be somewhere in build/scripts/build_all_scripts.xml, though.

Use NuSMV show_property and LTLSPEC names for unique mapping

Currently, the .source file for nusmv is generated but not used. By adding show_property to the .source file, nusmv outputs a list of the LTLSPEC given in the .smv file including the name (if given, e.g. by LTLSPEC NAME x := true).
By adding unique names to LTLSPECs, running nusmv on the .source file and updating the class AGResultsLifter to support the additional output, the lifting of nusmv results could be improved. This is especially beneficial for vacuity checks of contracts that belong to the same component.

Unable to change case expression's auto-generated "otherwise" basic expression

It seems that it is currently not possible to alter the auto-generated otherwise case in a case-expression when using the DSL for STATE-MACHINE. This prevents the default case from altering state variables. For instance it is not possible to decremented a counter/timer whenever none of the guard conditions are true. While the _040_state_machines documentation states that the DSL restricts the NuSMV base language, it doesn't mention this restriction.

Gradle Exception: Buildfile: build-nusmv-languages.xml does not exist

On commit:
8167cf2

When running:
./gradlew build_smv_languages

Full Exception:
> Task :build_smv_languages FAILED
Buildfile: /home/boakes/Projects/FASTEN/build/scripts/build-nusmv-languages.xml does not exist!
Build failed

Relevant code:
task build_smv_languages(type: BuildLanguages, dependsOn: [build_allScripts]) {
script new File("$buildDir/scripts/build-nusmv-languages.xml")
}

Gradle Version:
Gradle 5.5

Build time: 2019-06-28 17:36:05 UTC
Revision: 83820928f3ada1a3a1dbd9a6c0d47eb3f199378f

Kotlin: 1.3.31
Groovy: 2.5.4
Ant: Apache Ant(TM) version 1.9.14 compiled on March 12 2019
JVM: 11.0.5-ea (Ubuntu 11.0.5-ea+10-post-Ubuntu-0ubuntu1)
OS: Linux 5.3.0-23-generic amd64

Please let me know any other information you require.