inputs.ka invalid when contact map overconstraints observables defined

[hmedina]

KaSim will produce an inputs.ka file meant as a witness and recipe for reproducing the simulation, with all modifications, definitions, and parameters. It will also include the contact map, as derived from static analysis of the rules.

However, the rules may not establish bonds declared in observables. A user can define observables not reachable; it is a user's Kappa-given right. And observables are declared as variables. So a variable can be declared using a bond not declared by the contact map; KaSim objects to the witness file it just generated...

MWE, model.ka:

%agent: A(a, b)		%init: 2 A()
'a++' A(a[./1]), A(a[./1]) @ 1
'a--' A(a[1/.]), A(a[1/.]) @ 1
%obs: 'a' |A(a[1]), A(a[1])|
%obs: 'b' |A(b[1]), A(b[1])|
%mod: [E] = 1 do $STOP ;

For which inputs.ka:

// "uuid" : "214744874"
%def: "seed" "385632745"
%def: "dumpIfDeadlocked" "true"
%def: "maxConsecutiveClash" "3"
%def: "progressBarSize" "70"
%def: "progressBarSymbol" "#"
%def: "plotPeriod" "1" "t.u."
%def: "outputFileName" "data.csv"

%agent: A(a[a.A] b)

%var:/*0*/ 'a' |A(a[1]), A(a[1])|
%var:/*1*/ 'b' |A(b[1]), A(b[1])|
%plot: [T]
%plot: a
%plot: b

'a++' A(a[./1]), A(a[./1]) @ 1
'a--' A(a[1/.]), A(a[1/.]) @ 1

/*0*/%mod: ([E] = 1) do $STOP ; repeat [false]

%init: 2 A(a[.] b[.])

%mod: [E] = 1 do $STOP;

And so:

$ KaSim -i inputs.ka -d foo
Parsing inputs.ka...
done
+ simulation parameters
+ Sanity checks
File "inputs.ka", line 13, characters 29-30:
Forbidden link to a b.A from signature declaration

Concretely, in the user's model, observable b is unreachable as there is no rule to generate its bond; but the witness file further adds the constraints of the contact map typing, which now makes observable b an error. Reproducing this simulation requires editing the witness file manually to add/remove rules/constraints ...

In a user-given file, if the user gives a contact map, then the observables should be constrained by it. But in this case, for the witness file, the variable defining the observable should not. It seems to me there should be a parameter, a definition, that marks a file as a witness file.

[pirbo]

The cheapest thing to do is "to take into account bound type explicitly declared in an observable when inferring the contact map" but it makes it less accurate. A more expensive thing to do is to replace the unreachable patterns by 0 in the witness file.

[feret]

Is it the same for dead rules ? (When a bond occurs in the rhs of a dead rule and not in the contact map ?). To my opinion, this should be warning only, but should not block execution. All the more so since, observables are not problematic. For dead rules, it is more difficult but we can rely on KaSa.

…

Le 15 juil. 2020 à 11:51, Pierre Boutillier ***@***.***> a écrit : The cheapest thing to do is "to take into account bound type explicitly declared in an observable when inferring the contact map" but it makes it less accurate. A more expensive thing to do is to replace the unreachable patterns by 0 in the witness file. — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#625 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AACG3MZA6BEFTMV4BWLKPV3R3V33DANCNFSM4OXOVLQA>.

[hmedina]

When using WebSim, KaSa also throws exceptions and exits when encountering bonds used in observables that are not possible. Line 107 is an observable.

:: this link can never be formed; exception: Exit

file_name: core/KaSa_rep/frontend/preprocess.ml; message: line 1042, File "model.ka", line 107, characters 28-29:: ; exception: Exit