Skip to content

Commit

Permalink
Merge pull request #34 from ybbh/main
Browse files Browse the repository at this point in the history
sedeve-kit
  • Loading branch information
ybbh authored Jun 28, 2024
2 parents e1ee3a4 + b111422 commit f8c2de5
Show file tree
Hide file tree
Showing 6 changed files with 73 additions and 10 deletions.
5 changes: 4 additions & 1 deletion doc/how_to_start.md
Original file line number Diff line number Diff line change
Expand Up @@ -64,4 +64,7 @@ During testing, we add invariants to assert the correctness of our assumptions.

## Example
[Two-Phase Commit Protocol(2PC)](https://en.wikipedia.org/wiki/Two-phase_commit_protocol) is a atomic commit protocol.
The example of using this kit to develop 2PC could be found at [this repo](https://github.com/scuptio/example-2pc).
The example of using this kit to develop 2PC could be found at [this repo](https://github.com/scuptio/example-2pc).

[Raft](https://raft.github.io/) consensus algorithm.
We implement Raft[repo](https://github.com/scuptio/scupt-raft)
38 changes: 35 additions & 3 deletions src/action/serde_json_util.rs
Original file line number Diff line number Diff line change
@@ -1,12 +1,13 @@
use scupt_util::error_type::ET;
use scupt_util::error_type::ET::NoneOption;
use scupt_util::res::Res;
use serde_json::{Map, Value};
use serde_json::{json, Map, Value};
use tracing::error;

pub fn json_util_map_get_value(map: &Map<String, Value>, key: &str) -> Res<Value> {
match map.get(key) {
None => {
error!("map get string, cannot find key {}, in map {:?}", key, map);
error!("map get value, cannot find key {}, in map {:?}", key, map);
Err(ET::NoneOption)
}
Some(v) => { Ok(v.clone()) }
Expand All @@ -16,7 +17,7 @@ pub fn json_util_map_get_value(map: &Map<String, Value>, key: &str) -> Res<Value
pub fn json_util_map_get_value_ref<'a>(map: &'a Map<String, Value>, key: &str) -> Res<&'a Value> {
match map.get(key) {
None => {
error!("map get string, cannot find key {}", key);
error!("map get value reference, cannot find key {}", key);
Err(ET::NoneOption)
}
Some(v) => { Ok(v) }
Expand Down Expand Up @@ -49,3 +50,34 @@ pub fn json_util_map_get_i64(map: &Map<String, Value>, key: &str) -> Res<i64> {
}
}

#[test]
fn test_serde_json_util() {
let j = json!({
"i64":1,
"string":"s",
"value" : {
"x" : 1,
"y" : 2
}
});

let map = j.as_object().unwrap();

// OK
assert_eq!(Ok(1), json_util_map_get_i64(map, "i64"));
assert_eq!(Ok("s".to_string()), json_util_map_get_string(map, "string"));
let r1 = json_util_map_get_value(map, "value");
assert!(r1.is_ok());
let r1 = json_util_map_get_value_ref(map, "value");
assert!(r1.is_ok());

// non exist
assert_eq!(Err(NoneOption), json_util_map_get_i64(map, "non_exist"));
assert_eq!(Err(NoneOption), json_util_map_get_string(map, "non_exist"));
assert_eq!(Err(NoneOption), json_util_map_get_value(map, "non_exist"));
assert_eq!(Err(NoneOption), json_util_map_get_value(map, "non_exist"));

// wrong types
assert_eq!(Err(NoneOption), json_util_map_get_i64(map, "string"));
assert_eq!(Err(NoneOption), json_util_map_get_string(map, "i64"));
}
4 changes: 2 additions & 2 deletions src/trace/action_from_state_db.rs
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@ use crate::action::action_message::ActionMessage;
use crate::action::tla_actions::TLAActionSeq;
use crate::action::tla_typed_value::get_typed_value;
use crate::trace::action_graph::ActionGraph;
use crate::trace::read_json::read_from_dict_json;
use crate::trace::read_json::tla_constant_mapping;
use crate::trace::trace_db_interm::{Stage, TraceDBInterm};

pub fn read_actions<F>(path: String, dict: &HashMap<String, Value>, fn_handle_action: &F)
Expand All @@ -39,7 +39,7 @@ pub fn read_action_message<M: MsgTrait + 'static, F>(
) -> Res<()>
where F: Fn(ActionMessage<M>) -> Res<()>
{
let map = read_from_dict_json(Some(path_map.clone())).unwrap();
let map = tla_constant_mapping(Some(path_map.clone())).unwrap();
let f = |v: Value| -> Res<()> {
let tla_action_seq = TLAActionSeq::from(v.clone())?;
for vec in [tla_action_seq.actions(), tla_action_seq.states()] {
Expand Down
30 changes: 29 additions & 1 deletion src/trace/read_json.rs
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,11 @@ use scupt_util::error_type::ET;
use scupt_util::res::Res;
use serde_json::Value;

pub fn read_from_dict_json(opt_path: Option<String>) -> Res<HashMap<String, Value>> {

/// read a json file,
/// construct a mapping from TLA+ constant to programming language typed value
/// (Rust for example, by json Value)
pub fn tla_constant_mapping(opt_path: Option<String>) -> Res<HashMap<String, Value>> {
let path = match opt_path {
Some(p) => { p }
None => { return Ok(HashMap::new()); }
Expand Down Expand Up @@ -35,3 +39,27 @@ pub fn read_from_dict_json(opt_path: Option<String>) -> Res<HashMap<String, Valu
};
Ok(dict)
}


mod tests {
use std::collections::HashMap;
use std::fs;
use serde_json::json;
use uuid::Uuid;
use crate::trace::read_json::tla_constant_mapping;

#[test]
fn test_constant_mapping() {
assert_eq!(Ok(HashMap::new()), tla_constant_mapping(None));
assert!(tla_constant_mapping(Some("/tmp/json.non_existing_file".to_string())).is_err());
let invalid_json =r#"{ "x": }"#;
let path1 = format!("/tmp/test_const_mapping_valid_json.{}.json", Uuid::new_v4().to_string());
fs::write(path1.clone(), invalid_json).unwrap();
assert!(tla_constant_mapping(Some(path1)).is_err());

let array_json = json!([1, 2, 3]);
let path2 = format!("/tmp/test_const_mapping_array_json.{}.json", Uuid::new_v4().to_string());
fs::write(path2.clone(), array_json.to_string()).unwrap();
assert!(tla_constant_mapping(Some(path2)).is_err());
}
}
4 changes: 2 additions & 2 deletions src/trace/test_state_db_to_case.rs
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ mod test {

use crate::data::path::_test::_test_data_path;
use crate::trace::gen_case::{DataInput, gen_case};
use crate::trace::read_json::read_from_dict_json;
use crate::trace::read_json::tla_constant_mapping;
use crate::trace::trace_reader::TraceReader;

#[test]
Expand All @@ -24,7 +24,7 @@ mod test {

fn db_to_trace(input: String, output: String, setup_initialize: bool, expected_size: usize) {
let path_json = _test_data_path("map_const.json".to_string());
let r_dict = read_from_dict_json(Some(path_json));
let r_dict = tla_constant_mapping(Some(path_json));
let dict = match r_dict {
Ok(dict) => { dict }
Err(e) => { panic!("read from dict json file error: {}", e.to_string()); }
Expand Down
2 changes: 1 addition & 1 deletion src/trace_gen/trace_gen_portal.rs
Original file line number Diff line number Diff line change
Expand Up @@ -46,7 +46,7 @@ pub struct GenArgs {


pub fn portal(args: GenArgs) {
let r_dict = read_json::read_from_dict_json(args.map_const_path);
let r_dict = read_json::tla_constant_mapping(args.map_const_path);
let dict = match r_dict {
Ok(dict) => { dict }
Err(e) => { panic!("read from dict json file error: {}", e.to_string()); }
Expand Down

0 comments on commit f8c2de5

Please sign in to comment.