Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add parser and model builder for JANI format #30

Merged
merged 7 commits into from
Feb 3, 2025
+7,010 −1
Merged

Add parser and model builder for JANI format #30

Changes from 1 commit
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
94a331f
Added parser and model builder for jani format
keb77 Dec 5, 2024
910e54f
Apply cargo fmt
keb77 Dec 19, 2024
f0a3cfa
Test module for jani
EnricoGhiorzi Jan 10, 2025
9a393db
Modified test function for jani
keb77 Jan 29, 2025
5c946c0
Modified test.jani
keb77 Jan 30, 2025
d610339
Formatting fix
keb77 Jan 31, 2025
327c092
Merge branch 'main' into fmt_jani
EnricoGhiorzi Feb 3, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Next Next commit
Loading
Loading status checks…
Added parser and model builder for jani format 
Signed-off-by: keb77 <[email protected]>
@keb77
keb77 committed Dec 5, 2024
commit 94a331fe85795bbec1b3625ea8648c367d85bed7
3 changes: 2 additions & 1 deletion Cargo.toml
View file
Original file line number Diff line number Diff line change
@@ -11,13 +11,14 @@ panic = "abort"

# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
[workspace]
members = ["scan_core", "scan_fmt_xml"]
members = ["scan_core", "scan_fmt_xml", "scan_fmt_jani"]

[workspace.dependencies]
log = "0.4.20"

[dependencies]
scan_fmt_xml = { version = "0.1.0", path = "scan_fmt_xml" }
scan_fmt_jani = { version = "0.1.0", path = "scan_fmt_jani" }
clap = { version = "4.4.14", features = ["derive"] }
env_logger = "0.11.0"
log = { workspace = true }
18 changes: 18 additions & 0 deletions scan_fmt_jani/Cargo.toml
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,18 @@
[package]
name = "scan_fmt_jani"
version = "0.1.0"
edition = "2021"

[build-dependencies]
cfgrammar = "0.13"
lrlex = "0.13"
lrpar = "0.13"

[dependencies]
cfgrammar = "0.13"
lrlex = "0.13"
lrpar = "0.13"
scan_core = { path="../scan_core" }
rand = "0.8"
thiserror = "1.0.56"
ordered-float = "4.2.2"
15 changes: 15 additions & 0 deletions scan_fmt_jani/build.rs
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,15 @@
use cfgrammar::yacc::YaccKind;
use lrlex::CTLexerBuilder;

fn main() {
CTLexerBuilder::new()
.lrpar_config(|ctp| {
ctp.yacckind(YaccKind::Grmtools)
.grammar_in_src_dir("jani_parser/jani_parser.y")
.unwrap()
})
.lexer_in_src_dir("jani_parser/jani_parser.l")
.unwrap()
.build()
.unwrap();
}
979 changes: 979 additions & 0 deletions scan_fmt_jani/src/jani_builder.rs
View file

Large diffs are not rendered by default.

466 changes: 466 additions & 0 deletions scan_fmt_jani/src/jani_parser.rs
View file

Large diffs are not rendered by default.

134 changes: 134 additions & 0 deletions scan_fmt_jani/src/jani_parser/jani_parser.l
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,134 @@
%%
\{ "{"
\} "}"
\[ "["
\] "]"
\: ":"
\, ","

\"bool\" "bool"
\"int\" "int"
\"real\" "real"
\"kind\" "kind"
\"bounded\" "bounded"
\"base\" "base"
\"lower\-bound\" "lower-bound"
\"upper\-bound\" "upper-bound"
\"clock\" "clock"
\"continuous\" "continuous"

\"constant\" "constant"
\"e\" "e"
\"π\" "π"
\"op\" "op"
\"ite\" "ite"
\"if\" "if"
\"then\" "then"
\"else\" "else"
\"(∨|∧|=|≠|<|≤|\+|\-|\*|%|\/|pow|log|⇒|>|≥)\" "BINARYOPERATOR"
\"left\" "left"
\"right\" "right"
\"(¬|floor|ceil)\" "UNARYOPERATOR"
\"exp\" "exp"
\"der\" "der"
\"var\" "var"

\"elements\" "elements"
\"syncs\" "syncs"
\"comment\" "comment"
\"automaton\" "automaton"
\"input\-enable\" "input-enable"
\"synchronise\" "synchronise"
\"result\" "result"

\"version\" "version"
\"author\" "author"
\"description\" "description"
\"doi\" "doi"
\"url\" "url"

\"name\" "name"
\"type\" "type"
\"transient\" "transient"
\"initial\-value\" "initial-value"
\"value\" "value"

\"jani\-version\" "jani-version"
\"metadata\" "metadata"
\"features\" "features"
\"actions\" "actions"
\"constants\" "constants"
\"variables\" "variables"
\"restrict\-initial\" "restrict-initial"
\"properties\" "properties"
\"automata\" "automata"
\"system\" "system"

\"locations\" "locations"
\"time\-progress\" "time-progress"
\"transient\-values\" "transient-values"
\"ref\" "ref"
\"initial\-locations\" "initial-locations"
\"edges\" "edges"
\"location\" "location"
\"action\" "action"
\"rate\" "rate"
\"destinations\" "destinations"
\"guard\" "guard"
\"probability\" "probability"
\"assignments\" "assignments"
\"index\" "index"

\"expression\" "expression"

\"lower\" "lower"
\"lower\-exclusive\" "lower-exclusive"
\"upper\" "upper"
\"upper\-exclusive\" "upper-exclusive"

\"steps\" "steps"
\"time\" "time"

\"filter\" "filter"
\"fun\" "fun"
\"(min|max|sum|avg|count|argmin|argmax)\" "FUNTYPE"
\"(∀|∃)\" "QUANTIFICATION"
\"values\" "values"
\"states\" "states"

\"(Pmin|Pmax)\" "PMINMAX"

\"(Emin|Emax)\" "EMINMAX"
\"accumulate\" "accumulate"
\"reach\" "reach"
\"step\-instant\" "step-instant"
\"time\-instant\" "time-instant"
\"reward\-instants\" "reward-instants"
\"instant\" "instant"

\"(Smin|Smax)\" "SMINMAX"

\"(U|W)\" "UNTIL"
\"step\-bounds\" "step-bounds"
\"time\-bounds\" "time-bounds"
\"reward\-bounds\" "reward-bounds"
\"bounds\" "bounds"

\"(initial|deadlock|timelock)\" "STATEPREDICATE"

\"distribution\" "distribution"
\"(DiscreteUniform|Bernoulli|Binomial|NegativeBinomial|Poisson|Geometric|Hypergeometric|ConwayMaxwellPoisson|Zipf|Uniform|Normal|FoldedNormal|LogNormal|Beta|Cauchy|Chi|ChiSquared|Erlang|Exponential|FisherSnedecor|Gamma|InverseGamma|Laplace|Pareto|Rayleigh|Stable|StudentT|Weibull|Triangular)\" "DISTRIBUTIONTYPE"
\"args\" "args"

\"(lts|dtmc|ctmc|mdp|ctmdp|ma|ta|pta|sta|ha|pha|sha)\" "MODELTYPE"
\"(arrays|datatypes|derived\-operators|edge\-priorities|functions|hyperbolic\-functions|named\-expressions|nondet\-selection|state\-exit\-rewards|tradeoff\-properties|trigonometric\-functions)\" "MODELFEATURE"

\"(\\.|[^"\\])*\" "STRING"
[+-]?\d+(\.\d*)? "NUMBER"
true "true"
false "false"
null "null"

[\t\n\r ]+ ;

. "UNMATCHED"
3,447 changes: 3,447 additions & 0 deletions scan_fmt_jani/src/jani_parser/jani_parser.y
View file

Large diffs are not rendered by default.

7 changes: 7 additions & 0 deletions scan_fmt_jani/src/lib.rs
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
//! Parser and model builder for SCAN's JANI specification format.
pub mod jani_parser;
pub mod jani_builder;

pub use jani_parser::Parser;
pub use jani_builder::ModelBuilder;
347 changes: 347 additions & 0 deletions scan_fmt_jani/tests/die.jani
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,347 @@
{
"jani-version": 1,
"name": "die.jani",
"type": "dtmc",
"features": [ "derived-operators" ],
"variables": [
{
"name": "s",
"type": "int"
},
{
"name": "d",
"type": "int",
"initial-value": 0
}
],
"properties": [
{
"name": "Probability to throw a six",
"expression": {
"op": "filter",
"fun": "max",
"states": { "op": "initial" },
"values": {
"op": "Pmin",
"exp": {
"op": "U",
"left": true,
"right": {
"op": "∧",
"left": {
"op": "=",
"left": "s",
"right": 7
},
"right": {
"op": "=",
"left": "d",
"right": 6
}
}
}
}
}
},
{
"name": "Expected number of coin flips",
"expression": {
"op": "filter",
"fun": "max",
"states": { "op": "initial" },
"values": {
"op": "Emin",
"accumulate": [ "steps" ],
"exp": 1,
"reach": {
"op": "=",
"left": "s",
"right": 7
}
}
}
}
],
"automata": [
{
"name": "die",
"locations": [{ "name": "l" }],
"initial-locations": ["l"],
"edges": [
{
"location": "l",
"guard": {
"exp": {
"op": "=",
"left": "s",
"right": 0
}
},
"destinations": [
{
"location": "l",
"probability": { "exp": 0.5 },
"assignments": [
{
"ref": "s",
"value": 1
}
]
},
{
"location": "l",
"probability": { "exp": 0.5 },
"assignments": [
{
"ref": "s",
"value": 2
}
]
}
]
},
{
"location": "l",
"guard": {
"exp": {
"left": "s",
"op": "=",
"right": 1
}
},
"destinations": [
{
"location": "l",
"probability": { "exp": 0.5 },
"assignments": [
{
"ref": "s",
"value": 3
}
]
},
{
"location": "l",
"probability": { "exp": 0.5 },
"assignments": [
{
"ref": "s",
"value": 4
}
]
}
]
},
{
"location": "l",
"guard": {
"exp": {
"left": "s",
"op": "=",
"right": 2
}
},
"destinations": [
{
"location": "l",
"probability": { "exp": 0.5 },
"assignments": [
{
"ref": "s",
"value": 5
}
]
},
{
"location": "l",
"probability": { "exp": 0.5 },
"assignments": [
{
"ref": "s",
"value": 6
}
]
}
]
},
{
"location": "l",
"guard": {
"exp": {
"left": "s",
"op": "=",
"right": 3
}
},
"destinations": [
{
"location": "l",
"probability": { "exp": 0.5 },
"assignments": [
{
"ref": "s",
"value": 1
}
]
},
{
"location": "l",
"probability": { "exp": 0.5 },
"assignments": [
{
"ref": "s",
"value": 7
},
{
"ref": "d",
"value": 1
}
]
}
]
},
{
"location": "l",
"guard": {
"exp": {
"left": "s",
"op": "=",
"right": 4
}
},
"destinations": [
{
"location": "l",
"probability": { "exp": 0.5 },
"assignments": [
{
"ref": "s",
"value": 7
},
{
"ref": "d",
"value": 2
}
]
},
{
"location": "l",
"probability": { "exp": 0.5 },
"assignments": [
{
"ref": "s",
"value": 7
},
{
"ref": "d",
"value": 3
}
]
}
]
},
{
"location": "l",
"guard": {
"exp": {
"left": "s",
"op": "=",
"right": 5
}
},
"destinations": [
{
"location": "l",
"probability": { "exp": 0.5 },
"assignments": [
{
"ref": "s",
"value": 7
},
{
"ref": "d",
"value": 4
}
]
},
{
"location": "l",
"probability": { "exp": 0.5 },
"assignments": [
{
"ref": "s",
"value": 7
},
{
"ref": "d",
"value": 5
}
]
}
]
},
{
"location": "l",
"guard": {
"exp": {
"left": "s",
"op": "=",
"right": 6
}
},
"destinations": [
{
"location": "l",
"probability": { "exp": 0.5 },
"assignments": [
{
"ref": "s",
"value": 2
}
]
},
{
"location": "l",
"probability": { "exp": 0.5 },
"assignments": [
{
"ref": "s",
"value": 7
},
{
"ref": "d",
"value": 6
}
]
}
]
},
{
"location": "l",
"guard": {
"exp": {
"left": "s",
"op": "=",
"right": 7
}
},
"destinations": [
{
"location": "l",
"assignments": [
{
"ref": "s",
"value": 7
}
]
}
]
}
]

}
],
"system": {
"elements": [ { "automaton": "die" } ]
}
}
1,211 changes: 1,211 additions & 0 deletions scan_fmt_jani/tests/dining_crypt3.jani
View file

Large diffs are not rendered by default.

204 changes: 204 additions & 0 deletions scan_fmt_jani/tests/test.jani
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,204 @@
{
"jani-version": 1,
"name": "test.jani",
"type": "lts",
"constants": [
{
"name": "c1",
"type": "int",
"value": 10
},
{
"name": "c2",
"type": "bool",
"value": true
}
],
"variables": [
{
"name": "v1",
"type": "int",
"initial-value": 15
},
{
"name": "v2",
"type": "bool",
"initial-value": false
}
],
"actions": [ { "name": "a1" }, { "name": "a2" }, { "name": "a3" }, { "name": "a4" }, { "name": "a5" }, { "name": "a" } ],
"automata": [
{
"name": "test",
"locations": [{ "name": "l" } , { "name": "o" } , { "name": "c" } ],
"variables": [
{
"name": "b",
"type": "bool",
"initial-value": false
},
{
"name": "i",
"type": "int",
"initial-value": 0
}
],
"initial-locations": ["l"],
"edges": [
{
"location": "l",
"action": "a1",
"guard": {
"exp": {
"op": "¬",
"exp": "b"
}
},
"destinations": [
{
"location": "o",
"assignments": [
{
"ref": "b",
"value": true
}
]
}
]
},
{
"location": "o",
"action": "a2",
"guard": {
"exp": {
"op": "∧",
"left": "b",
"right": {
"op": "=",
"left": "i",
"right": 0
}
}
},
"destinations": [
{
"location": "c",
"assignments": [
{
"ref": "i",
"value": 1
}
]
}
]
},
{
"location": "c",
"action": "a3",
"guard": {
"exp": {
"op": "=",
"left": "i",
"right": 1
}
},
"destinations": [
{
"location": "l"
}
]
},
{
"location": "l",
"action": "a4",
"guard": {
"exp": {
"op": "∧",
"left": {
"op": "<",
"left": "c1",
"right": "v1"
},
"right": {
"op": "¬",
"exp": "v2"
}
}
},
"destinations": [
{
"location": "o",
"assignments": [
{
"ref": "v1",
"value": 5
}
]
}
]
},
{
"location": "o",
"action": "a5",
"guard": {
"exp": {
"op": "∧",
"left": "c2",
"right": "v2"
}
},
"destinations": [
{
"location": "c",
"assignments": [
{
"ref": "i",
"value": 0
}
]
}
]
}
]
},
{
"name": "tset",
"locations": [{ "name": "l" }],
"initial-locations": ["l"],
"edges": [
{
"location": "l",
"action": "a",
"guard": {
"exp": {
"op": "∧",
"left": {
"op": "¬",
"exp": "v2"
},
"right": {
"op": "<",
"left": "v1",
"right": "c1"
}
}
},
"destinations": [
{
"location": "l",
"assignments": [
{
"ref": "v2",
"value": true
}
]
}
]
}
]
}
],
"system": {
"elements": [ { "automaton": "test" }, { "automaton": "tset" } ]
}
}
158 changes: 158 additions & 0 deletions scan_fmt_jani/tests/test2.jani
View file
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I managed to run this test: parse the jani file, build the channel system, and run random actions on it. I would expect the channel system to terminate (meaning to get to a state in which no more transitions are possible), instead it seems to run forever. Do you have any idea why? Same applies for test.jani.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I believe the problem is caused by the issue we discussed during our last meeting regarding how global variables are handled: in a program graph where a transition has a guard containing global variables, the system continuously checks for updates to those variables (which is done through other transitions). This should be why test.jani doesn't terminate. test2.jani, on the other hand, is structured in a way that should terminate, but it probably gets caught in a loop for similar reasons because the test function always chooses the first element in the possible transitions list. I modified the test function to select random transitions instead and it terminates as expected.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Your last commit has no sign-off and it fails the automated test. Could you fix that?

Also, would it be possible to modify test.jani so that it eventually terminates too? That would make a good automated test.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

All done!

Original file line number Diff line number Diff line change
@@ -0,0 +1,158 @@
{
"jani-version": 1,
"name": "test.jani",
"type": "lts",
"constants": [
{
"name": "c1",
"type": "int",
"value": 10
},
{
"name": "c2",
"type": "bool",
"value": true
}
],
"variables": [
{
"name": "v1",
"type": "int",
"initial-value": 15
},
{
"name": "v2",
"type": "bool",
"initial-value": false
}
],
"actions": [ { "name": "a1" }, { "name": "a2" }, { "name": "a3" } ],
"automata": [
{
"name": "test",
"locations": [{ "name": "l" } , { "name": "o" } , { "name": "c" } ],
"variables": [
{
"name": "b",
"type": "bool",
"initial-value": false
},
{
"name": "i",
"type": "int",
"initial-value": 5
}
],
"initial-locations": ["l"],
"edges": [
{
"location": "l",
"action": "a1",
"guard": {
"exp": {
"op": "=",
"left": "i",
"right": 5
}
},
"destinations": [
{
"location": "o",
"assignments": [
{
"ref": "b",
"value": true
}
]
}
]
},
{
"location": "o",
"action": "a2",
"guard": {
"exp": {
"op": "∧",
"left": "b",
"right": {
"op": "=",
"left": "v1",
"right": 5
}
}
},
"destinations": [
{
"location": "c",
"assignments": [
{
"ref": "v2",
"value": true
},
{
"ref": "i",
"value": 10
}
]
}
]
}
]
},
{
"name": "tset",
"locations": [{ "name": "l" } , { "name": "o" } , { "name": "c" } ],
"variables": [
{
"name": "b",
"type": "bool",
"initial-value": true
},
{
"name": "i",
"type": "int",
"initial-value": 15
}
],
"initial-locations": ["l"],
"edges": [
{
"location": "l",
"action": "a1",
"guard": {
"exp": "b"
},
"destinations": [
{
"location": "o",
"assignments": [
{
"ref": "i",
"value": 5
}
]
}
]
},
{
"location": "o",
"action": "a2",
"destinations": [
{
"location": "c",
"assignments": [
{
"ref": "v1",
"value": 5
}
]
}
]
}
]
}
],
"system": {
"elements": [ { "automaton": "test" }, { "automaton": "tset" } ]
}
}