1
0
mirror of https://github.com/ellmau/adf-obdd.git synced 2025-12-20 09:39:38 +01:00

Compare commits

..

2 Commits

Author SHA1 Message Date
monsterkrampe
46ad9eb3fa
Add Delete and Index endpoints for ADFs 2023-04-03 11:00:42 +02:00
monsterkrampe
7e18b6194f
Return early for parse and solve; Add Adf GET 2023-04-03 10:25:51 +02:00
3 changed files with 215 additions and 74 deletions

View File

@ -28,4 +28,4 @@ futures-util = "0.3.28"
[features] [features]
cors_for_local_development = [] cors_for_local_development = []
mock_long_computations = []

View File

@ -1,18 +1,21 @@
use std::collections::{HashMap, HashSet}; use std::collections::{HashMap, HashSet};
use std::sync::{Arc, RwLock}; use std::sync::{Arc, RwLock};
#[cfg(feature = "mock_long_computations")]
use std::time::Duration;
use actix_identity::Identity; use actix_identity::Identity;
use actix_web::rt::spawn; use actix_web::rt::spawn;
use actix_web::rt::task::spawn_blocking; use actix_web::rt::task::spawn_blocking;
use actix_web::rt::time::timeout; use actix_web::rt::time::timeout;
use actix_web::{get, post, put, web, HttpMessage, HttpRequest, HttpResponse, Responder}; use actix_web::{delete, get, post, put, web, HttpMessage, HttpRequest, HttpResponse, Responder};
use adf_bdd::datatypes::adf::VarContainer; use adf_bdd::datatypes::adf::VarContainer;
use adf_bdd::datatypes::{BddNode, Term, Var}; use adf_bdd::datatypes::{BddNode, Term, Var};
use futures_util::{FutureExt, TryStreamExt};
use mongodb::bson::doc; use mongodb::bson::doc;
use mongodb::bson::{to_bson, Bson}; use mongodb::bson::{to_bson, Bson};
use mongodb::results::DeleteResult;
use names::{Generator, Name}; use names::{Generator, Name};
use serde::{Deserialize, Serialize}; use serde::{Deserialize, Serialize};
use futures_util::FutureExt;
use adf_bdd::adf::{Adf, DoubleLabeledGraph}; use adf_bdd::adf::{Adf, DoubleLabeledGraph};
use adf_bdd::adfbiodivine::Adf as BdAdf; use adf_bdd::adfbiodivine::Adf as BdAdf;
@ -52,7 +55,27 @@ impl From<AcAndGraph> for Bson {
} }
} }
type AcsAndGraphsOpt = Option<Vec<AcAndGraph>>; #[derive(Clone, Default, Deserialize, Serialize)]
pub(crate) enum OptionWithError<T> {
Some(T),
Error(String),
#[default]
None,
}
impl<T> OptionWithError<T> {
fn is_some(&self) -> bool {
matches!(self, Self::Some(_))
}
}
impl<T: Serialize> From<OptionWithError<T>> for Bson {
fn from(source: OptionWithError<T>) -> Self {
to_bson(&source).expect("Serialization should work")
}
}
type AcsAndGraphsOpt = OptionWithError<Vec<AcAndGraph>>;
#[derive(Default, Deserialize, Serialize)] #[derive(Default, Deserialize, Serialize)]
pub(crate) struct AcsPerStrategy { pub(crate) struct AcsPerStrategy {
@ -65,7 +88,7 @@ pub(crate) struct AcsPerStrategy {
pub(crate) stable_nogood: AcsAndGraphsOpt, pub(crate) stable_nogood: AcsAndGraphsOpt,
} }
#[derive(Deserialize, Serialize)] #[derive(Clone, Deserialize, Serialize)]
pub(crate) struct VarContainerDb { pub(crate) struct VarContainerDb {
names: Vec<String>, names: Vec<String>,
mapping: HashMap<String, String>, mapping: HashMap<String, String>,
@ -101,7 +124,7 @@ impl From<VarContainerDb> for VarContainer {
} }
} }
#[derive(Deserialize, Serialize)] #[derive(Clone, Deserialize, Serialize)]
pub(crate) struct BddNodeDb { pub(crate) struct BddNodeDb {
var: String, var: String,
lo: String, lo: String,
@ -130,7 +153,7 @@ impl From<BddNodeDb> for BddNode {
type SimplifiedBdd = Vec<BddNodeDb>; type SimplifiedBdd = Vec<BddNodeDb>;
#[derive(Deserialize, Serialize)] #[derive(Clone, Deserialize, Serialize)]
pub(crate) struct SimplifiedAdf { pub(crate) struct SimplifiedAdf {
pub(crate) ordering: VarContainerDb, pub(crate) ordering: VarContainerDb,
pub(crate) bdd: SimplifiedBdd, pub(crate) bdd: SimplifiedBdd,
@ -147,13 +170,15 @@ impl SimplifiedAdf {
} }
} }
type SimplifiedAdfOpt = OptionWithError<SimplifiedAdf>;
#[derive(Deserialize, Serialize)] #[derive(Deserialize, Serialize)]
pub(crate) struct AdfProblem { pub(crate) struct AdfProblem {
pub(crate) name: String, pub(crate) name: String,
pub(crate) username: String, pub(crate) username: String,
pub(crate) code: String, pub(crate) code: String,
pub(crate) parsing_used: Parsing, pub(crate) parsing_used: Parsing,
pub(crate) adf: SimplifiedAdf, pub(crate) adf: SimplifiedAdfOpt,
pub(crate) acs_per_strategy: AcsPerStrategy, pub(crate) acs_per_strategy: AcsPerStrategy,
} }
@ -299,12 +324,26 @@ async fn add_adf_problem(
} }
}; };
let adf_problem_input_clone = adf_problem_input.clone(); let adf_problem: AdfProblem = AdfProblem {
name: problem_name.clone(),
username: username.clone(),
code: adf_problem_input.code.clone(),
parsing_used: adf_problem_input.parse_strategy,
adf: SimplifiedAdfOpt::None,
acs_per_strategy: AcsPerStrategy::default(),
};
let result = adf_coll.insert_one(&adf_problem, None).await;
if let Err(err) = result {
return HttpResponse::InternalServerError()
.body(format!("Could not create Database entry. Error: {err}"));
}
let username_clone = username.clone(); let username_clone = username.clone();
let problem_name_clone = problem_name.clone(); let problem_name_clone = problem_name.clone();
// TODO: change this: we want to return a response from the request whil the computation is running let adf_fut = timeout(
let adf_res = timeout(
COMPUTE_TIME, COMPUTE_TIME,
spawn_blocking(move || { spawn_blocking(move || {
let running_info = RunningInfo { let running_info = RunningInfo {
@ -319,11 +358,14 @@ async fn add_adf_problem(
.unwrap() .unwrap()
.insert(running_info.clone()); .insert(running_info.clone());
#[cfg(feature = "mock_long_computations")]
std::thread::sleep(Duration::from_secs(20));
let parser = AdfParser::default(); let parser = AdfParser::default();
parser.parse()(&adf_problem_input_clone.code) parser.parse()(&adf_problem_input.code)
.map_err(|_| "ADF could not be parsed, double check your input!")?; .map_err(|_| "ADF could not be parsed, double check your input!")?;
let lib_adf = match adf_problem_input_clone.parse_strategy { let lib_adf = match adf_problem_input.parse_strategy {
Parsing::Naive => Adf::from_parser(&parser), Parsing::Naive => Adf::from_parser(&parser),
Parsing::Hybrid => { Parsing::Hybrid => {
let bd_adf = BdAdf::from_parser(&parser); let bd_adf = BdAdf::from_parser(&parser);
@ -331,49 +373,55 @@ async fn add_adf_problem(
} }
}; };
let ac_and_graph = AcAndGraph {
ac: lib_adf.ac.iter().map(|t| t.0.to_string()).collect(),
graph: lib_adf.into_double_labeled_graph(None),
};
app_state app_state
.currently_running .currently_running
.lock() .lock()
.unwrap() .unwrap()
.remove(&running_info); .remove(&running_info);
let ac_and_graph = AcAndGraph {
ac: lib_adf.ac.iter().map(|t| t.0.to_string()).collect(),
graph: lib_adf.into_double_labeled_graph(None),
};
Ok::<_, &str>((SimplifiedAdf::from_lib_adf(lib_adf), ac_and_graph)) Ok::<_, &str>((SimplifiedAdf::from_lib_adf(lib_adf), ac_and_graph))
}), }),
) );
.await;
match adf_res { spawn(adf_fut.then(move |adf_res| async move {
Err(err) => HttpResponse::InternalServerError().body(err.to_string()), let (adf, ac_and_graph): (SimplifiedAdfOpt, AcsAndGraphsOpt) = match adf_res {
Ok(Err(err)) => HttpResponse::InternalServerError().body(err.to_string()), Err(err) => (
Ok(Ok(Err(err))) => HttpResponse::InternalServerError().body(err.to_string()), SimplifiedAdfOpt::Error(err.to_string()),
Ok(Ok(Ok((adf, ac_and_graph)))) => { AcsAndGraphsOpt::Error(err.to_string()),
let acs = AcsPerStrategy { ),
parse_only: Some(vec![ac_and_graph]), Ok(Err(err)) => (
..Default::default() SimplifiedAdfOpt::Error(err.to_string()),
}; AcsAndGraphsOpt::Error(err.to_string()),
),
Ok(Ok(Err(err))) => (
SimplifiedAdfOpt::Error(err.to_string()),
AcsAndGraphsOpt::Error(err.to_string()),
),
Ok(Ok(Ok((adf, ac_and_graph)))) => (
SimplifiedAdfOpt::Some(adf),
AcsAndGraphsOpt::Some(vec![ac_and_graph]),
),
};
let adf_problem: AdfProblem = AdfProblem { let result = adf_coll
name: problem_name, .update_one(
username, doc! { "name": problem_name, "username": username },
code: adf_problem_input.code, doc! { "$set": { "adf": &adf, "acs_per_strategy.parse_only": &ac_and_graph } },
parsing_used: adf_problem_input.parse_strategy, None,
adf, )
acs_per_strategy: acs, .await;
};
let result = adf_coll.insert_one(&adf_problem, None).await; if let Err(err) = result {
log::error!("{err}");
match result {
Ok(_) => HttpResponse::Ok().json(AdfProblemInfo::from_adf_prob_and_tasks(adf_problem, &HashSet::new())), // there should be no tasks running here
Err(err) => HttpResponse::InternalServerError().body(err.to_string()),
}
} }
} }));
HttpResponse::Ok().body("Parsing started...")
} }
#[derive(Deserialize)] #[derive(Deserialize)]
@ -415,6 +463,18 @@ async fn solve_adf_problem(
Ok(Some(prob)) => prob, Ok(Some(prob)) => prob,
}; };
let simp_adf: SimplifiedAdf = match adf_problem.adf {
SimplifiedAdfOpt::None => {
return HttpResponse::BadRequest().body("The ADF problem has not been parsed yet.")
}
SimplifiedAdfOpt::Error(err) => {
return HttpResponse::BadRequest().body(format!(
"The ADF problem could not be parsed. Update it and try again. Error: {err}"
))
}
SimplifiedAdfOpt::Some(adf) => adf,
};
let has_been_solved = match adf_problem_input.strategy { let has_been_solved = match adf_problem_input.strategy {
Strategy::Complete => adf_problem.acs_per_strategy.complete.is_some(), Strategy::Complete => adf_problem.acs_per_strategy.complete.is_some(),
Strategy::Ground => adf_problem.acs_per_strategy.ground.is_some(), Strategy::Ground => adf_problem.acs_per_strategy.ground.is_some(),
@ -432,16 +492,14 @@ async fn solve_adf_problem(
let username_clone = username.clone(); let username_clone = username.clone();
let problem_name_clone = problem_name.clone(); let problem_name_clone = problem_name.clone();
let strategy_clone = adf_problem_input.strategy.clone();
// TODO: change this: we want to return a response from the request whil the computation is running
let acs_and_graphs_fut = timeout( let acs_and_graphs_fut = timeout(
COMPUTE_TIME, COMPUTE_TIME,
spawn_blocking(move || { spawn_blocking(move || {
let running_info = RunningInfo { let running_info = RunningInfo {
username: username_clone, username: username_clone,
adf_name: problem_name_clone, adf_name: problem_name_clone,
task: Task::Solve(strategy_clone.clone()), task: Task::Solve(adf_problem_input.strategy),
}; };
app_state app_state
@ -450,18 +508,20 @@ async fn solve_adf_problem(
.unwrap() .unwrap()
.insert(running_info.clone()); .insert(running_info.clone());
#[cfg(feature = "mock_long_computations")]
std::thread::sleep(Duration::from_secs(20));
let mut adf: Adf = Adf::from_ord_nodes_and_ac( let mut adf: Adf = Adf::from_ord_nodes_and_ac(
adf_problem.adf.ordering.into(), simp_adf.ordering.into(),
adf_problem.adf.bdd.into_iter().map(Into::into).collect(), simp_adf.bdd.into_iter().map(Into::into).collect(),
adf_problem simp_adf
.adf
.ac .ac
.into_iter() .into_iter()
.map(|t| Term(t.parse().unwrap())) .map(|t| Term(t.parse().unwrap()))
.collect(), .collect(),
); );
let acs: Vec<Ac> = match strategy_clone { let acs: Vec<Ac> = match adf_problem_input.strategy {
Strategy::Complete => adf.complete().collect(), Strategy::Complete => adf.complete().collect(),
Strategy::Ground => vec![adf.grounded()], Strategy::Ground => vec![adf.grounded()],
Strategy::Stable => adf.stable().collect(), Strategy::Stable => adf.stable().collect(),
@ -494,29 +554,27 @@ async fn solve_adf_problem(
); );
spawn(acs_and_graphs_fut.then(move |acs_and_graphs_res| async move { spawn(acs_and_graphs_fut.then(move |acs_and_graphs_res| async move {
match acs_and_graphs_res { let acs_and_graphs_enum: AcsAndGraphsOpt = match acs_and_graphs_res {
// TODO: error states should somehow be set in the database since the status codes are irrelevant in this future Err(err) => AcsAndGraphsOpt::Error(err.to_string()),
Err(err) => HttpResponse::InternalServerError().body(err.to_string()), Ok(Err(err)) => AcsAndGraphsOpt::Error(err.to_string()),
Ok(Err(err)) => HttpResponse::InternalServerError().body(err.to_string()), Ok(Ok(acs_and_graphs)) => AcsAndGraphsOpt::Some(acs_and_graphs),
Ok(Ok(acs_and_graphs)) => {
let result = adf_coll.update_one(doc! { "name": problem_name, "username": username }, match adf_problem_input.strategy {
Strategy::Complete => doc! { "$set": { "acs_per_strategy.complete": Some(&acs_and_graphs) } },
Strategy::Ground => doc! { "$set": { "acs_per_strategy.ground": Some(&acs_and_graphs) } },
Strategy::Stable => doc! { "$set": { "acs_per_strategy.stable": Some(&acs_and_graphs) } },
Strategy::StableCountingA => doc! { "$set": { "acs_per_strategy.stable_counting_a": Some(&acs_and_graphs) } },
Strategy::StableCountingB => doc! { "$set": { "acs_per_strategy.stable_counting_b": Some(&acs_and_graphs) } },
Strategy::StableNogood => doc! { "$set": { "acs_per_strategy.stable_nogood": Some(&acs_and_graphs) } },
}, None).await;
match result {
Ok(_) => HttpResponse::Ok().json(acs_and_graphs),
Err(err) => HttpResponse::InternalServerError().body(err.to_string()),
}
}
}; };
let result = adf_coll.update_one(doc! { "name": problem_name, "username": username }, match adf_problem_input.strategy {
Strategy::Complete => doc! { "$set": { "acs_per_strategy.complete": &acs_and_graphs_enum } },
Strategy::Ground => doc! { "$set": { "acs_per_strategy.ground": &acs_and_graphs_enum } },
Strategy::Stable => doc! { "$set": { "acs_per_strategy.stable": &acs_and_graphs_enum } },
Strategy::StableCountingA => doc! { "$set": { "acs_per_strategy.stable_counting_a": &acs_and_graphs_enum } },
Strategy::StableCountingB => doc! { "$set": { "acs_per_strategy.stable_counting_b": &acs_and_graphs_enum } },
Strategy::StableNogood => doc! { "$set": { "acs_per_strategy.stable_nogood": &acs_and_graphs_enum } },
}, None).await;
if let Err(err) = result {
log::error!("{err}");
}
})); }));
HttpResponse::Ok().body("Parsing started...") HttpResponse::Ok().body("Solving started...")
} }
#[get("/{problem_name}")] #[get("/{problem_name}")]
@ -556,3 +614,80 @@ async fn get_adf_problem(
&app_state.currently_running.lock().unwrap(), &app_state.currently_running.lock().unwrap(),
)) ))
} }
#[delete("/{problem_name}")]
async fn delete_adf_problem(
app_state: web::Data<AppState>,
identity: Option<Identity>,
path: web::Path<String>,
) -> impl Responder {
let problem_name = path.into_inner();
let adf_coll: mongodb::Collection<AdfProblem> = app_state
.mongodb_client
.database(DB_NAME)
.collection(ADF_COLL);
let username = match identity.map(|id| id.id()) {
None => {
return HttpResponse::Unauthorized().body("You need to login to get an ADF problem.")
}
Some(Err(err)) => return HttpResponse::InternalServerError().body(err.to_string()),
Some(Ok(username)) => username,
};
match adf_coll
.delete_one(doc! { "name": &problem_name, "username": &username }, None)
.await
{
Ok(DeleteResult {
deleted_count: 0, ..
}) => HttpResponse::InternalServerError().body("Adf Problem could not be deleted."),
Ok(DeleteResult {
deleted_count: 1, ..
}) => HttpResponse::Ok().body("Adf Problem deleted."),
Ok(_) => {
unreachable!("delete_one removes at most one entry so all cases are covered already")
}
Err(err) => HttpResponse::InternalServerError().body(err.to_string()),
}
}
#[get("/")]
async fn get_adf_problems_for_user(
app_state: web::Data<AppState>,
identity: Option<Identity>,
) -> impl Responder {
let adf_coll: mongodb::Collection<AdfProblem> = app_state
.mongodb_client
.database(DB_NAME)
.collection(ADF_COLL);
let username = match identity.map(|id| id.id()) {
None => {
return HttpResponse::Unauthorized().body("You need to login to get an ADF problem.")
}
Some(Err(err)) => return HttpResponse::InternalServerError().body(err.to_string()),
Some(Ok(username)) => username,
};
let adf_problem_cursor = match adf_coll.find(doc! { "username": &username }, None).await {
Err(err) => return HttpResponse::InternalServerError().body(err.to_string()),
Ok(cursor) => cursor,
};
let adf_problems: Vec<AdfProblemInfo> = match adf_problem_cursor
.map_ok(|adf_problem| {
AdfProblemInfo::from_adf_prob_and_tasks(
adf_problem,
&app_state.currently_running.lock().unwrap(),
)
})
.try_collect()
.await
{
Err(err) => return HttpResponse::InternalServerError().body(err.to_string()),
Ok(probs) => probs,
};
HttpResponse::Ok().json(adf_problems)
}

View File

@ -17,7 +17,10 @@ mod adf;
mod config; mod config;
mod user; mod user;
use adf::{add_adf_problem, solve_adf_problem}; use adf::{
add_adf_problem, delete_adf_problem, get_adf_problem, get_adf_problems_for_user,
solve_adf_problem,
};
use config::{AppState, ASSET_DIRECTORY, COOKIE_DURATION}; use config::{AppState, ASSET_DIRECTORY, COOKIE_DURATION};
use user::{ use user::{
create_username_index, delete_account, login, logout, register, update_user, user_info, create_username_index, delete_account, login, logout, register, update_user, user_info,
@ -82,7 +85,10 @@ async fn main() -> std::io::Result<()> {
.service( .service(
web::scope("/adf") web::scope("/adf")
.service(add_adf_problem) .service(add_adf_problem)
.service(solve_adf_problem), .service(solve_adf_problem)
.service(get_adf_problem)
.service(delete_adf_problem)
.service(get_adf_problems_for_user),
) )
// this mus be last to not override anything // this mus be last to not override anything
.service(fs::Files::new("/", ASSET_DIRECTORY).index_file("index.html")) .service(fs::Files::new("/", ASSET_DIRECTORY).index_file("index.html"))