use std::str::FromStr;
use crate::ast::*;
grammar;
match {
r"\s+" => {}, // skip whitespace
r"//[^\n\r]*[\n\r]*" => {}, // skip line comments
} else {
_ // default tokenization for everything else
}
Comma<T>: Vec<T> = {
<mut v:(<T> ",")*> <e:T?> => match e {
None => v,
Some(e) => {
v.push(e);
v
}
}
};
pub DTMC: DTMCAst = {
"dtmc" <items:TopLevelItem*> => {
let mut modules = Vec::new();
let mut constants = Vec::new();
let mut renamed_modules = Vec::new();
let mut labels = Vec::new();
for (mut item_modules, mut item_constants, mut item_renamed_modules, mut item_labels) in items {
modules.append(&mut item_modules);
constants.append(&mut item_constants);
renamed_modules.append(&mut item_renamed_modules);
labels.append(&mut item_labels);
}
DTMCAst { modules, constants, renamed_modules, labels, properties: Vec::new() }
}
};
pub DTMCProps: (Vec<(String, ConstDecl)>, Vec<Property>) = {
<items:PropTopLevelItem*> => {
let mut constants = Vec::new();
let mut properties = Vec::new();
for (mut item_constants, mut item_properties) in items {
constants.append(&mut item_constants);
properties.append(&mut item_properties);
}
(constants, properties)
}
};
PropTopLevelItem: (Vec<(String, ConstDecl)>, Vec<Property>) = {
<constant:ConstDeclStmt> => (vec![constant], vec![]),
<property:PropertyStmt> => (vec![], vec![property]),
};
TopLevelItem: (Vec<Module>, Vec<(String, ConstDecl)>, Vec<RenamedModule>, Vec<LabelDecl>) = {
<module:Module> => (vec![module], vec![], vec![], vec![]),
<renamed_module:RenamedModuleDecl> => (vec![], vec![], vec![renamed_module], vec![]),
<constant:ConstDeclStmt> => (vec![], vec![constant], vec![], vec![]),
<label:LabelDeclStmt> => (vec![], vec![], vec![], vec![label]),
<IgnoredRewardsBlock> => (vec![], vec![], vec![], vec![]),
<IgnoredFormulaDecl> => (vec![], vec![], vec![], vec![]),
};
StringLit: String = {
r#""[^"\r\n]*""# => {
let raw = <>;
raw[1..raw.len()-1].to_string()
}
};
IgnoredFormulaDecl: () = {
"formula" <Ident> "=" <Expr> ";" => ()
};
LabelDeclStmt: LabelDecl = {
"label" <name:StringLit> "=" <expr:Expr> ";" => LabelDecl { name, expr }
};
RewardItem: () = {
"[" <Comma<Ident>> "]" <Expr> ":" <Expr> ";" => (),
<Expr> ":" <Expr> ";" => (),
};
IgnoredRewardsBlock: () = {
"rewards" <StringLit?> <RewardItem*> "endrewards" => ()
};
ConstTypeDecl: ConstType = {
"bool" => ConstType::Bool,
"int" => ConstType::Int,
"float" => ConstType::Float,
"double" => ConstType::Float,
};
ConstDeclStmt: (String, ConstDecl) = {
"const" <const_type:ConstTypeDecl> <name:Ident> "=" <value:Expr> ";"
=> (name, ConstDecl { const_type, value: Some(value) }),
"const" <const_type:ConstTypeDecl> <name:Ident> ";"
=> (name, ConstDecl { const_type, value: None }),
};
PropertyStmt: Property = {
"P" "=" "?" "[" <psi:PathFormulaExpr> "]"
=> Property::ProbQuery(psi),
"R" "{" <_reward_name:StringLit> "}" "=" "?" "[" <psi:PathFormulaExpr> "]"
=> Property::RewardQuery(psi),
"R" "=" "?" "[" <psi:PathFormulaExpr> "]"
=> Property::RewardQuery(psi),
};
PathFormulaExpr: PathFormula = {
"X" <phi:PathStateExpr> => PathFormula::Next(phi),
"F" <phi:PathStateExpr> => PathFormula::Until {
lhs: Box::new(Expr::BoolLit(true)),
rhs: phi,
bound: None,
},
"F" "<=" <k:BoundExpr> <phi:PathStateExpr> => PathFormula::Until {
lhs: Box::new(Expr::BoolLit(true)),
rhs: phi,
bound: Some(k),
},
<lhs:PathStateExpr> "U" "<=" <k:BoundExpr> <rhs:PathStateExpr> => PathFormula::Until {
lhs,
rhs,
bound: Some(k),
},
<lhs:PathStateExpr> "U" <rhs:PathStateExpr> => PathFormula::Until {
lhs,
rhs,
bound: None,
},
};
PathStateExpr: Box<Expr> = {
<label:StringLit> => Box::new(Expr::LabelRef(label)),
<Expr>,
};
BoundExpr: Box<Expr> = {
r"[0-9]+" => Box::new(Expr::IntLit(i32::from_str(<>).unwrap())),
<var:Ident> => Box::new(Expr::Ident(var)),
"(" <e:Expr> ")" => e,
};
Module: Module = {
"module" <name:Ident> <local_vars:VarDecl*> <commands:Command*> "endmodule"
=> Module { name, local_vars, commands }
};
RenamePair: (String, String) = {
<from:Ident> "=" <to:Ident> => (from, to),
};
RenamedModuleDecl: RenamedModule = {
"module" <name:Ident> "=" <base:Ident> "[" <renames:Comma<RenamePair>> "]" "endmodule"
=> RenamedModule { name, base, renames }
};
VarDecl: VarDecl = {
<name:Ident> ":" "bool" "init" <init:Expr> ";"
=> VarDecl { name, var_type: VarType::Bool, init },
<name:Ident> ":" "bool" ";"
=> VarDecl { name, var_type: VarType::Bool, init: Box::new(Expr::BoolLit(false)) },
<name:Ident> ":" "[" <lo:Expr> ".." <hi:Expr> "]" "init" <init:Expr> ";"
=> VarDecl { name, var_type: VarType::BoundedInt { lo, hi }, init },
<name:Ident> ":" "[" <lo:Expr> ".." <hi:Expr> "]" ";" => {
let init = lo.clone();
VarDecl { name, var_type: VarType::BoundedInt { lo, hi }, init }
},
};
Command: Command = {
"[" <labels:Comma<Ident>> "]" <guard:Expr> "->" <updates:UpdateList> ";"
=> Command { labels, guard, updates }
};
UpdateList: Vec<ProbUpdate> = {
<mut v:(<ProbUpdate> "+")*> <e:ProbUpdate> => { v.push(e); v },
};
ProbUpdate: ProbUpdate = {
<prob:Expr> ":" <assignments:AssignmentList>
=> ProbUpdate { prob, assignments },
<assignments:AssignmentList>
=> ProbUpdate { prob: Box::new(Expr::FloatLit(1.0)), assignments }
};
AssignmentList: Vec<Box<Expr>> = {
<mut v:(<Assignment> "&")*> <e:Assignment> => { v.push(e); v }
};
Assignment: Box<Expr> = {
"(" <var:Ident> "'" "=" <e:Expr> ")"
=> Box::new(Expr::BinOp {
lhs: Box::new(Expr::PrimedIdent(var)),
op: BinOp::Eq,
rhs: e,
})
};
PrimedIdentExpr: Box<Expr> = {
<var:Ident> "'" => Box::new(Expr::PrimedIdent(var)),
};
Ident: String = {
r"[a-zA-Z_][a-zA-Z0-9_]*" => <>.to_string()
};
Expr: Box<Expr> = {
<cond:OrExpr> "?" <then_branch:Expr> ":" <else_branch:Expr>
=> Box::new(Expr::Ternary { cond, then_branch, else_branch }),
<PrimedIdentExpr>,
<OrExpr>
};
OrOp: BinOp = {
"||" => BinOp::Or,
"|" => BinOp::Or,
};
AndOp: BinOp = {
"&&" => BinOp::And,
"&" => BinOp::And,
};
EqOp: BinOp = {
"=" => BinOp::Eq,
"!=" => BinOp::Neq,
};
CmpOp: BinOp = {
"<" => BinOp::Lt,
"<=" => BinOp::Leq,
">" => BinOp::Gt,
">=" => BinOp::Geq,
};
AddOp: BinOp = {
"+" => BinOp::Plus,
"-" => BinOp::Minus,
};
MulOp: BinOp = {
"*" => BinOp::Mul,
"/" => BinOp::Div,
};
OrExpr: Box<Expr> = {
<head:AndExpr> <tail:(<OrOp> <AndExpr>)*> => {
let mut expr = head;
for (op, rhs) in tail {
expr = Box::new(Expr::BinOp { lhs: expr, op, rhs });
}
expr
}
};
AndExpr: Box<Expr> = {
<head:EqExpr> <tail:(<AndOp> <EqExpr>)*> => {
let mut expr = head;
for (op, rhs) in tail {
expr = Box::new(Expr::BinOp { lhs: expr, op, rhs });
}
expr
}
};
EqExpr: Box<Expr> = {
<head:CmpExpr> <tail:(<EqOp> <CmpExpr>)*> => {
let mut expr = head;
for (op, rhs) in tail {
expr = Box::new(Expr::BinOp { lhs: expr, op, rhs });
}
expr
}
};
CmpExpr: Box<Expr> = {
<head:AddExpr> <tail:(<CmpOp> <AddExpr>)*> => {
let mut expr = head;
for (op, rhs) in tail {
expr = Box::new(Expr::BinOp { lhs: expr, op, rhs });
}
expr
}
};
AddExpr: Box<Expr> = {
<head:MulExpr> <tail:(<AddOp> <MulExpr>)*> => {
let mut expr = head;
for (op, rhs) in tail {
expr = Box::new(Expr::BinOp { lhs: expr, op, rhs });
}
expr
}
};
MulExpr: Box<Expr> = {
<head:UnaryExpr> <tail:(<MulOp> <UnaryExpr>)*> => {
let mut expr = head;
for (op, rhs) in tail {
expr = Box::new(Expr::BinOp { lhs: expr, op, rhs });
}
expr
}
};
UnaryExpr: Box<Expr> = {
"!" <e:UnaryExpr> => Box::new(Expr::UnaryOp { op: UnOp::Not, operand: e }),
"-" <e:UnaryExpr> => Box::new(Expr::UnaryOp { op: UnOp::Neg, operand: e }),
<PrimaryExpr>
};
PrimaryExpr: Box<Expr> = {
r"[0-9]+" => Box::new(Expr::IntLit(i32::from_str(<>).unwrap())),
r"[0-9]+\.[0-9]+" => Box::new(Expr::FloatLit(f64::from_str(<>).unwrap())),
"false" => Box::new(Expr::BoolLit(false)),
"true" => Box::new(Expr::BoolLit(true)),
<var:Ident> => Box::new(Expr::Ident(var)),
"(" <Expr> ")",
};