coco-team / cocosim2 Goto Github PK

The modifications to the contract Subsystem of inputs connections to the contract blocks (assume, guarantee, mode ..) are discarded when the model is closed and opened again. There is a callback called each time when the model is opened which connects inputs again.

This is something breaking the user modification to the Contract Subsystem. The callback should be called only when the user has specified number of assumptions ... and hit ok or apply in the validator dialogue box.

I tested it, but there was an error that "lustrec failed for model "
In the debug information, it said that "fatal error: exception invalid_argument("equal: abstract value")"

I saw a function view generated cocospec in the tutorial video, but I can't find on mine. Was it used for importing cocospec file generated by FRET since I don't see any function to do the job.

Hi Mudathir,
Why you force specific convention in names in your Blocks mapping.
See nameSet{i} = Utils.name_format(blockSet{i}); in:
function [nodeNameToBlockNameMap] = getBlocksMapping()
%get blocks names from nodes names
%ToDo: refactor this process with the Java translator
blockSet = find_system(bdroot(gcs),'LookUnderMasks', 'on');
nameSet = cell(length(blockSet), 1);
for i = 1 : length(blockSet)
nameSet{i} = Utils.name_format(blockSet{i});
nameSet{i} = strrep(nameSet{i}, '/','_');
end
nodeNameToBlockNameMap = containers.Map(nameSet, blockSet);
end

This function is used to replace node names with their block names in displaying counterExamples in tables or HTML tables, Why not using the mapping file so it can be generic?
I am using the different convention in naming Lustre names, but using traceability should be OK. As everything is stored with Original PAth.

When validator connects contract inputs to assume, guarantees and modes. The outputs of the components subject to verification should not be connected with Assume and Require. As they cannot be mentioning this outputs.

If it is difficult to differentiate between input signals and the output signal of the component to verify in Validator callback. The user should be aware of this issue and remove by himself these signals, if not Kind2 will complain.

The following StateLabels are not supported by the chartParser.
Having "/" in front of state name:
A1a/ en:a = 1

I am wondering why the OuterTransitions in Junction is encapsulated in "Destination":
transitionStruct.Destination = buildDestinationStruct(transitions(i));
junctionStruct.OuterTransitions = [junctionStruct.OuterTransitions transitionStruct];

But in State is not:
transitionStruct = buildDestinationStruct(transitions(i));
stateStruct.OuterTransitions = [stateStruct.OuterTransitions transitionStruct];

Could you please remove Destination from transitionStruct in junction case, that will make more sense to have a common grammar for all OuterTransitions.

I wanted to make the modification but it may break Paul translator of Stateflow. So you need to adapt his code to access directly the OuterTransitions struct without going throw Destination.
BTW there is another Destination field in OuterTransition struct, this one is correct.

Thanks,
Hamza

'A/
en:
x = x([3 1 2]) + 1;'

stateAction = edu.uiowa.chart.state.StateParser.parse(state.LabelString);
stateStruct.Actions.Entry{1} =
'
i=3;
x=x([312])+1;'

space is "[3 1 2]" was removed. Which changes the value of the action.

(Debug) Error using displayVerificationResults>initializeVerificationVisualization (line 55)
Invalid inputs specified for method 'get'
Error in displayVerificationResults (line 10)
initializeVerificationVisualization(verificationResults);
Error in cocoSpecKind2 (line 93)
displayVerificationResults(verificationResults, compositionalMap);

Error using displayVerificationResults>initializeVerificationVisualization (line 57)
Invalid inputs specified for method 'removeDialogControl'
Error in displayVerificationResults (line 10)
initializeVerificationVisualization(verificationResults);
Error in cocoSpecKind2 (line 93)
displayVerificationResults(verificationResults, compositionalMap);
Error in toLustreVerify (line 78)
status = cocoSpecKind2(nom_lustre_file, mapping_file, kind2_out);
Error in verifyMenu>kindCallback (line 50)
toLustreVerify(model_full_path);

There is an error when running on ubuntu 18.04.
I dont know how to install using source code (that .zip file), so I download the .mltbx file and clicked it to install. But on Windows there is no such error.

Why there are two files with the same content.
I found that Kind.sls is the one used by Validator callback, so any modification to CocosimSpecification will not impact the callback.
Can we have one and remove Kind.slx from contract_callback.m (lines 180) and use CocosimSpecification.slx?

Thanks,

Error using displayVerificationResults>createMaskAction (line 181)
Dialog control with name 'Display_counter_example_as_signals' already exists
Error in displayVerificationResults>addCounterExampleOptions (line 155)
createMaskAction('Display counter example as signals', cexSignals, propertyStruct.originPath);
Error in displayVerificationResults>displayPropertyResult (line 131)
addCounterExampleOptions(propertyStruct, resultIndex, propertyIndex);
Error in displayVerificationResults>displayVerificationResult (line 33)
ancestorColor = displayPropertyResult(verificationResult.properties{i},ancestorColor, resultIndex, i);
Error in displayVerificationResults (line 12)
displayVerificationResult(verificationResults,compositionalMap, analysisIndex);
Error in cocoSpecKind2 (line 93)
displayVerificationResults(verificationResults, compositionalMap);