ellmau/adf-obdd
1
0
Fork 0
mirror of https://github.com/ellmau/adf-obdd.git synced 2025-12-18 09:19:38 +01:00
Code Issues Projects Releases Wiki Activity

Add naive af support to webserver (#195)

Browse Source 
* 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 <monsterkrampe@users.noreply.github.com>
This commit is contained in:
Lukas Gerlach 2025-06-30 08:51:23 +02:00 committed by GitHub
parent c9631346ab
commit ff12d4fede
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
11 changed files with 202 additions and 64 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
.github/workflows/devskim.yml vendored
View File

@ -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

8
bin/src/main.rs
View File

@ -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!();
}

14
flake.lock generated
View File

@ -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": {

4
flake.nix
View File

@ -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]);
};
};

21
frontend/src/components/adf-new-form.tsx
View File

@ -40,6 +40,7 @@ function AdfNewForm({ fetchProblems }: { fetchProblems: () => void; }) {
const [code, setCode] = useState(PLACEHOLDER);
const [filename, setFilename] = useState('');
const [parsing, setParsing] = useState<Parsing>('Naive');
const [isAf, setIsAf] = useState(false);
const [name, setName] = useState('');
const fileRef = useRef<HTMLInputElement>(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
{' '}
<Link href="https://github.com/ellmau/adf-obdd" target="_blank" rel="noopener noreferrer">here</Link>
. For the AF syntax, we currently only allow the ICCMA competition format, see for example
{' '}
<Link href="https://argumentationcompetition.org/2025/rules.html" target="_blank" rel="noopener noreferrer">here</Link>
.
</>
)}
@ -137,6 +142,20 @@ function AdfNewForm({ fetchProblems }: { fetchProblems: () => void; }) {
<Container sx={{ marginTop: 2 }}>
<Stack direction="row" justifyContent="center" spacing={2}>
<FormControl>
<FormLabel id="isAf-radio-group">ADF or AF?</FormLabel>
<RadioGroup
row
aria-labelledby="isAf-radio-group"
name="isAf"
value={isAf}
onChange={(e) => setIsAf(((e.target as HTMLInputElement).value))}
>
<FormControlLabel value={false} control={<Radio />} label="ADF" />
<FormControlLabel value={true} control={<Radio />} label="AF" />
</RadioGroup>
<span style={{ fontSize: "0.7em" }}>AFs are converted to ADFs internally.</span>
</FormControl>
<FormControl>
<FormLabel id="parsing-radio-group">Parsing Strategy</FormLabel>
<RadioGroup

14
frontend/src/help-texts/add-info.md
View File

@ -21,3 +21,17 @@ The `Parsing Strategy` determines the internal implementation used for these. `N
You will get a view on the BDD in the detail view after you added the problem.
You can optionally set a name for you ADF problem. Otherwise a random name will be chosen. At the moment the name cannot be changed later (but you could remove and re-add the problem).
We also support adding AFs in the ICCMA competition format. They are converted to ADFs internally in the obvious way.
For example you can try the following code and change the option below from ADF to AF.
```
p af 5
# this is a comment
1 2
2 4
4 5
5 4
5 5
```

4
lib/src/datatypes/bdd.rs
View File

@ -275,8 +275,8 @@ mod test {
let term: Term = Term::from(value);
let var = Var::from(value);
// display
assert_eq!(format!("{}", term), format!("Term({})", value));
assert_eq!(format!("{}", var), format!("Var({})", value));
assert_eq!(format!("{term}"), format!("Term({})", value));
assert_eq!(format!("{var}"), format!("Var({})", value));
//deref
assert_eq!(value, *term);
true

2
lib/src/obdd.rs
View File

@ -690,7 +690,7 @@ mod test {
let a1 = bdd.and(v1, v2);
let _a2 = bdd.or(a1, v3);
assert_eq!(format!("{}", bdd), " \n0 BddNode: Var(18446744073709551614), lo: Term(0), hi: Term(0)\n1 BddNode: Var(18446744073709551615), lo: Term(1), hi: Term(1)\n2 BddNode: Var(0), lo: Term(0), hi: Term(1)\n3 BddNode: Var(1), lo: Term(0), hi: Term(1)\n4 BddNode: Var(2), lo: Term(0), hi: Term(1)\n5 BddNode: Var(0), lo: Term(0), hi: Term(3)\n6 BddNode: Var(1), lo: Term(4), hi: Term(1)\n7 BddNode: Var(0), lo: Term(4), hi: Term(6)\n");
assert_eq!(format!("{bdd}"), " \n0 BddNode: Var(18446744073709551614), lo: Term(0), hi: Term(0)\n1 BddNode: Var(18446744073709551615), lo: Term(1), hi: Term(1)\n2 BddNode: Var(0), lo: Term(0), hi: Term(1)\n3 BddNode: Var(1), lo: Term(0), hi: Term(1)\n4 BddNode: Var(2), lo: Term(0), hi: Term(1)\n5 BddNode: Var(0), lo: Term(0), hi: Term(3)\n6 BddNode: Var(1), lo: Term(4), hi: Term(1)\n7 BddNode: Var(0), lo: Term(4), hi: Term(6)\n");
}
#[test]

70
lib/src/parser.rs
View File

@ -20,28 +20,28 @@ use crate::datatypes::adf::VarContainer;
/// A representation of a formula, still using the strings from the input.
#[derive(Clone, PartialEq, Eq)]
pub enum Formula<'a> {
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<Formula<'a>>),
Not(Box<Formula>),
/// Conjunction of two subformulae.
And(Box<Formula<'a>>, Box<Formula<'a>>),
And(Box<Formula>, Box<Formula>),
/// Disjunction of two subformulae.
Or(Box<Formula<'a>>, Box<Formula<'a>>),
Or(Box<Formula>, Box<Formula>),
/// Implication of two subformulae.
Imp(Box<Formula<'a>>, Box<Formula<'a>>),
Imp(Box<Formula>, Box<Formula>),
/// Exclusive-Or of two subformulae.
Xor(Box<Formula<'a>>, Box<Formula<'a>>),
Xor(Box<Formula>, Box<Formula>),
/// If and only if connective between two formulae.
Iff(Box<Formula<'a>>, Box<Formula<'a>>),
Iff(Box<Formula>, Box<Formula>),
}
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<RwLock<Vec<String>>>,
dict: Arc<RwLock<HashMap<String, usize>>>,
formulae: RefCell<Vec<Formula<'a>>>,
formulaname: RefCell<Vec<String>>,
pub struct AdfParser {
/// A name for each statement (identified by index in vector)
pub namelist: Arc<RwLock<Vec<String>>>,
/// Inverse mapping from name to index of statement in vector above
pub dict: Arc<RwLock<HashMap<String, usize>>>,
/// The formula (acceptance condition) for each statement identified by its index
pub formulae: RefCell<Vec<Formula>>,
/// The formula for each statement identified by its index
pub formulaname: RefCell<Vec<String>>,
}
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]);

2
server/docker-compose.yml
View File

@ -3,7 +3,7 @@ version: '3.1'
services:
mongo:
image: mongo
image: mongo:6
restart: always
ports:
- 27017:27017

121
server/src/adf.rs
View File

@ -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<Text<String>>, // Either Code or File is set
file: Option<TempFile>, // Either Code or File is set
parsing: Text<Parsing>,
is_af: Text<bool>, // 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<AddAdfProblemBodyMultipart> for AddAdfProblemBodyPlain {
@ -237,6 +242,7 @@ impl TryFrom<AddAdfProblemBodyMultipart> 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<Task>,
}
@ -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<Vec<usize>>);
impl From<AF> for AdfParser {
fn from(source: AF) -> Self {
let names: Vec<String> = (0..source.0.len())
.map(|val| (val + 1).to_string())
.collect();
let dict: HashMap<String, usize> = names
.iter()
.enumerate()
.map(|(i, val)| (val.clone(), i))
.collect();
let formulae: Vec<Formula> = 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<AdfParser, &'static str> {
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 <n>");
}
let Ok(num_arguments) = first_line[2].parse::<usize>() else {
return Err("Could not convert number of arguments to u32; expected first line to be of the form: p af <n>");
};
let attacks_opt: Option<Vec<(usize, usize)>> = 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::<usize>().ok()?, b.parse::<usize>().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<usize>> = 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()),