mirror of
https://github.com/ellmau/adf-obdd.git
synced 2025-12-20 09:39:38 +01:00
Compare commits
3 Commits
fde9ce28c5
...
7ddb013f12
| Author | SHA1 | Date | |
|---|---|---|---|
|
7ddb013f12 | ||
|
ca6c94f2e5 | ||
|
|
54e57e3820 |
663
Cargo.lock
generated
663
Cargo.lock
generated
File diff suppressed because it is too large
Load Diff
@ -63,7 +63,6 @@ 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
|
||||||
@ -181,7 +180,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 = adf_bdd::parser::AdfParser::default();
|
let 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) => {
|
||||||
@ -283,7 +282,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 = adf_bdd::parser::AdfParser::default();
|
let 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": 1722363685,
|
"lastModified": 1738591040,
|
||||||
"narHash": "sha256-XCf2PIAT6lH7BwytgioPmVf/wkzXjSKScC4KzcZgb64=",
|
"narHash": "sha256-4WNeriUToshQ/L5J+dTSWC5OJIwT39SEP7V7oylndi8=",
|
||||||
"owner": "gytis-ivaskevicius",
|
"owner": "gytis-ivaskevicius",
|
||||||
"repo": "flake-utils-plus",
|
"repo": "flake-utils-plus",
|
||||||
"rev": "6b10f51ff73a66bb29f3bc8151a59d217713f496",
|
"rev": "afcb15b845e74ac5e998358709b2b5fe42a948d1",
|
||||||
"type": "github"
|
"type": "github"
|
||||||
},
|
},
|
||||||
"original": {
|
"original": {
|
||||||
@ -38,11 +38,11 @@
|
|||||||
},
|
},
|
||||||
"nixpkgs": {
|
"nixpkgs": {
|
||||||
"locked": {
|
"locked": {
|
||||||
"lastModified": 1736200483,
|
"lastModified": 1741724370,
|
||||||
"narHash": "sha256-JO+lFN2HsCwSLMUWXHeOad6QUxOuwe9UOAF/iSl1J4I=",
|
"narHash": "sha256-WsD+8uodhl58jzKKcPH4jH9dLTLFWZpVmGq4W1XDVF4=",
|
||||||
"owner": "NixOS",
|
"owner": "NixOS",
|
||||||
"repo": "nixpkgs",
|
"repo": "nixpkgs",
|
||||||
"rev": "3f0a8ac25fb674611b98089ca3a5dd6480175751",
|
"rev": "95600680c021743fd87b3e2fe13be7c290e1cac4",
|
||||||
"type": "github"
|
"type": "github"
|
||||||
},
|
},
|
||||||
"original": {
|
"original": {
|
||||||
@ -66,11 +66,11 @@
|
|||||||
]
|
]
|
||||||
},
|
},
|
||||||
"locked": {
|
"locked": {
|
||||||
"lastModified": 1736390353,
|
"lastModified": 1741833135,
|
||||||
"narHash": "sha256-e2SP1zV9CISHlYZwEhwT53N9CW7yPh0tKTR0vuQqiWc=",
|
"narHash": "sha256-HUtFcF4NLwvu7CAowWgqCHXVkNj0EOc/W6Ism4biV6I=",
|
||||||
"owner": "oxalica",
|
"owner": "oxalica",
|
||||||
"repo": "rust-overlay",
|
"repo": "rust-overlay",
|
||||||
"rev": "1033caad3e26a56050de55ba0384df5ff0fa5ebd",
|
"rev": "f3cd1e0feb994188fe3ad9a5c3ab021ed433b8c8",
|
||||||
"type": "github"
|
"type": "github"
|
||||||
},
|
},
|
||||||
"original": {
|
"original": {
|
||||||
|
|||||||
@ -1,9 +1,12 @@
|
|||||||
<!DOCTYPE html>
|
<!doctype html>
|
||||||
<html>
|
<html>
|
||||||
<head>
|
<head>
|
||||||
<title>ADF-BDD.dev - Legal Notice</title>
|
<title>ADF-BDD.dev - Legal Notice</title>
|
||||||
<meta name="description" content="Impressum and Data Protection Regulation for adf-bdd.dev">
|
<meta
|
||||||
<meta name="viewport" content="width=device-width, initial-scale=1">
|
name="description"
|
||||||
|
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;
|
||||||
@ -15,7 +18,7 @@
|
|||||||
max-width: 1000px;
|
max-width: 1000px;
|
||||||
margin: 0 auto 32px;
|
margin: 0 auto 32px;
|
||||||
padding: 16px;
|
padding: 16px;
|
||||||
box-shadow: 0 0 10px 0px rgba(0,0,0,0.4);
|
box-shadow: 0 0 10px 0px rgba(0, 0, 0, 0.4);
|
||||||
}
|
}
|
||||||
section > :first-child {
|
section > :first-child {
|
||||||
margin-top: 0;
|
margin-top: 0;
|
||||||
@ -24,76 +27,186 @@
|
|||||||
margin-bottom: 0;
|
margin-bottom: 0;
|
||||||
}
|
}
|
||||||
</style>
|
</style>
|
||||||
</head>
|
</head>
|
||||||
<body>
|
<body>
|
||||||
|
<header>
|
||||||
<header>
|
|
||||||
<h1>ADF-BDD.DEV Legal Notice</h1>
|
<h1>ADF-BDD.DEV Legal Notice</h1>
|
||||||
</header>
|
</header>
|
||||||
|
|
||||||
<section>
|
<section>
|
||||||
<h2>Impressum</h2>
|
<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>
|
<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>
|
||||||
|
|
||||||
<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 send to us when you access the website.
|
We process your personal data only in form of metadata that is
|
||||||
This is done to pursue our legitimate interest of providing and improving this publicly available website (https://adf-bdd.dev).
|
send to us when you access the website. This is done to pursue
|
||||||
To this aim, this metadata is also written to server log files.
|
our legitimate interest of providing and improving this publicly
|
||||||
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.
|
available website (https://adf-bdd.dev). To this aim, this
|
||||||
We only set cookies that are necessary for the provision of our service, i.e. to check if a user is logged in.
|
metadata is also written to server log files. The data may
|
||||||
We do not set any so-called tracking cookies and we do not use any third party analytics tools on this website.
|
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>
|
</p>
|
||||||
<h3>Legal basis</h3>
|
<h3>Legal basis</h3>
|
||||||
<p>
|
<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>
|
</p>
|
||||||
<h3>Rights of data subjects</h3>
|
<h3>Rights of data subjects</h3>
|
||||||
<ul>
|
<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>
|
||||||
<li>You have the right to erasure or restriction of the processing and/or a right to object to the processing.</li>
|
You have the right to obtain information from TU Dresden
|
||||||
<li>You can contact TU Dresden's Data Protection Officer at any time.
|
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>
|
<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 href="https://tu-dresden.de/informationssicherheit" target="_blank" rel="noreferrer noopener">https://tu-dresden.de/informationssicherheit</a>
|
<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 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>
|
<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 href="http://www.datenschutz.sachsen.de" target="_blank" rel="noreferrer noopener">www.datenschutz.sachsen.de</a>
|
<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,12 +1133,7 @@ mod test {
|
|||||||
|
|
||||||
let grounded = adf.grounded();
|
let grounded = adf.grounded();
|
||||||
let (s, r) = unbounded();
|
let (s, r) = unbounded();
|
||||||
adf.nogood_internal(
|
adf.nogood_internal(&grounded, heuristics::heu_simple, Adf::stability_check, s);
|
||||||
&grounded,
|
|
||||||
heuristics::heu_simple,
|
|
||||||
Adf::stability_check,
|
|
||||||
s,
|
|
||||||
);
|
|
||||||
|
|
||||||
assert_eq!(
|
assert_eq!(
|
||||||
r.iter().collect::<Vec<_>>(),
|
r.iter().collect::<Vec<_>>(),
|
||||||
|
|||||||
@ -2,7 +2,6 @@
|
|||||||
//! 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
|
||||||
@ -323,19 +322,15 @@ 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(
|
self.varset.eval_expression(&BooleanExpression::Const(true)),
|
||||||
&BooleanExpression::Const(true),
|
|
||||||
),
|
|
||||||
|acc, (idx, formula)| {
|
|acc, (idx, formula)| {
|
||||||
acc.and(
|
acc.and(
|
||||||
&formula.iff(
|
&formula.iff(
|
||||||
&self.varset.eval_expression(
|
&self.varset.eval_expression(&BooleanExpression::Variable(
|
||||||
&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