Skip to content

Commit

Permalink
Remove UserTokenError (#148)
Browse files Browse the repository at this point in the history
This was broken because it required Reveaal to store all the user tokens
that is has given out. This violates the principle of idempotency. The
server cannot know when a user id is no longer in use, because we have
no "log out" endpoint and even if we had one the client could crash and
thus not send out a "log out" message.

Instead we assume that all clients are well behaved and use GetUserToken
to get a token that is not in use.

Co-authored-by: CasperStaahl <cstahl20@student.aau.dk>
  • Loading branch information
mads256h and CasperStaahl authored Nov 25, 2022
1 parent 07f633c commit bf43914
Show file tree
Hide file tree
Showing 4 changed files with 21 additions and 37 deletions.
2 changes: 1 addition & 1 deletion Ecdar-ProtoBuf
Submodule Ecdar-ProtoBuf updated 1 files
+46 −58 query.proto
18 changes: 6 additions & 12 deletions src/ProtobufServer/ecdar_requests/send_query.rs
Original file line number Diff line number Diff line change
Expand Up @@ -9,15 +9,11 @@ use crate::DataReader::json_writer::component_to_json;
use crate::DataReader::parse_queries;
use crate::ModelObjects::queries::Query;
use crate::ProtobufServer::services::component::Rep;
use crate::ProtobufServer::services::query_response::query_ok::{
use crate::ProtobufServer::services::query_response::{
ComponentResult, ConsistencyResult as ProtobufConsistencyResult,
DeterminismResult as ProtobufDeterminismResult, RefinementResult,
DeterminismResult as ProtobufDeterminismResult, ReachabilityResult, RefinementResult,
Result as ProtobufResult,
};
use crate::ProtobufServer::services::query_response::query_ok::{
ReachabilityResult, Result as ProtobufResult,
};
use crate::ProtobufServer::services::query_response::QueryOk;
use crate::ProtobufServer::services::query_response::Response as QueryOkOrErrorResponse;
use crate::ProtobufServer::services::{
self, Component as ProtobufComponent, ComponentClock as ProtobufComponentClock,
Conjunction as ProtobufConjunction, Constraint as ProtobufConstraint,
Expand Down Expand Up @@ -83,11 +79,9 @@ impl ConcreteEcdarBackend {
let result = executable_query.execute();

let reply = QueryResponse {
response: Some(QueryOkOrErrorResponse::QueryOk(QueryOk {
query_id: query_request.query_id,
info: vec![], // TODO: Should be logs
result: convert_ecdar_result(&result),
})),
query_id: query_request.query_id,
info: vec![], // TODO: Should be logs
result: convert_ecdar_result(&result),
};

Ok(reply)
Expand Down
2 changes: 1 addition & 1 deletion src/logging.rs
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
use crate::ProtobufServer::services::query_response::query_ok::Information;
use crate::ProtobufServer::services::query_response::Information;
use chrono::Local;
use colored::{ColoredString, Colorize};
use log::SetLoggerError;
Expand Down
36 changes: 13 additions & 23 deletions src/tests/grpc/send_query.rs
Original file line number Diff line number Diff line change
Expand Up @@ -2,8 +2,7 @@
mod refinements {
use crate::ProtobufServer::services::component::Rep;
use crate::ProtobufServer::services::ecdar_backend_server::EcdarBackend;
use crate::ProtobufServer::services::query_response::query_ok;
use crate::ProtobufServer::services::query_response::Response;
use crate::ProtobufServer::services::query_response;
use crate::ProtobufServer::services::Component;
use crate::ProtobufServer::services::ComponentsInfo;
use crate::ProtobufServer::services::QueryRequest;
Expand All @@ -22,13 +21,10 @@ mod refinements {
assert!(query_response.is_ok());

let query_result = query_response.unwrap().into_inner();

if let Response::QueryOk(query_ok) = query_result.response.unwrap() {
let result = query_ok.result.unwrap();
match result {
query_ok::Result::Refinement(refine) => assert!(refine.success),
_ => panic!(),
}
let result = query_result.result.unwrap();
match result {
query_response::Result::Refinement(refine) => assert!(refine.success),
_ => panic!(),
}
}

Expand All @@ -41,13 +37,10 @@ mod refinements {
assert!(query_response.is_ok());

let query_result = query_response.unwrap().into_inner();

if let Response::QueryOk(query_ok) = query_result.response.unwrap() {
let result = query_ok.result.unwrap();
match result {
query_ok::Result::Consistency(consistent) => assert!(consistent.success),
_ => panic!(),
}
let result = query_result.result.unwrap();
match result {
query_response::Result::Consistency(consistent) => assert!(consistent.success),
_ => panic!(),
}
}

Expand All @@ -60,13 +53,10 @@ mod refinements {
assert!(query_response.is_ok());

let query_result = query_response.unwrap().into_inner();

if let Response::QueryOk(query_ok) = query_result.response.unwrap() {
let result = query_ok.result.unwrap();
match result {
query_ok::Result::Determinism(determinism) => assert!(determinism.success),
_ => panic!(),
}
let result = query_result.result.unwrap();
match result {
query_response::Result::Determinism(determinism) => assert!(determinism.success),
_ => panic!(),
}
}

Expand Down

0 comments on commit bf43914

Please sign in to comment.