From ff12d4fede6197d3f24dba52650f5492bb7cc04c Mon Sep 17 00:00:00 2001 From: Lukas Gerlach <12497479+monsterkrampe@users.noreply.github.com> Date: Mon, 30 Jun 2025 08:51:23 +0200 Subject: [PATCH] Add naive af support to webserver (#195) * Update flake * Remove cargo-kcov * Make AdfParser publically accessible * Fix mongodb version to 6 * Add naive AF support in Web * Add missing doc strings * Remove unused import * Remove TODO comment * Update DevSkim Action * Upgrade flake * Apply clippy suggestions --------- Co-authored-by: monsterkrampe --- .github/workflows/devskim.yml | 6 +- bin/src/main.rs | 8 +- flake.lock | 14 +-- flake.nix | 4 +- frontend/src/components/adf-new-form.tsx | 21 +++- frontend/src/help-texts/add-info.md | 14 +++ lib/src/datatypes/bdd.rs | 4 +- lib/src/obdd.rs | 2 +- lib/src/parser.rs | 70 ++++++------- server/docker-compose.yml | 2 +- server/src/adf.rs | 121 +++++++++++++++++++++-- 11 files changed, 202 insertions(+), 64 deletions(-) diff --git a/.github/workflows/devskim.yml b/.github/workflows/devskim.yml index 2b9b877..cb96cce 100644 --- a/.github/workflows/devskim.yml +++ b/.github/workflows/devskim.yml @@ -16,19 +16,19 @@ on: jobs: lint: name: DevSkim - runs-on: ubuntu-20.04 + runs-on: ubuntu-latest permissions: actions: read contents: read security-events: write steps: - name: Checkout code - uses: actions/checkout@v3 + uses: actions/checkout@v4 - name: Run DevSkim scanner uses: microsoft/DevSkim-Action@v1 - name: Upload DevSkim scan results to GitHub Security tab - uses: github/codeql-action/upload-sarif@v2 + uses: github/codeql-action/upload-sarif@v3 with: sarif_file: devskim-results.sarif diff --git a/bin/src/main.rs b/bin/src/main.rs index 17a707e..77d8cf6 100644 --- a/bin/src/main.rs +++ b/bin/src/main.rs @@ -204,14 +204,14 @@ impl App { Some("nai") => { let naive_adf = adf.hybrid_step_opt(false); for ac_counts in naive_adf.formulacounts(false) { - print!("{:?} ", ac_counts); + print!("{ac_counts:?} "); } println!(); } Some("mem") => { let naive_adf = adf.hybrid_step_opt(false); for ac_counts in naive_adf.formulacounts(true) { - print!("{:?}", ac_counts); + print!("{ac_counts:?}"); } println!(); } @@ -383,13 +383,13 @@ impl App { match self.counter.as_deref() { Some("nai") => { for ac_counts in adf.formulacounts(false) { - print!("{:?} ", ac_counts); + print!("{ac_counts:?} "); } println!(); } Some("mem") => { for ac_counts in adf.formulacounts(true) { - print!("{:?}", ac_counts); + print!("{ac_counts:?}"); } println!(); } diff --git a/flake.lock b/flake.lock index 9a3baf9..cee7eea 100644 --- a/flake.lock +++ b/flake.lock @@ -38,16 +38,16 @@ }, "nixpkgs": { "locked": { - "lastModified": 1741724370, - "narHash": "sha256-WsD+8uodhl58jzKKcPH4jH9dLTLFWZpVmGq4W1XDVF4=", + "lastModified": 1750969886, + "narHash": "sha256-zW/OFnotiz/ndPFdebpo3X0CrbVNf22n4DjN2vxlb58=", "owner": "NixOS", "repo": "nixpkgs", - "rev": "95600680c021743fd87b3e2fe13be7c290e1cac4", + "rev": "a676066377a2fe7457369dd37c31fd2263b662f4", "type": "github" }, "original": { "owner": "NixOS", - "ref": "nixos-24.11", + "ref": "nixos-25.05", "repo": "nixpkgs", "type": "github" } @@ -66,11 +66,11 @@ ] }, "locked": { - "lastModified": 1741833135, - "narHash": "sha256-HUtFcF4NLwvu7CAowWgqCHXVkNj0EOc/W6Ism4biV6I=", + "lastModified": 1751251399, + "narHash": "sha256-y+viCuy/eKKpkX1K2gDvXIJI/yzvy6zA3HObapz9XZ0=", "owner": "oxalica", "repo": "rust-overlay", - "rev": "f3cd1e0feb994188fe3ad9a5c3ab021ed433b8c8", + "rev": "b22d5ee8c60ed1291521f2dde48784edd6bf695b", "type": "github" }, "original": { diff --git a/flake.nix b/flake.nix index 14ac338..de01226 100644 --- a/flake.nix +++ b/flake.nix @@ -2,7 +2,7 @@ rec { description = "adf-bdd, Abstract Dialectical Frameworks solved by Binary Decision Diagrams; developed in Dresden"; inputs = { - nixpkgs.url = "github:NixOS/nixpkgs/nixos-24.11"; + nixpkgs.url = "github:NixOS/nixpkgs/nixos-25.05"; rust-overlay = { url = "github:oxalica/rust-overlay"; inputs = { @@ -81,7 +81,7 @@ rec { pkgs.cargo-audit pkgs.cargo-license ] - ++ (notOn ["aarch64-darwin" "x86_64-darwin"] [pkgs.kcov pkgs.cargo-kcov pkgs.gnuplot pkgs.valgrind]) + ++ (notOn ["aarch64-darwin" "x86_64-darwin"] [pkgs.kcov pkgs.gnuplot pkgs.valgrind]) ++ (notOn ["aarch64-linux" "aarch64-darwin" "i686-linux"] [pkgs.cargo-tarpaulin]); }; }; diff --git a/frontend/src/components/adf-new-form.tsx b/frontend/src/components/adf-new-form.tsx index af2841c..cd518ba 100644 --- a/frontend/src/components/adf-new-form.tsx +++ b/frontend/src/components/adf-new-form.tsx @@ -40,6 +40,7 @@ function AdfNewForm({ fetchProblems }: { fetchProblems: () => void; }) { const [code, setCode] = useState(PLACEHOLDER); const [filename, setFilename] = useState(''); const [parsing, setParsing] = useState('Naive'); + const [isAf, setIsAf] = useState(false); const [name, setName] = useState(''); const fileRef = useRef(null); @@ -59,6 +60,7 @@ function AdfNewForm({ fetchProblems }: { fetchProblems: () => void; }) { } formData.append('parsing', parsing); + formData.append('is_af', isAf); formData.append('name', name); fetch(`${process.env.NODE_ENV === 'development' ? '//localhost:8080' : ''}/adf/add`, { @@ -119,10 +121,13 @@ function AdfNewForm({ fetchProblems }: { fetchProblems: () => void; }) { label="Put your code here:" helperText={( <> - For more info on the syntax, have a + For more info on the ADF syntax, have a look {' '} here + . For the AF syntax, we currently only allow the ICCMA competition format, see for example + {' '} + here . )} @@ -137,6 +142,20 @@ function AdfNewForm({ fetchProblems }: { fetchProblems: () => void; }) { + + ADF or AF? + setIsAf(((e.target as HTMLInputElement).value))} + > + } label="ADF" /> + } label="AF" /> + + AFs are converted to ADFs internally. + Parsing Strategy { +pub enum Formula { /// `c(f)` in the input format. Bot, /// `c(v)` in the input format. Top, /// Some atomic variable in the input format. - Atom(&'a str), + Atom(String), /// Negation of a subformula. - Not(Box>), + Not(Box), /// Conjunction of two subformulae. - And(Box>, Box>), + And(Box, Box), /// Disjunction of two subformulae. - Or(Box>, Box>), + Or(Box, Box), /// Implication of two subformulae. - Imp(Box>, Box>), + Imp(Box, Box), /// Exclusive-Or of two subformulae. - Xor(Box>, Box>), + Xor(Box, Box), /// If and only if connective between two formulae. - Iff(Box>, Box>), + Iff(Box, Box), } -impl Formula<'_> { +impl Formula { pub(crate) fn to_boolean_expr( &self, ) -> biodivine_lib_bdd::boolean_expression::BooleanExpression { @@ -90,29 +90,29 @@ impl Formula<'_> { } } -impl std::fmt::Debug for Formula<'_> { +impl std::fmt::Debug for Formula { fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { match self { Formula::Atom(a) => { - write!(f, "{}", a)?; + write!(f, "{a}")?; } Formula::Not(n) => { - write!(f, "not({:?})", n)?; + write!(f, "not({n:?})")?; } Formula::And(f1, f2) => { - write!(f, "and({:?},{:?})", f1, f2)?; + write!(f, "and({f1:?},{f2:?})")?; } Formula::Or(f1, f2) => { - write!(f, "or({:?},{:?})", f1, f2)?; + write!(f, "or({f1:?},{f2:?})")?; } Formula::Imp(f1, f2) => { - write!(f, "imp({:?},{:?})", f1, f2)?; + write!(f, "imp({f1:?},{f2:?})")?; } Formula::Xor(f1, f2) => { - write!(f, "xor({:?},{:?})", f1, f2)?; + write!(f, "xor({f1:?},{f2:?})")?; } Formula::Iff(f1, f2) => { - write!(f, "iff({:?},{:?})", f1, f2)?; + write!(f, "iff({f1:?},{f2:?})")?; } Formula::Bot => { write!(f, "Const(B)")?; @@ -132,14 +132,18 @@ impl std::fmt::Debug for Formula<'_> { /// /// Note that the parser can be utilised by an [ADF][`crate::adf::Adf`] to initialise it with minimal overhead. #[derive(Debug)] -pub struct AdfParser<'a> { - namelist: Arc>>, - dict: Arc>>, - formulae: RefCell>>, - formulaname: RefCell>, +pub struct AdfParser { + /// A name for each statement (identified by index in vector) + pub namelist: Arc>>, + /// Inverse mapping from name to index of statement in vector above + pub dict: Arc>>, + /// The formula (acceptance condition) for each statement identified by its index + pub formulae: RefCell>, + /// The formula for each statement identified by its index + pub formulaname: RefCell>, } -impl Default for AdfParser<'_> { +impl Default for AdfParser { fn default() -> Self { AdfParser { namelist: Arc::new(RwLock::new(Vec::new())), @@ -150,10 +154,7 @@ impl Default for AdfParser<'_> { } } -impl<'a, 'b> AdfParser<'b> -where - 'a: 'b, -{ +impl<'a> AdfParser { #[allow(dead_code)] fn parse_statements(&'a self) -> impl FnMut(&'a str) -> IResult<&'a str, ()> { move |input| { @@ -212,9 +213,9 @@ where } } -impl<'a> AdfParser<'a> { +impl AdfParser { /// Creates a new parser, utilising the already existing [VarContainer] - pub fn with_var_container(var_container: VarContainer) -> AdfParser<'a> { + pub fn with_var_container(var_container: VarContainer) -> AdfParser { AdfParser { namelist: var_container.names(), dict: var_container.mappings(), @@ -224,7 +225,7 @@ impl<'a> AdfParser<'a> { } } -impl AdfParser<'_> { +impl AdfParser { /// after an update to the namelist, all indizes are updated fn regenerate_indizes(&self) { self.namelist @@ -284,7 +285,7 @@ impl AdfParser<'_> { } fn atomic_term(input: &str) -> IResult<&str, Formula> { - AdfParser::atomic(input).map(|(input, result)| (input, Formula::Atom(result))) + AdfParser::atomic(input).map(|(input, result)| (input, Formula::Atom(result.to_string()))) } fn formula(input: &str) -> IResult<&str, Formula> { @@ -480,7 +481,7 @@ mod test { let (_remain, result) = AdfParser::formula(input).unwrap(); assert_eq!( - format!("{:?}", result), + format!("{result:?}"), "and(or(not(a),iff( iff left ,b)),xor(imp(c,d),e))" ); @@ -504,7 +505,10 @@ mod test { assert_eq!(parser.dict_value("b"), Some(2usize)); assert_eq!( format!("{:?}", parser.ac_at(1).unwrap()), - format!("{:?}", Formula::Not(Box::new(Formula::Atom("a")))) + format!( + "{:?}", + Formula::Not(Box::new(Formula::Atom("a".to_string()))) + ) ); assert_eq!(parser.formula_count(), 3); assert_eq!(parser.formula_order(), vec![0, 2, 1]); diff --git a/server/docker-compose.yml b/server/docker-compose.yml index f81f775..0801db0 100644 --- a/server/docker-compose.yml +++ b/server/docker-compose.yml @@ -3,7 +3,7 @@ version: '3.1' services: mongo: - image: mongo + image: mongo:6 restart: always ports: - 27017:27017 diff --git a/server/src/adf.rs b/server/src/adf.rs index c085f32..430d3d7 100644 --- a/server/src/adf.rs +++ b/server/src/adf.rs @@ -1,3 +1,4 @@ +use std::cell::RefCell; use std::collections::{HashMap, HashSet}; use std::sync::{Arc, RwLock}; #[cfg(feature = "mock_long_computations")] @@ -21,7 +22,7 @@ use serde::{Deserialize, Serialize}; use adf_bdd::adf::Adf; use adf_bdd::adfbiodivine::Adf as BdAdf; use adf_bdd::obdd::Bdd; -use adf_bdd::parser::AdfParser; +use adf_bdd::parser::{AdfParser, Formula}; use crate::config::{AppState, RunningInfo, Task, ADF_COLL, COMPUTE_TIME, DB_NAME, USER_COLL}; use crate::user::{username_exists, User}; @@ -205,6 +206,8 @@ pub(crate) struct AdfProblem { pub(crate) username: String, pub(crate) code: String, pub(crate) parsing_used: Parsing, + #[serde(default)] + pub(crate) is_af: bool, pub(crate) adf: SimplifiedAdfOpt, pub(crate) acs_per_strategy: AcsPerStrategy, } @@ -215,6 +218,7 @@ struct AddAdfProblemBodyMultipart { code: Option>, // Either Code or File is set file: Option, // Either Code or File is set parsing: Text, + is_af: Text, // if its not an AF then it is an ADF } #[derive(Clone)] @@ -222,6 +226,7 @@ struct AddAdfProblemBodyPlain { name: String, code: String, parsing: Parsing, + is_af: bool, // if its not an AF then it is an ADF } impl TryFrom for AddAdfProblemBodyPlain { @@ -237,6 +242,7 @@ impl TryFrom for AddAdfProblemBodyPlain { .and_then(|code| (!code.is_empty()).then_some(code)) .ok_or("Either a file or the code has to be provided.")?, parsing: source.parsing.into_inner(), + is_af: source.is_af.into_inner(), }) } } @@ -259,6 +265,7 @@ struct AdfProblemInfo { name: String, code: String, parsing_used: Parsing, + is_af: bool, acs_per_strategy: AcsPerStrategy, running_tasks: Vec, } @@ -269,6 +276,7 @@ impl AdfProblemInfo { name: adf.name.clone(), code: adf.code, parsing_used: adf.parsing_used, + is_af: adf.is_af, acs_per_strategy: adf.acs_per_strategy, running_tasks: tasks .iter() @@ -280,6 +288,87 @@ impl AdfProblemInfo { } } +struct AF(Vec>); + +impl From for AdfParser { + fn from(source: AF) -> Self { + let names: Vec = (0..source.0.len()) + .map(|val| (val + 1).to_string()) + .collect(); + let dict: HashMap = names + .iter() + .enumerate() + .map(|(i, val)| (val.clone(), i)) + .collect(); + let formulae: Vec = source + .0 + .into_iter() + .map(|attackers| { + attackers.into_iter().fold(Formula::Top, |acc, attacker| { + Formula::And( + Box::new(acc), + Box::new(Formula::Not(Box::new(Formula::Atom( + (attacker + 1).to_string(), + )))), + ) + }) + }) + .collect(); + let formulanames = names.clone(); + + Self { + namelist: Arc::new(RwLock::new(names)), + dict: Arc::new(RwLock::new(dict)), + formulae: RefCell::new(formulae), + formulaname: RefCell::new(formulanames), + } + } +} + +fn parse_af(code: String) -> Result { + let mut lines = code.lines(); + + let Some(first_line) = lines.next() else { + return Err("There must be at least one line in the AF input."); + }; + + let first_line: Vec<_> = first_line.split(" ").collect(); + if first_line[0] != "p" || first_line[1] != "af" { + return Err("Expected first line to be of the form: p af "); + } + + let Ok(num_arguments) = first_line[2].parse::() else { + return Err("Could not convert number of arguments to u32; expected first line to be of the form: p af "); + }; + + let attacks_opt: Option> = lines + .filter(|line| !line.starts_with('#') && !line.is_empty()) + .map(|line| { + let mut line = line.split(" "); + let a = line.next()?; + let b = line.next()?; + if line.next().is_some() { + None + } else { + Some((a.parse::().ok()?, b.parse::().ok()?)) + } + }) + .collect(); + let Some(attacks) = attacks_opt else { + return Err("Line must be of the form: n m"); + }; + + // index in outer vector represents attacked element + let mut is_attacked_by: Vec> = vec![vec![]; num_arguments]; + for (a, b) in attacks { + is_attacked_by[b - 1].push(a - 1); // we normalize names to be zero-indexed + } + + let hacked_adf_parser = AdfParser::from(AF(is_attacked_by)); + + Ok(hacked_adf_parser) +} + #[post("/add")] async fn add_adf_problem( req: HttpRequest, @@ -381,6 +470,7 @@ async fn add_adf_problem( username: username.clone(), code: adf_problem_input.code.clone(), parsing_used: adf_problem_input.parsing, + is_af: adf_problem_input.is_af, adf: SimplifiedAdfOpt::None, acs_per_strategy: AcsPerStrategy::default(), }; @@ -413,9 +503,20 @@ async fn add_adf_problem( #[cfg(feature = "mock_long_computations")] std::thread::sleep(Duration::from_secs(20)); - let parser = AdfParser::default(); - let parse_result = parser.parse()(&adf_problem_input.code) - .map_err(|_| "ADF could not be parsed, double check your input!"); + let (parser, parse_result) = { + if adf_problem_input.is_af { + parse_af(adf_problem_input.code) + .map(|p| (p, Ok(()))) + .unwrap_or_else(|e| (AdfParser::default(), Err(e))) + } else { + let parser = AdfParser::default(); + let parse_result = parser.parse()(&adf_problem_input.code) + .map(|_| ()) + .map_err(|_| "ADF could not be parsed, double check your input!"); + + (parser, parse_result) + } + }; let result = parse_result.map(|_| { let lib_adf = match adf_problem_input.parsing { @@ -500,7 +601,7 @@ async fn solve_adf_problem( .collection(ADF_COLL); let username = match identity.map(|id| id.id()) { - None => { + Option::None => { return HttpResponse::Unauthorized().body("You need to login to add an ADF problem.") } Some(Err(err)) => return HttpResponse::InternalServerError().body(err.to_string()), @@ -512,7 +613,7 @@ async fn solve_adf_problem( .await { Err(err) => return HttpResponse::InternalServerError().body(err.to_string()), - Ok(None) => { + Ok(Option::None) => { return HttpResponse::NotFound() .body(format!("ADF problem with name {problem_name} not found.")) } @@ -644,7 +745,7 @@ async fn get_adf_problem( .collection(ADF_COLL); let username = match identity.map(|id| id.id()) { - None => { + Option::None => { return HttpResponse::Unauthorized().body("You need to login to get an ADF problem.") } Some(Err(err)) => return HttpResponse::InternalServerError().body(err.to_string()), @@ -656,7 +757,7 @@ async fn get_adf_problem( .await { Err(err) => return HttpResponse::InternalServerError().body(err.to_string()), - Ok(None) => { + Ok(Option::None) => { return HttpResponse::NotFound() .body(format!("ADF problem with name {problem_name} not found.")) } @@ -682,7 +783,7 @@ async fn delete_adf_problem( .collection(ADF_COLL); let username = match identity.map(|id| id.id()) { - None => { + Option::None => { return HttpResponse::Unauthorized().body("You need to login to get an ADF problem.") } Some(Err(err)) => return HttpResponse::InternalServerError().body(err.to_string()), @@ -717,7 +818,7 @@ async fn get_adf_problems_for_user( .collection(ADF_COLL); let username = match identity.map(|id| id.id()) { - None => { + Option::None => { return HttpResponse::Unauthorized().body("You need to login to get an ADF problem.") } Some(Err(err)) => return HttpResponse::InternalServerError().body(err.to_string()),