mirror of
https://github.com/ellmau/adf-obdd.git
synced 2025-12-20 09:39:38 +01:00
Compare commits
2 Commits
a0ad716b28
...
46ad9eb3fa
| Author | SHA1 | Date | |
|---|---|---|---|
|
|
46ad9eb3fa | ||
|
|
7e18b6194f |
@ -28,4 +28,4 @@ futures-util = "0.3.28"
|
||||
|
||||
[features]
|
||||
cors_for_local_development = []
|
||||
|
||||
mock_long_computations = []
|
||||
|
||||
@ -1,18 +1,21 @@
|
||||
use std::collections::{HashMap, HashSet};
|
||||
use std::sync::{Arc, RwLock};
|
||||
#[cfg(feature = "mock_long_computations")]
|
||||
use std::time::Duration;
|
||||
|
||||
use actix_identity::Identity;
|
||||
use actix_web::rt::spawn;
|
||||
use actix_web::rt::task::spawn_blocking;
|
||||
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::{BddNode, Term, Var};
|
||||
use futures_util::{FutureExt, TryStreamExt};
|
||||
use mongodb::bson::doc;
|
||||
use mongodb::bson::{to_bson, Bson};
|
||||
use mongodb::results::DeleteResult;
|
||||
use names::{Generator, Name};
|
||||
use serde::{Deserialize, Serialize};
|
||||
use futures_util::FutureExt;
|
||||
|
||||
use adf_bdd::adf::{Adf, DoubleLabeledGraph};
|
||||
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)]
|
||||
pub(crate) struct AcsPerStrategy {
|
||||
@ -65,7 +88,7 @@ pub(crate) struct AcsPerStrategy {
|
||||
pub(crate) stable_nogood: AcsAndGraphsOpt,
|
||||
}
|
||||
|
||||
#[derive(Deserialize, Serialize)]
|
||||
#[derive(Clone, Deserialize, Serialize)]
|
||||
pub(crate) struct VarContainerDb {
|
||||
names: Vec<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 {
|
||||
var: String,
|
||||
lo: String,
|
||||
@ -130,7 +153,7 @@ impl From<BddNodeDb> for BddNode {
|
||||
|
||||
type SimplifiedBdd = Vec<BddNodeDb>;
|
||||
|
||||
#[derive(Deserialize, Serialize)]
|
||||
#[derive(Clone, Deserialize, Serialize)]
|
||||
pub(crate) struct SimplifiedAdf {
|
||||
pub(crate) ordering: VarContainerDb,
|
||||
pub(crate) bdd: SimplifiedBdd,
|
||||
@ -147,13 +170,15 @@ impl SimplifiedAdf {
|
||||
}
|
||||
}
|
||||
|
||||
type SimplifiedAdfOpt = OptionWithError<SimplifiedAdf>;
|
||||
|
||||
#[derive(Deserialize, Serialize)]
|
||||
pub(crate) struct AdfProblem {
|
||||
pub(crate) name: String,
|
||||
pub(crate) username: String,
|
||||
pub(crate) code: String,
|
||||
pub(crate) parsing_used: Parsing,
|
||||
pub(crate) adf: SimplifiedAdf,
|
||||
pub(crate) adf: SimplifiedAdfOpt,
|
||||
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 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_res = timeout(
|
||||
let adf_fut = timeout(
|
||||
COMPUTE_TIME,
|
||||
spawn_blocking(move || {
|
||||
let running_info = RunningInfo {
|
||||
@ -319,11 +358,14 @@ async fn add_adf_problem(
|
||||
.unwrap()
|
||||
.insert(running_info.clone());
|
||||
|
||||
#[cfg(feature = "mock_long_computations")]
|
||||
std::thread::sleep(Duration::from_secs(20));
|
||||
|
||||
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!")?;
|
||||
|
||||
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::Hybrid => {
|
||||
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
|
||||
.currently_running
|
||||
.lock()
|
||||
.unwrap()
|
||||
.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))
|
||||
}),
|
||||
)
|
||||
.await;
|
||||
);
|
||||
|
||||
match adf_res {
|
||||
Err(err) => HttpResponse::InternalServerError().body(err.to_string()),
|
||||
Ok(Err(err)) => HttpResponse::InternalServerError().body(err.to_string()),
|
||||
Ok(Ok(Err(err))) => HttpResponse::InternalServerError().body(err.to_string()),
|
||||
Ok(Ok(Ok((adf, ac_and_graph)))) => {
|
||||
let acs = AcsPerStrategy {
|
||||
parse_only: Some(vec![ac_and_graph]),
|
||||
..Default::default()
|
||||
};
|
||||
spawn(adf_fut.then(move |adf_res| async move {
|
||||
let (adf, ac_and_graph): (SimplifiedAdfOpt, AcsAndGraphsOpt) = match adf_res {
|
||||
Err(err) => (
|
||||
SimplifiedAdfOpt::Error(err.to_string()),
|
||||
AcsAndGraphsOpt::Error(err.to_string()),
|
||||
),
|
||||
Ok(Err(err)) => (
|
||||
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 {
|
||||
name: problem_name,
|
||||
username,
|
||||
code: adf_problem_input.code,
|
||||
parsing_used: adf_problem_input.parse_strategy,
|
||||
adf,
|
||||
acs_per_strategy: acs,
|
||||
};
|
||||
let result = adf_coll
|
||||
.update_one(
|
||||
doc! { "name": problem_name, "username": username },
|
||||
doc! { "$set": { "adf": &adf, "acs_per_strategy.parse_only": &ac_and_graph } },
|
||||
None,
|
||||
)
|
||||
.await;
|
||||
|
||||
let result = adf_coll.insert_one(&adf_problem, None).await;
|
||||
|
||||
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()),
|
||||
}
|
||||
if let Err(err) = result {
|
||||
log::error!("{err}");
|
||||
}
|
||||
}
|
||||
}));
|
||||
|
||||
HttpResponse::Ok().body("Parsing started...")
|
||||
}
|
||||
|
||||
#[derive(Deserialize)]
|
||||
@ -415,6 +463,18 @@ async fn solve_adf_problem(
|
||||
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 {
|
||||
Strategy::Complete => adf_problem.acs_per_strategy.complete.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 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(
|
||||
COMPUTE_TIME,
|
||||
spawn_blocking(move || {
|
||||
let running_info = RunningInfo {
|
||||
username: username_clone,
|
||||
adf_name: problem_name_clone,
|
||||
task: Task::Solve(strategy_clone.clone()),
|
||||
task: Task::Solve(adf_problem_input.strategy),
|
||||
};
|
||||
|
||||
app_state
|
||||
@ -450,18 +508,20 @@ async fn solve_adf_problem(
|
||||
.unwrap()
|
||||
.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(
|
||||
adf_problem.adf.ordering.into(),
|
||||
adf_problem.adf.bdd.into_iter().map(Into::into).collect(),
|
||||
adf_problem
|
||||
.adf
|
||||
simp_adf.ordering.into(),
|
||||
simp_adf.bdd.into_iter().map(Into::into).collect(),
|
||||
simp_adf
|
||||
.ac
|
||||
.into_iter()
|
||||
.map(|t| Term(t.parse().unwrap()))
|
||||
.collect(),
|
||||
);
|
||||
|
||||
let acs: Vec<Ac> = match strategy_clone {
|
||||
let acs: Vec<Ac> = match adf_problem_input.strategy {
|
||||
Strategy::Complete => adf.complete().collect(),
|
||||
Strategy::Ground => vec![adf.grounded()],
|
||||
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 {
|
||||
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) => HttpResponse::InternalServerError().body(err.to_string()),
|
||||
Ok(Err(err)) => HttpResponse::InternalServerError().body(err.to_string()),
|
||||
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 acs_and_graphs_enum: AcsAndGraphsOpt = match acs_and_graphs_res {
|
||||
Err(err) => AcsAndGraphsOpt::Error(err.to_string()),
|
||||
Ok(Err(err)) => AcsAndGraphsOpt::Error(err.to_string()),
|
||||
Ok(Ok(acs_and_graphs)) => AcsAndGraphsOpt::Some(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": &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}")]
|
||||
@ -556,3 +614,80 @@ async fn get_adf_problem(
|
||||
&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)
|
||||
}
|
||||
|
||||
@ -17,7 +17,10 @@ mod adf;
|
||||
mod config;
|
||||
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 user::{
|
||||
create_username_index, delete_account, login, logout, register, update_user, user_info,
|
||||
@ -82,7 +85,10 @@ async fn main() -> std::io::Result<()> {
|
||||
.service(
|
||||
web::scope("/adf")
|
||||
.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
|
||||
.service(fs::Files::new("/", ASSET_DIRECTORY).index_file("index.html"))
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user