mirror of
https://github.com/ellmau/adf-obdd.git
synced 2025-12-20 09:39:38 +01:00
Compare commits
No commits in common. "ca6c94f2e55e3dcc15e3b5598413d7c21cae9f80" and "f601d473ccda5083c3fabd06320e94a935a74292" have entirely different histories.
ca6c94f2e5
...
f601d473cc
2003
Cargo.lock
generated
2003
Cargo.lock
generated
File diff suppressed because it is too large
Load Diff
@ -63,6 +63,7 @@ OPTIONS:
|
||||
#![deny(
|
||||
missing_debug_implementations,
|
||||
missing_copy_implementations,
|
||||
missing_copy_implementations,
|
||||
trivial_casts,
|
||||
trivial_numeric_casts,
|
||||
unsafe_code
|
||||
@ -180,7 +181,7 @@ impl App {
|
||||
let input = std::fs::read_to_string(self.input.clone()).expect("Error Reading File");
|
||||
match self.implementation.as_str() {
|
||||
"hybrid" => {
|
||||
let parser = AdfParser::default();
|
||||
let parser = adf_bdd::parser::AdfParser::default();
|
||||
match parser.parse()(&input) {
|
||||
Ok(_) => log::info!("[Done] parsing"),
|
||||
Err(e) => {
|
||||
@ -282,7 +283,7 @@ impl App {
|
||||
if self.counter.is_some() {
|
||||
log::error!("Modelcounting not supported in biodivine mode");
|
||||
}
|
||||
let parser = AdfParser::default();
|
||||
let parser = adf_bdd::parser::AdfParser::default();
|
||||
match parser.parse()(&input) {
|
||||
Ok(_) => log::info!("[Done] parsing"),
|
||||
Err(e) => {
|
||||
|
||||
24
flake.lock
generated
24
flake.lock
generated
@ -5,11 +5,11 @@
|
||||
"flake-utils": "flake-utils_2"
|
||||
},
|
||||
"locked": {
|
||||
"lastModified": 1738591040,
|
||||
"narHash": "sha256-4WNeriUToshQ/L5J+dTSWC5OJIwT39SEP7V7oylndi8=",
|
||||
"lastModified": 1696331477,
|
||||
"narHash": "sha256-YkbRa/1wQWdWkVJ01JvV+75KIdM37UErqKgTf0L54Fk=",
|
||||
"owner": "gytis-ivaskevicius",
|
||||
"repo": "flake-utils-plus",
|
||||
"rev": "afcb15b845e74ac5e998358709b2b5fe42a948d1",
|
||||
"rev": "bfc53579db89de750b25b0c5e7af299e0c06d7d3",
|
||||
"type": "github"
|
||||
},
|
||||
"original": {
|
||||
@ -38,16 +38,16 @@
|
||||
},
|
||||
"nixpkgs": {
|
||||
"locked": {
|
||||
"lastModified": 1741724370,
|
||||
"narHash": "sha256-WsD+8uodhl58jzKKcPH4jH9dLTLFWZpVmGq4W1XDVF4=",
|
||||
"lastModified": 1704290814,
|
||||
"narHash": "sha256-LWvKHp7kGxk/GEtlrGYV68qIvPHkU9iToomNFGagixU=",
|
||||
"owner": "NixOS",
|
||||
"repo": "nixpkgs",
|
||||
"rev": "95600680c021743fd87b3e2fe13be7c290e1cac4",
|
||||
"rev": "70bdadeb94ffc8806c0570eb5c2695ad29f0e421",
|
||||
"type": "github"
|
||||
},
|
||||
"original": {
|
||||
"owner": "NixOS",
|
||||
"ref": "nixos-24.11",
|
||||
"ref": "nixos-23.05",
|
||||
"repo": "nixpkgs",
|
||||
"type": "github"
|
||||
}
|
||||
@ -61,16 +61,20 @@
|
||||
},
|
||||
"rust-overlay": {
|
||||
"inputs": {
|
||||
"flake-utils": [
|
||||
"flake-utils",
|
||||
"flake-utils"
|
||||
],
|
||||
"nixpkgs": [
|
||||
"nixpkgs"
|
||||
]
|
||||
},
|
||||
"locked": {
|
||||
"lastModified": 1741833135,
|
||||
"narHash": "sha256-HUtFcF4NLwvu7CAowWgqCHXVkNj0EOc/W6Ism4biV6I=",
|
||||
"lastModified": 1704680242,
|
||||
"narHash": "sha256-5bD6iSPDgVTLly2gy2oJVwzuyuFZOz2p4qt8c8UoYIE=",
|
||||
"owner": "oxalica",
|
||||
"repo": "rust-overlay",
|
||||
"rev": "f3cd1e0feb994188fe3ad9a5c3ab021ed433b8c8",
|
||||
"rev": "2037779e018ebc2d381001a891e2a793fce7a74f",
|
||||
"type": "github"
|
||||
},
|
||||
"original": {
|
||||
|
||||
@ -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-23.05";
|
||||
rust-overlay = {
|
||||
url = "github:oxalica/rust-overlay";
|
||||
inputs = {
|
||||
|
||||
@ -1,212 +1,99 @@
|
||||
<!doctype html>
|
||||
<html>
|
||||
<head>
|
||||
<title>ADF-BDD.dev - Legal Notice</title>
|
||||
<meta
|
||||
name="description"
|
||||
content="Impressum and Data Protection Regulation for adf-bdd.dev"
|
||||
/>
|
||||
<meta name="viewport" content="width=device-width, initial-scale=1" />
|
||||
<style>
|
||||
body {
|
||||
font-family: Helvetica;
|
||||
}
|
||||
h1 {
|
||||
text-align: center;
|
||||
}
|
||||
section {
|
||||
max-width: 1000px;
|
||||
margin: 0 auto 32px;
|
||||
padding: 16px;
|
||||
box-shadow: 0 0 10px 0px rgba(0, 0, 0, 0.4);
|
||||
}
|
||||
section > :first-child {
|
||||
margin-top: 0;
|
||||
}
|
||||
section > :last-child {
|
||||
margin-bottom: 0;
|
||||
}
|
||||
</style>
|
||||
</head>
|
||||
<body>
|
||||
<header>
|
||||
<h1>ADF-BDD.DEV Legal Notice</h1>
|
||||
</header>
|
||||
<!DOCTYPE html>
|
||||
<html>
|
||||
<head>
|
||||
<title>ADF-BDD.dev - Legal Notice</title>
|
||||
<meta name="description" content="Impressum and Data Protection Regulation for adf-bdd.dev">
|
||||
<meta name="viewport" content="width=device-width, initial-scale=1">
|
||||
<style>
|
||||
body {
|
||||
font-family: Helvetica;
|
||||
}
|
||||
h1 {
|
||||
text-align: center;
|
||||
}
|
||||
section {
|
||||
max-width: 1000px;
|
||||
margin: 0 auto 32px;
|
||||
padding: 16px;
|
||||
box-shadow: 0 0 10px 0px rgba(0,0,0,0.4);
|
||||
}
|
||||
section > :first-child {
|
||||
margin-top: 0;
|
||||
}
|
||||
section > :last-child {
|
||||
margin-bottom: 0;
|
||||
}
|
||||
</style>
|
||||
</head>
|
||||
<body>
|
||||
|
||||
<section>
|
||||
<h2>Impressum</h2>
|
||||
<header>
|
||||
<h1>ADF-BDD.DEV Legal Notice</h1>
|
||||
</header>
|
||||
|
||||
The
|
||||
<a
|
||||
href="https://tu-dresden.de/impressum?set_language=en"
|
||||
target="_blank"
|
||||
rel="noreferrer noopener"
|
||||
>Impressum of TU Dresden</a
|
||||
>
|
||||
applies with the following amendments:
|
||||
<section>
|
||||
<h2>Impressum</h2>
|
||||
|
||||
<h3>Responsibilities - Content and Technical Implementation</h3>
|
||||
The <a href="https://tu-dresden.de/impressum?set_language=en" target="_blank" rel="noreferrer noopener">Impressum of TU Dresden</a> applies with the following amendments:
|
||||
|
||||
<p>
|
||||
Dipl.-Inf. Lukas Gerlach<br />
|
||||
Technische Universität Dresden<br />
|
||||
Fakultät Informatik<br />
|
||||
Institut für Theoretische Informatik<br />
|
||||
Professur für Wissensbasierte Systeme<br />
|
||||
01062 Dresden<br />
|
||||
GERMANY
|
||||
</p>
|
||||
<p>
|
||||
Email: lukas.gerlach@tu-dresden.de<br />
|
||||
Phone: (+49) 351 / 463 43503
|
||||
</p>
|
||||
</section>
|
||||
<h3>Responsibilities - Content and Technical Implementation</h3>
|
||||
|
||||
<section>
|
||||
<h2>Data Protection Regulation</h2>
|
||||
<p>
|
||||
We process your personal data only in form of metadata that is
|
||||
send to us when you access the website. This is done to pursue
|
||||
our legitimate interest of providing and improving this publicly
|
||||
available website (https://adf-bdd.dev). To this aim, this
|
||||
metadata is also written to server log files. The data may
|
||||
contain the following of your personal information: public IP
|
||||
address, time of access, internet browser (e.g. user agent,
|
||||
version), operating system, referrer url, hostname of requesting
|
||||
machine. We only set cookies that are necessary for the
|
||||
provision of our service, i.e. to check if a user is logged in.
|
||||
</p>
|
||||
<h3>
|
||||
Data Processed for Website Provisioning and Log File Creation:
|
||||
Log Files for Website Provisioning
|
||||
</h3>
|
||||
<p>
|
||||
We use Cloudflare to resolve DNS requests for our website. To
|
||||
ensure the security and performance of our website, we log
|
||||
technical errors that may occur when accessing our website.
|
||||
Additionally, information that your device's browser
|
||||
automatically transmits to our server is collected. This
|
||||
information includes:
|
||||
</p>
|
||||
<p>
|
||||
Dipl.-Inf. Lukas Gerlach<br>
|
||||
Technische Universität Dresden<br>
|
||||
Fakultät Informatik<br>
|
||||
Institut für Theoretische Informatik<br>
|
||||
Professur für Wissensbasierte Systeme<br>
|
||||
01062 Dresden<br>
|
||||
GERMANY
|
||||
</p>
|
||||
<p>
|
||||
Email: lukas.gerlach@tu-dresden.de<br>
|
||||
Phone: (+49) 351 / 463 43503
|
||||
</p>
|
||||
</section>
|
||||
|
||||
<ul>
|
||||
<li>IP address and operating system of your device,</li>
|
||||
<li>Browser type, version, language,</li>
|
||||
<li>
|
||||
The website from which the access was made (referrer URL),
|
||||
</li>
|
||||
<li>The status code (e.g., 404), and</li>
|
||||
<li>The transmission protocol used (e.g., http/2).</li>
|
||||
</ul>
|
||||
<section>
|
||||
<h2>Data Protection Regulation</h2>
|
||||
<p>
|
||||
We process your personal data only in form of metadata that is send to us when you access the website.
|
||||
This is done to pursue our legitimate interest of providing and improving this publicly available website (https://adf-bdd.dev).
|
||||
To this aim, this metadata is also written to server log files.
|
||||
The data may contain the following of your personal information: public IP address, time of access, internet browser (e.g. user agent, version), operating system, referrer url, hostname of requesting machine.
|
||||
We only set cookies that are necessary for the provision of our service, i.e. to check if a user is logged in.
|
||||
We do not set any so-called tracking cookies and we do not use any third party analytics tools on this website.
|
||||
</p>
|
||||
<h3>Legal basis</h3>
|
||||
<p>
|
||||
The legal basis for the data processing is <a href="https://gdpr.eu/article-6-how-to-process-personal-data-legally/" target="_blank" rel="noreferrer noopener">Section §6 para.1 lit. f GDPR</a>.
|
||||
</p>
|
||||
<h3>Rights of data subjects</h3>
|
||||
<ul>
|
||||
<li>You have the right to obtain information from TU Dresden about the data stored about your person and/or to have incorrectly stored data corrected.</li>
|
||||
<li>You have the right to erasure or restriction of the processing and/or a right to object to the processing.</li>
|
||||
<li>You can contact TU Dresden's Data Protection Officer at any time.
|
||||
<p>
|
||||
Tel.: +49 351 / 463 32839<br>
|
||||
Fax: +49 351 / 463 39718<br>
|
||||
Email: informationssicherheit@tu-dresden.de<br>
|
||||
<a href="https://tu-dresden.de/informationssicherheit" target="_blank" rel="noreferrer noopener">https://tu-dresden.de/informationssicherheit</a>
|
||||
</p>
|
||||
</li>
|
||||
<li>
|
||||
You also have the right to complain to a supervisory authority if you are concerned that the processing of your personal data is an infringement of the law. The competent supervisory authority for data protection is:
|
||||
<p>
|
||||
Saxon Data Protection Commissioner<br>
|
||||
Ms. Dr. Juliane Hundert<br>
|
||||
Devrientstraße 5<br>
|
||||
01067 Dresden<br>
|
||||
Email: saechsdsb@slt.sachsen.de<br>
|
||||
Phone: + 49 351 / 85471 101<br>
|
||||
<a href="http://www.datenschutz.sachsen.de" target="_blank" rel="noreferrer noopener">www.datenschutz.sachsen.de</a>
|
||||
</p>
|
||||
</li>
|
||||
</ul>
|
||||
</section>
|
||||
|
||||
<p>
|
||||
The processing of this data is based on our legitimate interest
|
||||
according to Art. 6(1)(f) GDPR. Our legitimate interest lies in
|
||||
troubleshooting, optimizing, and ensuring the performance of our
|
||||
website, as well as guaranteeing the security of our network and
|
||||
systems. We do not use the data to personally identify
|
||||
individual users unless there is a legal reason to do so or
|
||||
explicit consent is obtained from you.
|
||||
</p>
|
||||
|
||||
<p>
|
||||
Cloudflare acts as an intermediary between your browser and our
|
||||
server. When a DNS record is set to "Proxied," Cloudflare
|
||||
answers DNS queries with a Cloudflare Anycast IP address instead
|
||||
of the actual IP address of our server. This directs HTTP/HTTPS
|
||||
requests to the Cloudflare network, which offers advantages in
|
||||
terms of security and performance. Cloudflare also hides the IP
|
||||
address of our origin server, making it more difficult for
|
||||
attackers to directly target it.
|
||||
</p>
|
||||
|
||||
<p>
|
||||
Cloudflare may store certain data related to DNS requests,
|
||||
including IP addresses. However, Cloudflare anonymizes IP
|
||||
addresses by truncating the last octets for IPv4 and the last 80
|
||||
bits for IPv6. The truncated IP addresses are deleted within 25
|
||||
hours. Cloudflare is committed to not selling or sharing users'
|
||||
personal data with third parties and not using the data for
|
||||
targeted advertising. For more information on data protection at
|
||||
Cloudflare, please see the Cloudflare Privacy Policy:
|
||||
<a href="https://www.cloudflare.com/de-de/privacypolicy/"
|
||||
>https://www.cloudflare.com/de-de/privacypolicy/</a
|
||||
>
|
||||
</p>
|
||||
|
||||
<p>
|
||||
To meet the requirements of the GDPR, we have entered into a
|
||||
Data Processing Agreement (DPA) with Cloudflare, which ensures
|
||||
that Cloudflare processes the data on our behalf and in
|
||||
accordance with applicable data protection regulations. You have
|
||||
the right to access, rectify, erase, restrict processing, and
|
||||
data portability of your personal data. Please contact us if you
|
||||
wish to exercise these rights.
|
||||
</p>
|
||||
|
||||
<p>
|
||||
Please note that our website is hosted on our own servers, and
|
||||
Cloudflare merely serves as a DNS provider and proxy. We
|
||||
implement appropriate technical and organizational measures to
|
||||
ensure the protection of your data.
|
||||
</p>
|
||||
<h3>Legal basis</h3>
|
||||
<p>
|
||||
The legal basis for the data processing is
|
||||
<a
|
||||
href="https://gdpr.eu/article-6-how-to-process-personal-data-legally/"
|
||||
target="_blank"
|
||||
rel="noreferrer noopener"
|
||||
>Section §6 para.1 lit. f GDPR</a
|
||||
>.
|
||||
</p>
|
||||
<h3>Rights of data subjects</h3>
|
||||
<ul>
|
||||
<li>
|
||||
You have the right to obtain information from TU Dresden
|
||||
about the data stored about your person and/or to have
|
||||
incorrectly stored data corrected.
|
||||
</li>
|
||||
<li>
|
||||
You have the right to erasure or restriction of the
|
||||
processing and/or a right to object to the processing.
|
||||
</li>
|
||||
<li>
|
||||
You can contact TU Dresden's Data Protection Officer at any
|
||||
time.
|
||||
<p>
|
||||
Tel.: +49 351 / 463 32839<br />
|
||||
Fax: +49 351 / 463 39718<br />
|
||||
Email: informationssicherheit@tu-dresden.de<br />
|
||||
<a
|
||||
href="https://tu-dresden.de/informationssicherheit"
|
||||
target="_blank"
|
||||
rel="noreferrer noopener"
|
||||
>https://tu-dresden.de/informationssicherheit</a
|
||||
>
|
||||
</p>
|
||||
</li>
|
||||
<li>
|
||||
You also have the right to complain to a supervisory
|
||||
authority if you are concerned that the processing of your
|
||||
personal data is an infringement of the law. The competent
|
||||
supervisory authority for data protection is:
|
||||
<p>
|
||||
Saxon Data Protection Commissioner<br />
|
||||
Ms. Dr. Juliane Hundert<br />
|
||||
Devrientstraße 5<br />
|
||||
01067 Dresden<br />
|
||||
Email: saechsdsb@slt.sachsen.de<br />
|
||||
Phone: + 49 351 / 85471 101<br />
|
||||
<a
|
||||
href="http://www.datenschutz.sachsen.de"
|
||||
target="_blank"
|
||||
rel="noreferrer noopener"
|
||||
>www.datenschutz.sachsen.de</a
|
||||
>
|
||||
</p>
|
||||
</li>
|
||||
</ul>
|
||||
</section>
|
||||
</body>
|
||||
</body>
|
||||
</html>
|
||||
|
||||
|
||||
@ -1133,7 +1133,12 @@ mod test {
|
||||
|
||||
let grounded = adf.grounded();
|
||||
let (s, r) = unbounded();
|
||||
adf.nogood_internal(&grounded, heuristics::heu_simple, Adf::stability_check, s);
|
||||
adf.nogood_internal(
|
||||
&grounded,
|
||||
crate::adf::heuristics::heu_simple,
|
||||
crate::adf::Adf::stability_check,
|
||||
s,
|
||||
);
|
||||
|
||||
assert_eq!(
|
||||
r.iter().collect::<Vec<_>>(),
|
||||
@ -1167,8 +1172,8 @@ mod test {
|
||||
let (s, r) = unbounded();
|
||||
adf.nogood_internal(
|
||||
&grounded,
|
||||
heuristics::heu_simple,
|
||||
Adf::stability_check,
|
||||
crate::adf::heuristics::heu_simple,
|
||||
crate::adf::Adf::stability_check,
|
||||
s.clone(),
|
||||
);
|
||||
let stable_result = r.try_iter().collect::<Vec<_>>();
|
||||
|
||||
@ -5,7 +5,6 @@
|
||||
//! - grounded
|
||||
//! - stable
|
||||
//! - complete
|
||||
//!
|
||||
//! semantics of ADFs.
|
||||
|
||||
use crate::{
|
||||
@ -90,7 +89,7 @@ impl Adf {
|
||||
|
||||
pub(crate) fn stm_rewriting(&mut self, parser: &AdfParser) {
|
||||
let expr = parser.formula_order().iter().enumerate().fold(
|
||||
BooleanExpression::Const(true),
|
||||
biodivine_lib_bdd::boolean_expression::BooleanExpression::Const(true),
|
||||
|acc, (insert_order, new_order)| {
|
||||
BooleanExpression::And(
|
||||
Box::new(acc),
|
||||
@ -322,15 +321,19 @@ impl Adf {
|
||||
fn stable_representation(&self) -> Bdd {
|
||||
log::debug!("[Start] stable representation rewriting");
|
||||
self.ac.iter().enumerate().fold(
|
||||
self.varset.eval_expression(&BooleanExpression::Const(true)),
|
||||
self.varset.eval_expression(
|
||||
&biodivine_lib_bdd::boolean_expression::BooleanExpression::Const(true),
|
||||
),
|
||||
|acc, (idx, formula)| {
|
||||
acc.and(
|
||||
&formula.iff(
|
||||
&self.varset.eval_expression(&BooleanExpression::Variable(
|
||||
self.ordering
|
||||
.name(crate::datatypes::Var(idx))
|
||||
.expect("Variable should exist"),
|
||||
)),
|
||||
&self.varset.eval_expression(
|
||||
&biodivine_lib_bdd::boolean_expression::BooleanExpression::Variable(
|
||||
self.ordering
|
||||
.name(crate::datatypes::Var(idx))
|
||||
.expect("Variable should exist"),
|
||||
),
|
||||
),
|
||||
),
|
||||
)
|
||||
},
|
||||
@ -427,8 +430,8 @@ mod test {
|
||||
let c = variables.eval_expression_string("c");
|
||||
let d = variables.eval_expression_string("a & b & c");
|
||||
let e = variables.eval_expression_string("a ^ b");
|
||||
let t = variables.eval_expression(&BooleanExpression::Const(true));
|
||||
let f = variables.eval_expression(&BooleanExpression::Const(false));
|
||||
let t = variables.eval_expression(&boolean_expression::BooleanExpression::Const(true));
|
||||
let f = variables.eval_expression(&boolean_expression::BooleanExpression::Const(false));
|
||||
|
||||
println!("{:?}", a.to_string());
|
||||
println!("{:?}", a.to_bytes());
|
||||
|
||||
@ -342,6 +342,7 @@ let parsed_adf: Adf = parsed_custom_adf.into();
|
||||
#![deny(
|
||||
missing_debug_implementations,
|
||||
missing_copy_implementations,
|
||||
missing_copy_implementations,
|
||||
trivial_casts,
|
||||
trivial_numeric_casts,
|
||||
unsafe_code
|
||||
|
||||
@ -33,7 +33,6 @@ impl super::Bdd {
|
||||
/// # Attention
|
||||
/// - Constants for [`⊤`][crate::datatypes::Term::TOP] and [`⊥`][crate::datatypes::Term::BOT] concepts are not sent, as they are considered to be existing in every [Bdd][super::Bdd] structure.
|
||||
/// - Mixing manipulating operations and utilising the communication channel for a receiving [roBDD][super::Bdd] may end up in inconsistent data.
|
||||
///
|
||||
/// So far, only manipulate the [roBDD][super::Bdd] if no further [recv][Self::recv] will be called.
|
||||
pub fn with_sender_receiver(
|
||||
sender: crossbeam_channel::Sender<BddNode>,
|
||||
|
||||
@ -11,7 +11,7 @@ where
|
||||
V: Serialize + 'a,
|
||||
{
|
||||
let container: Vec<_> = target.into_iter().collect();
|
||||
Serialize::serialize(&container, ser)
|
||||
serde::Serialize::serialize(&container, ser)
|
||||
}
|
||||
|
||||
/// Deserialize from a [Vector][std::vec::Vec] to a [Map][std::collections::HashMap].
|
||||
@ -22,6 +22,6 @@ where
|
||||
K: Deserialize<'de>,
|
||||
V: Deserialize<'de>,
|
||||
{
|
||||
let container: Vec<_> = Deserialize::deserialize(des)?;
|
||||
let container: Vec<_> = serde::Deserialize::deserialize(des)?;
|
||||
Ok(T::from_iter(container))
|
||||
}
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user