mirror of
https://github.com/ellmau/adf-obdd.git
synced 2025-12-20 09:39:38 +01:00
Compare commits
2 Commits
7ddb013f12
...
fde9ce28c5
| Author | SHA1 | Date | |
|---|---|---|---|
|
fde9ce28c5 | ||
|
|
331836142c |
661
Cargo.lock
generated
661
Cargo.lock
generated
File diff suppressed because it is too large
Load Diff
@ -63,6 +63,7 @@ OPTIONS:
|
|||||||
#![deny(
|
#![deny(
|
||||||
missing_debug_implementations,
|
missing_debug_implementations,
|
||||||
missing_copy_implementations,
|
missing_copy_implementations,
|
||||||
|
missing_copy_implementations,
|
||||||
trivial_casts,
|
trivial_casts,
|
||||||
trivial_numeric_casts,
|
trivial_numeric_casts,
|
||||||
unsafe_code
|
unsafe_code
|
||||||
@ -180,7 +181,7 @@ impl App {
|
|||||||
let input = std::fs::read_to_string(self.input.clone()).expect("Error Reading File");
|
let input = std::fs::read_to_string(self.input.clone()).expect("Error Reading File");
|
||||||
match self.implementation.as_str() {
|
match self.implementation.as_str() {
|
||||||
"hybrid" => {
|
"hybrid" => {
|
||||||
let parser = AdfParser::default();
|
let parser = adf_bdd::parser::AdfParser::default();
|
||||||
match parser.parse()(&input) {
|
match parser.parse()(&input) {
|
||||||
Ok(_) => log::info!("[Done] parsing"),
|
Ok(_) => log::info!("[Done] parsing"),
|
||||||
Err(e) => {
|
Err(e) => {
|
||||||
@ -282,7 +283,7 @@ impl App {
|
|||||||
if self.counter.is_some() {
|
if self.counter.is_some() {
|
||||||
log::error!("Modelcounting not supported in biodivine mode");
|
log::error!("Modelcounting not supported in biodivine mode");
|
||||||
}
|
}
|
||||||
let parser = AdfParser::default();
|
let parser = adf_bdd::parser::AdfParser::default();
|
||||||
match parser.parse()(&input) {
|
match parser.parse()(&input) {
|
||||||
Ok(_) => log::info!("[Done] parsing"),
|
Ok(_) => log::info!("[Done] parsing"),
|
||||||
Err(e) => {
|
Err(e) => {
|
||||||
|
|||||||
18
flake.lock
generated
18
flake.lock
generated
@ -5,11 +5,11 @@
|
|||||||
"flake-utils": "flake-utils_2"
|
"flake-utils": "flake-utils_2"
|
||||||
},
|
},
|
||||||
"locked": {
|
"locked": {
|
||||||
"lastModified": 1738591040,
|
"lastModified": 1722363685,
|
||||||
"narHash": "sha256-4WNeriUToshQ/L5J+dTSWC5OJIwT39SEP7V7oylndi8=",
|
"narHash": "sha256-XCf2PIAT6lH7BwytgioPmVf/wkzXjSKScC4KzcZgb64=",
|
||||||
"owner": "gytis-ivaskevicius",
|
"owner": "gytis-ivaskevicius",
|
||||||
"repo": "flake-utils-plus",
|
"repo": "flake-utils-plus",
|
||||||
"rev": "afcb15b845e74ac5e998358709b2b5fe42a948d1",
|
"rev": "6b10f51ff73a66bb29f3bc8151a59d217713f496",
|
||||||
"type": "github"
|
"type": "github"
|
||||||
},
|
},
|
||||||
"original": {
|
"original": {
|
||||||
@ -38,11 +38,11 @@
|
|||||||
},
|
},
|
||||||
"nixpkgs": {
|
"nixpkgs": {
|
||||||
"locked": {
|
"locked": {
|
||||||
"lastModified": 1741724370,
|
"lastModified": 1736200483,
|
||||||
"narHash": "sha256-WsD+8uodhl58jzKKcPH4jH9dLTLFWZpVmGq4W1XDVF4=",
|
"narHash": "sha256-JO+lFN2HsCwSLMUWXHeOad6QUxOuwe9UOAF/iSl1J4I=",
|
||||||
"owner": "NixOS",
|
"owner": "NixOS",
|
||||||
"repo": "nixpkgs",
|
"repo": "nixpkgs",
|
||||||
"rev": "95600680c021743fd87b3e2fe13be7c290e1cac4",
|
"rev": "3f0a8ac25fb674611b98089ca3a5dd6480175751",
|
||||||
"type": "github"
|
"type": "github"
|
||||||
},
|
},
|
||||||
"original": {
|
"original": {
|
||||||
@ -66,11 +66,11 @@
|
|||||||
]
|
]
|
||||||
},
|
},
|
||||||
"locked": {
|
"locked": {
|
||||||
"lastModified": 1741833135,
|
"lastModified": 1736390353,
|
||||||
"narHash": "sha256-HUtFcF4NLwvu7CAowWgqCHXVkNj0EOc/W6Ism4biV6I=",
|
"narHash": "sha256-e2SP1zV9CISHlYZwEhwT53N9CW7yPh0tKTR0vuQqiWc=",
|
||||||
"owner": "oxalica",
|
"owner": "oxalica",
|
||||||
"repo": "rust-overlay",
|
"repo": "rust-overlay",
|
||||||
"rev": "f3cd1e0feb994188fe3ad9a5c3ab021ed433b8c8",
|
"rev": "1033caad3e26a56050de55ba0384df5ff0fa5ebd",
|
||||||
"type": "github"
|
"type": "github"
|
||||||
},
|
},
|
||||||
"original": {
|
"original": {
|
||||||
|
|||||||
@ -1,12 +1,9 @@
|
|||||||
<!doctype html>
|
<!DOCTYPE html>
|
||||||
<html>
|
<html>
|
||||||
<head>
|
<head>
|
||||||
<title>ADF-BDD.dev - Legal Notice</title>
|
<title>ADF-BDD.dev - Legal Notice</title>
|
||||||
<meta
|
<meta name="description" content="Impressum and Data Protection Regulation for adf-bdd.dev">
|
||||||
name="description"
|
<meta name="viewport" content="width=device-width, initial-scale=1">
|
||||||
content="Impressum and Data Protection Regulation for adf-bdd.dev"
|
|
||||||
/>
|
|
||||||
<meta name="viewport" content="width=device-width, initial-scale=1" />
|
|
||||||
<style>
|
<style>
|
||||||
body {
|
body {
|
||||||
font-family: Helvetica;
|
font-family: Helvetica;
|
||||||
@ -29,6 +26,7 @@
|
|||||||
</style>
|
</style>
|
||||||
</head>
|
</head>
|
||||||
<body>
|
<body>
|
||||||
|
|
||||||
<header>
|
<header>
|
||||||
<h1>ADF-BDD.DEV Legal Notice</h1>
|
<h1>ADF-BDD.DEV Legal Notice</h1>
|
||||||
</header>
|
</header>
|
||||||
@ -36,28 +34,21 @@
|
|||||||
<section>
|
<section>
|
||||||
<h2>Impressum</h2>
|
<h2>Impressum</h2>
|
||||||
|
|
||||||
The
|
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:
|
||||||
<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>
|
<h3>Responsibilities - Content and Technical Implementation</h3>
|
||||||
|
|
||||||
<p>
|
<p>
|
||||||
Dipl.-Inf. Lukas Gerlach<br />
|
Dipl.-Inf. Lukas Gerlach<br>
|
||||||
Technische Universität Dresden<br />
|
Technische Universität Dresden<br>
|
||||||
Fakultät Informatik<br />
|
Fakultät Informatik<br>
|
||||||
Institut für Theoretische Informatik<br />
|
Institut für Theoretische Informatik<br>
|
||||||
Professur für Wissensbasierte Systeme<br />
|
Professur für Wissensbasierte Systeme<br>
|
||||||
01062 Dresden<br />
|
01062 Dresden<br>
|
||||||
GERMANY
|
GERMANY
|
||||||
</p>
|
</p>
|
||||||
<p>
|
<p>
|
||||||
Email: lukas.gerlach@tu-dresden.de<br />
|
Email: lukas.gerlach@tu-dresden.de<br>
|
||||||
Phone: (+49) 351 / 463 43503
|
Phone: (+49) 351 / 463 43503
|
||||||
</p>
|
</p>
|
||||||
</section>
|
</section>
|
||||||
@ -65,148 +56,44 @@
|
|||||||
<section>
|
<section>
|
||||||
<h2>Data Protection Regulation</h2>
|
<h2>Data Protection Regulation</h2>
|
||||||
<p>
|
<p>
|
||||||
We process your personal data only in form of metadata that is
|
We process your personal data only in form of metadata that is send to us when you access the website.
|
||||||
send to us when you access the website. This is done to pursue
|
This is done to pursue our legitimate interest of providing and improving this publicly available website (https://adf-bdd.dev).
|
||||||
our legitimate interest of providing and improving this publicly
|
To this aim, this metadata is also written to server log files.
|
||||||
available website (https://adf-bdd.dev). To this aim, this
|
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.
|
||||||
metadata is also written to server log files. The data may
|
We only set cookies that are necessary for the provision of our service, i.e. to check if a user is logged in.
|
||||||
contain the following of your personal information: public IP
|
We do not set any so-called tracking cookies and we do not use any third party analytics tools on this website.
|
||||||
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>
|
</p>
|
||||||
<h3>Legal basis</h3>
|
<h3>Legal basis</h3>
|
||||||
<p>
|
<p>
|
||||||
The legal basis for the data processing is
|
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>.
|
||||||
<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>
|
</p>
|
||||||
<h3>Rights of data subjects</h3>
|
<h3>Rights of data subjects</h3>
|
||||||
<ul>
|
<ul>
|
||||||
<li>
|
<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>
|
||||||
You have the right to obtain information from TU Dresden
|
<li>You have the right to erasure or restriction of the processing and/or a right to object to the processing.</li>
|
||||||
about the data stored about your person and/or to have
|
<li>You can contact TU Dresden's Data Protection Officer at any time.
|
||||||
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>
|
<p>
|
||||||
Tel.: +49 351 / 463 32839<br />
|
Tel.: +49 351 / 463 32839<br>
|
||||||
Fax: +49 351 / 463 39718<br />
|
Fax: +49 351 / 463 39718<br>
|
||||||
Email: informationssicherheit@tu-dresden.de<br />
|
Email: informationssicherheit@tu-dresden.de<br>
|
||||||
<a
|
<a href="https://tu-dresden.de/informationssicherheit" target="_blank" rel="noreferrer noopener">https://tu-dresden.de/informationssicherheit</a>
|
||||||
href="https://tu-dresden.de/informationssicherheit"
|
|
||||||
target="_blank"
|
|
||||||
rel="noreferrer noopener"
|
|
||||||
>https://tu-dresden.de/informationssicherheit</a
|
|
||||||
>
|
|
||||||
</p>
|
</p>
|
||||||
</li>
|
</li>
|
||||||
<li>
|
<li>
|
||||||
You also have the right to complain to a supervisory
|
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:
|
||||||
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>
|
<p>
|
||||||
Saxon Data Protection Commissioner<br />
|
Saxon Data Protection Commissioner<br>
|
||||||
Ms. Dr. Juliane Hundert<br />
|
Ms. Dr. Juliane Hundert<br>
|
||||||
Devrientstraße 5<br />
|
Devrientstraße 5<br>
|
||||||
01067 Dresden<br />
|
01067 Dresden<br>
|
||||||
Email: saechsdsb@slt.sachsen.de<br />
|
Email: saechsdsb@slt.sachsen.de<br>
|
||||||
Phone: + 49 351 / 85471 101<br />
|
Phone: + 49 351 / 85471 101<br>
|
||||||
<a
|
<a href="http://www.datenschutz.sachsen.de" target="_blank" rel="noreferrer noopener">www.datenschutz.sachsen.de</a>
|
||||||
href="http://www.datenschutz.sachsen.de"
|
|
||||||
target="_blank"
|
|
||||||
rel="noreferrer noopener"
|
|
||||||
>www.datenschutz.sachsen.de</a
|
|
||||||
>
|
|
||||||
</p>
|
</p>
|
||||||
</li>
|
</li>
|
||||||
</ul>
|
</ul>
|
||||||
</section>
|
</section>
|
||||||
|
|
||||||
</body>
|
</body>
|
||||||
</html>
|
</html>
|
||||||
|
|
||||||
|
|||||||
@ -1133,7 +1133,12 @@ mod test {
|
|||||||
|
|
||||||
let grounded = adf.grounded();
|
let grounded = adf.grounded();
|
||||||
let (s, r) = unbounded();
|
let (s, r) = unbounded();
|
||||||
adf.nogood_internal(&grounded, heuristics::heu_simple, Adf::stability_check, s);
|
adf.nogood_internal(
|
||||||
|
&grounded,
|
||||||
|
heuristics::heu_simple,
|
||||||
|
Adf::stability_check,
|
||||||
|
s,
|
||||||
|
);
|
||||||
|
|
||||||
assert_eq!(
|
assert_eq!(
|
||||||
r.iter().collect::<Vec<_>>(),
|
r.iter().collect::<Vec<_>>(),
|
||||||
|
|||||||
@ -2,6 +2,7 @@
|
|||||||
//! utilising the biodivine-lib-bdd (see <https://github.com/sybila/biodivine-lib-bdd>) BDD implementation to compute various semantics.
|
//! utilising the biodivine-lib-bdd (see <https://github.com/sybila/biodivine-lib-bdd>) BDD implementation to compute various semantics.
|
||||||
//!
|
//!
|
||||||
//! These are currently the
|
//! These are currently the
|
||||||
|
//!
|
||||||
//! - grounded
|
//! - grounded
|
||||||
//! - stable
|
//! - stable
|
||||||
//! - complete
|
//! - complete
|
||||||
@ -322,15 +323,19 @@ impl Adf {
|
|||||||
fn stable_representation(&self) -> Bdd {
|
fn stable_representation(&self) -> Bdd {
|
||||||
log::debug!("[Start] stable representation rewriting");
|
log::debug!("[Start] stable representation rewriting");
|
||||||
self.ac.iter().enumerate().fold(
|
self.ac.iter().enumerate().fold(
|
||||||
self.varset.eval_expression(&BooleanExpression::Const(true)),
|
self.varset.eval_expression(
|
||||||
|
&BooleanExpression::Const(true),
|
||||||
|
),
|
||||||
|acc, (idx, formula)| {
|
|acc, (idx, formula)| {
|
||||||
acc.and(
|
acc.and(
|
||||||
&formula.iff(
|
&formula.iff(
|
||||||
&self.varset.eval_expression(&BooleanExpression::Variable(
|
&self.varset.eval_expression(
|
||||||
|
&BooleanExpression::Variable(
|
||||||
self.ordering
|
self.ordering
|
||||||
.name(crate::datatypes::Var(idx))
|
.name(crate::datatypes::Var(idx))
|
||||||
.expect("Variable should exist"),
|
.expect("Variable should exist"),
|
||||||
)),
|
),
|
||||||
|
),
|
||||||
),
|
),
|
||||||
)
|
)
|
||||||
},
|
},
|
||||||
|
|||||||
Loading…
x
Reference in New Issue
Block a user