mirror of
https://github.com/ellmau/adf-obdd.git
synced 2025-12-19 09:29:36 +01:00
Compare commits
4 Commits
7d1abef2ba
...
a0de86216d
| Author | SHA1 | Date | |
|---|---|---|---|
|
a0de86216d | ||
|
ca6c94f2e5 | ||
|
|
54e57e3820 | ||
|
|
18b55b1761 |
2001
Cargo.lock
generated
2001
Cargo.lock
generated
File diff suppressed because it is too large
Load Diff
@ -63,7 +63,6 @@ OPTIONS:
|
||||
#![deny(
|
||||
missing_debug_implementations,
|
||||
missing_copy_implementations,
|
||||
missing_copy_implementations,
|
||||
trivial_casts,
|
||||
trivial_numeric_casts,
|
||||
unsafe_code
|
||||
@ -181,7 +180,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 = adf_bdd::parser::AdfParser::default();
|
||||
let parser = AdfParser::default();
|
||||
match parser.parse()(&input) {
|
||||
Ok(_) => log::info!("[Done] parsing"),
|
||||
Err(e) => {
|
||||
@ -283,7 +282,7 @@ impl App {
|
||||
if self.counter.is_some() {
|
||||
log::error!("Modelcounting not supported in biodivine mode");
|
||||
}
|
||||
let parser = adf_bdd::parser::AdfParser::default();
|
||||
let 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": 1696331477,
|
||||
"narHash": "sha256-YkbRa/1wQWdWkVJ01JvV+75KIdM37UErqKgTf0L54Fk=",
|
||||
"lastModified": 1738591040,
|
||||
"narHash": "sha256-4WNeriUToshQ/L5J+dTSWC5OJIwT39SEP7V7oylndi8=",
|
||||
"owner": "gytis-ivaskevicius",
|
||||
"repo": "flake-utils-plus",
|
||||
"rev": "bfc53579db89de750b25b0c5e7af299e0c06d7d3",
|
||||
"rev": "afcb15b845e74ac5e998358709b2b5fe42a948d1",
|
||||
"type": "github"
|
||||
},
|
||||
"original": {
|
||||
@ -38,16 +38,16 @@
|
||||
},
|
||||
"nixpkgs": {
|
||||
"locked": {
|
||||
"lastModified": 1704290814,
|
||||
"narHash": "sha256-LWvKHp7kGxk/GEtlrGYV68qIvPHkU9iToomNFGagixU=",
|
||||
"lastModified": 1741724370,
|
||||
"narHash": "sha256-WsD+8uodhl58jzKKcPH4jH9dLTLFWZpVmGq4W1XDVF4=",
|
||||
"owner": "NixOS",
|
||||
"repo": "nixpkgs",
|
||||
"rev": "70bdadeb94ffc8806c0570eb5c2695ad29f0e421",
|
||||
"rev": "95600680c021743fd87b3e2fe13be7c290e1cac4",
|
||||
"type": "github"
|
||||
},
|
||||
"original": {
|
||||
"owner": "NixOS",
|
||||
"ref": "nixos-23.05",
|
||||
"ref": "nixos-24.11",
|
||||
"repo": "nixpkgs",
|
||||
"type": "github"
|
||||
}
|
||||
@ -61,20 +61,16 @@
|
||||
},
|
||||
"rust-overlay": {
|
||||
"inputs": {
|
||||
"flake-utils": [
|
||||
"flake-utils",
|
||||
"flake-utils"
|
||||
],
|
||||
"nixpkgs": [
|
||||
"nixpkgs"
|
||||
]
|
||||
},
|
||||
"locked": {
|
||||
"lastModified": 1704680242,
|
||||
"narHash": "sha256-5bD6iSPDgVTLly2gy2oJVwzuyuFZOz2p4qt8c8UoYIE=",
|
||||
"lastModified": 1741833135,
|
||||
"narHash": "sha256-HUtFcF4NLwvu7CAowWgqCHXVkNj0EOc/W6Ism4biV6I=",
|
||||
"owner": "oxalica",
|
||||
"repo": "rust-overlay",
|
||||
"rev": "2037779e018ebc2d381001a891e2a793fce7a74f",
|
||||
"rev": "f3cd1e0feb994188fe3ad9a5c3ab021ed433b8c8",
|
||||
"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-23.05";
|
||||
nixpkgs.url = "github:NixOS/nixpkgs/nixos-24.11";
|
||||
rust-overlay = {
|
||||
url = "github:oxalica/rust-overlay";
|
||||
inputs = {
|
||||
|
||||
@ -1,9 +1,12 @@
|
||||
<!DOCTYPE html>
|
||||
<!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">
|
||||
<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;
|
||||
@ -26,7 +29,6 @@
|
||||
</style>
|
||||
</head>
|
||||
<body>
|
||||
|
||||
<header>
|
||||
<h1>ADF-BDD.DEV Legal Notice</h1>
|
||||
</header>
|
||||
@ -34,21 +36,28 @@
|
||||
<section>
|
||||
<h2>Impressum</h2>
|
||||
|
||||
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:
|
||||
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:
|
||||
|
||||
<h3>Responsibilities - Content and Technical Implementation</h3>
|
||||
|
||||
<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>
|
||||
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>
|
||||
Email: lukas.gerlach@tu-dresden.de<br />
|
||||
Phone: (+49) 351 / 463 43503
|
||||
</p>
|
||||
</section>
|
||||
@ -56,44 +65,148 @@
|
||||
<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.
|
||||
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>
|
||||
|
||||
<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>
|
||||
|
||||
<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>.
|
||||
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.
|
||||
<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>
|
||||
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:
|
||||
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>
|
||||
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>
|
||||
</html>
|
||||
|
||||
|
||||
@ -1133,12 +1133,7 @@ mod test {
|
||||
|
||||
let grounded = adf.grounded();
|
||||
let (s, r) = unbounded();
|
||||
adf.nogood_internal(
|
||||
&grounded,
|
||||
crate::adf::heuristics::heu_simple,
|
||||
crate::adf::Adf::stability_check,
|
||||
s,
|
||||
);
|
||||
adf.nogood_internal(&grounded, heuristics::heu_simple, Adf::stability_check, s);
|
||||
|
||||
assert_eq!(
|
||||
r.iter().collect::<Vec<_>>(),
|
||||
@ -1172,8 +1167,8 @@ mod test {
|
||||
let (s, r) = unbounded();
|
||||
adf.nogood_internal(
|
||||
&grounded,
|
||||
crate::adf::heuristics::heu_simple,
|
||||
crate::adf::Adf::stability_check,
|
||||
heuristics::heu_simple,
|
||||
Adf::stability_check,
|
||||
s.clone(),
|
||||
);
|
||||
let stable_result = r.try_iter().collect::<Vec<_>>();
|
||||
|
||||
@ -5,6 +5,7 @@
|
||||
//! - grounded
|
||||
//! - stable
|
||||
//! - complete
|
||||
//!
|
||||
//! semantics of ADFs.
|
||||
|
||||
use crate::{
|
||||
@ -89,7 +90,7 @@ impl Adf {
|
||||
|
||||
pub(crate) fn stm_rewriting(&mut self, parser: &AdfParser) {
|
||||
let expr = parser.formula_order().iter().enumerate().fold(
|
||||
biodivine_lib_bdd::boolean_expression::BooleanExpression::Const(true),
|
||||
BooleanExpression::Const(true),
|
||||
|acc, (insert_order, new_order)| {
|
||||
BooleanExpression::And(
|
||||
Box::new(acc),
|
||||
@ -321,19 +322,15 @@ impl Adf {
|
||||
fn stable_representation(&self) -> Bdd {
|
||||
log::debug!("[Start] stable representation rewriting");
|
||||
self.ac.iter().enumerate().fold(
|
||||
self.varset.eval_expression(
|
||||
&biodivine_lib_bdd::boolean_expression::BooleanExpression::Const(true),
|
||||
),
|
||||
self.varset.eval_expression(&BooleanExpression::Const(true)),
|
||||
|acc, (idx, formula)| {
|
||||
acc.and(
|
||||
&formula.iff(
|
||||
&self.varset.eval_expression(
|
||||
&biodivine_lib_bdd::boolean_expression::BooleanExpression::Variable(
|
||||
&self.varset.eval_expression(&BooleanExpression::Variable(
|
||||
self.ordering
|
||||
.name(crate::datatypes::Var(idx))
|
||||
.expect("Variable should exist"),
|
||||
),
|
||||
),
|
||||
)),
|
||||
),
|
||||
)
|
||||
},
|
||||
@ -430,8 +427,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(&boolean_expression::BooleanExpression::Const(true));
|
||||
let f = variables.eval_expression(&boolean_expression::BooleanExpression::Const(false));
|
||||
let t = variables.eval_expression(&BooleanExpression::Const(true));
|
||||
let f = variables.eval_expression(&BooleanExpression::Const(false));
|
||||
|
||||
println!("{:?}", a.to_string());
|
||||
println!("{:?}", a.to_bytes());
|
||||
|
||||
@ -342,7 +342,6 @@ 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,6 +33,7 @@ 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();
|
||||
serde::Serialize::serialize(&container, ser)
|
||||
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<_> = serde::Deserialize::deserialize(des)?;
|
||||
let container: Vec<_> = Deserialize::deserialize(des)?;
|
||||
Ok(T::from_iter(container))
|
||||
}
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user