1
0
mirror of https://github.com/ellmau/adf-obdd.git synced 2025-12-20 09:39:38 +01:00

Add help texts to frontend

This commit is contained in:
monsterkrampe 2023-04-21 10:41:41 +02:00
parent 2bec9c49bf
commit 85bd732c21
No known key found for this signature in database
GPG Key ID: B8ADC1F5A5CE5057
11 changed files with 183 additions and 1 deletions

5
frontend/index.d.ts vendored Normal file
View File

@ -0,0 +1,5 @@
declare module 'bundle-text:*' {
const s: string
export default s
}

View File

@ -9,6 +9,7 @@
"build": "parcel build" "build": "parcel build"
}, },
"devDependencies": { "devDependencies": {
"@parcel/transformer-inline-string": "2.8.2",
"@types/node": "^18.15.11", "@types/node": "^18.15.11",
"@types/react": "^18.0.26", "@types/react": "^18.0.26",
"@types/react-dom": "^18.0.10", "@types/react-dom": "^18.0.10",
@ -29,7 +30,9 @@
"@emotion/react": "^11.10.5", "@emotion/react": "^11.10.5",
"@emotion/styled": "^11.10.5", "@emotion/styled": "^11.10.5",
"@fontsource/roboto": "^4.5.8", "@fontsource/roboto": "^4.5.8",
"@mui/icons-material": "^5.11.16",
"@mui/material": "^5.11.4", "@mui/material": "^5.11.4",
"markdown-to-jsx": "^7.2.0",
"react": "^18.2.0", "react": "^18.2.0",
"react-dom": "^18.2.0", "react-dom": "^18.2.0",
"react-router-dom": "^6.10.0" "react-router-dom": "^6.10.0"

View File

@ -3,11 +3,15 @@ import React, {
} from 'react'; } from 'react';
import { useParams, useNavigate } from 'react-router-dom'; import { useParams, useNavigate } from 'react-router-dom';
import { import {
Accordion,
AccordionDetails,
AccordionSummary,
Alert, Alert,
AlertColor, AlertColor,
Button, Button,
Chip, Chip,
Container, Container,
Grid,
Paper, Paper,
Pagination, Pagination,
Skeleton, Skeleton,
@ -18,6 +22,11 @@ import {
Typography, Typography,
} from '@mui/material'; } from '@mui/material';
import ExpandMoreIcon from '@mui/icons-material/ExpandMore';
import DetailInfoMd from 'bundle-text:../help-texts/detail-info.md';
import Markdown from './markdown';
import GraphG6, { GraphProps } from './graph-g6'; import GraphG6, { GraphProps } from './graph-g6';
import LoadingContext from './loading-context'; import LoadingContext from './loading-context';
import SnackbarContext from './snackbar-context'; import SnackbarContext from './snackbar-context';
@ -218,6 +227,27 @@ function AdfDetails() {
<Typography variant="h3" component="h1" align="center" gutterBottom> <Typography variant="h3" component="h1" align="center" gutterBottom>
ADF-BDD.DEV ADF-BDD.DEV
</Typography> </Typography>
<Container sx={{ marginTop: 2, marginBottom: 2 }}>
<Accordion>
<AccordionSummary expandIcon={<ExpandMoreIcon />}>
<span style={{ fontWeight: 'bold' }}>What can I do with the ADF now?</span>
</AccordionSummary>
<AccordionDetails>
<Grid container alignItems="center" spacing={2}>
<Grid item xs={12} sm={8}>
<Markdown>{DetailInfoMd}</Markdown>
</Grid>
<Grid item xs={12} sm={4}>
<img
src={new URL('../help-texts/example-bdd.png', import.meta.url).toString()}
alt="Example BDD"
style={{ maxWidth: '100%', borderRadius: 4, boxShadow: '0 0 5px 0 rgba(0,0,0,0.4)' }}
/>
</Grid>
</Grid>
</AccordionDetails>
</Accordion>
</Container>
<Container sx={{ marginBottom: 4 }}> <Container sx={{ marginBottom: 4 }}>
{problem ? ( {problem ? (
<> <>

View File

@ -122,7 +122,7 @@ function AdfNewForm({ fetchProblems }: { fetchProblems: () => void; }) {
For more info on the syntax, have a For more info on the syntax, have a
look look
{' '} {' '}
<Link href="https://github.com/ellmau/adf-obdd" target="_blank" rel="noreferrer">here</Link> <Link href="https://github.com/ellmau/adf-obdd" target="_blank" rel="noopener noreferrer">here</Link>
. .
</> </>
)} )}

View File

@ -7,6 +7,9 @@ import {
} from 'react-router-dom'; } from 'react-router-dom';
import { import {
Accordion,
AccordionDetails,
AccordionSummary,
Chip, Chip,
Container, Container,
Paper, Paper,
@ -19,6 +22,11 @@ import {
Typography, Typography,
} from '@mui/material'; } from '@mui/material';
import ExpandMoreIcon from '@mui/icons-material/ExpandMore';
import AddInfoMd from 'bundle-text:../help-texts/add-info.md';
import Markdown from './markdown';
import AdfNewForm from './adf-new-form'; import AdfNewForm from './adf-new-form';
import { import {
@ -102,6 +110,16 @@ function AdfOverview() {
<Typography variant="h3" component="h1" align="center" gutterBottom> <Typography variant="h3" component="h1" align="center" gutterBottom>
ADF-BDD.DEV ADF-BDD.DEV
</Typography> </Typography>
<Container sx={{ marginTop: 2, marginBottom: 2 }}>
<Accordion>
<AccordionSummary expandIcon={<ExpandMoreIcon />}>
<span style={{ fontWeight: 'bold' }}>What is this webapp doing and how should I use it?</span>
</AccordionSummary>
<AccordionDetails>
<Markdown>{AddInfoMd}</Markdown>
</AccordionDetails>
</Accordion>
</Container>
{problems.length > 0 {problems.length > 0
&& ( && (
<Container sx={{ marginBottom: 4 }}> <Container sx={{ marginBottom: 4 }}>

View File

@ -367,6 +367,12 @@ function GraphG6(props: Props) {
<span style={{ color: '#1976d2', marginRight: 8 }}>hi edge (condition is true)</span> <span style={{ color: '#1976d2', marginRight: 8 }}>hi edge (condition is true)</span>
{' '} {' '}
Click nodes to hightlight paths! (You can also drag and zoom.) Click nodes to hightlight paths! (You can also drag and zoom.)
<br />
The
{' '}
<span style={{ color: '#4caf50' }}>Root for: X</span>
{' '}
labels indicate where to start looking to determine the truth value of statement X.
</div> </div>
</> </>
); );

View File

@ -0,0 +1,58 @@
import React from 'react';
import ReactMarkdown from 'markdown-to-jsx';
import {
Box,
Link,
Typography,
} from '@mui/material';
const options = {
overrides: {
h1: {
component: Typography,
props: {
gutterBottom: true,
variant: 'h4',
},
},
h2: {
component: Typography,
props: { gutterBottom: true, variant: 'h6' },
},
h3: {
component: Typography,
props: { gutterBottom: true, variant: 'subtitle1' },
},
h4: {
component: Typography,
props: {
gutterBottom: true,
variant: 'caption',
paragraph: true,
},
},
p: {
component: Typography,
props: { paragraph: true, sx: { '&:last-child': { marginBottom: 0 } } },
},
a: {
component: (props: any) => (
// eslint-disable-next-line react/jsx-props-no-spreading
<Link target="_blank" rel="noopener noreferrer" {...props} />
),
},
li: {
component: (props: any) => (
<Box component="li" sx={{ mt: 1 }}>
{/* eslint-disable-next-line react/jsx-props-no-spreading */}
<Typography component="span" {...props} />
</Box>
),
},
},
};
export default function Markdown(props: any) {
// eslint-disable-next-line react/jsx-props-no-spreading
return <ReactMarkdown options={options} {...props} />;
}

View File

@ -0,0 +1,23 @@
ADF-BDD.dev allows you to solve Abstract Dialectical Frameworks (ADFs). The ADFs are represented as Binary Decision Diagrams (BDDs).
The Web UI mimics many options of the CLI version of the [underlying adf-bdd tool](https://github.com/ellmau/adf-obdd). The syntax for the ADF code is indentical.
In the below form, you can either type/paste your `code` or upload a file in the same format.
To put it briefly, an ADF consists of statements and accectance conditions for these statements.
For instance, the following code indicates that `a,b,c,d` are statements, that `a` is assumed to be true (verum), `b` is true if is true (which is tautological), `c` is true if `a` and `b` are true, and `d` is true if `b` is false.
```
s(a).
s(b).
s(c).
s(d).
ac(a,c(v)).
ac(b,b).
ac(c,and(a,b)).
ac(d,neg(b)).
```
Internally, the ADF is respresented as a BDD.
The `Parsing Strategy` determines the internal implementation used for these. `Naive` uses the own BDD implementation of our tool. `Hybrid` mixes our approaches with the existing Rust BDD library [`biodivine`](https://crates.io/crates/biodivine-lib-bdd). Don't be concerned about this choice if you are new to this tool; just pick either one.
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).

View File

@ -0,0 +1,13 @@
First of all you can review the code that you added. You can also delete the problem if you made a mistake or do not need it anymore.
Further below, you can have a look at the BDD representations of your problem using different semantics.
In principle, each statement gets it's own BDD that indicates how its truth value can be obtained from the other ones. Note that every BDD has the `BOT` and `TOP` nodes ultimately indicating the truth value (false or true respectively).
All these individual BDDs are displayed in a merged representation where the `Root for:` labels tell you where to start looking if you want to
get the truth value of an individual statement.
For instance, consider a BDD that (besides `BOT` and `TOP`) only contains a node `b` annotated with `Root for: a` and the annotation `Root for: b` at the `TOP` node.
Since the root for `b` is the `TOP` node, we know that `b` must be true. Then, to obtain the truth value for `a`, we start at the `b` and since we know that `b` must be true, we can follow the blue edge to obtain the value for `a` (we will end up in `BOT` or `TOP` there). If `b` would be false, we would follow the orange edge analogously. Note that is not always possible to directly determine the truth values of statements (which is exactly why we need tools like this).
On the very left, you can view the initial representation of your problem after parsing. This also indicates the parsing strategy that you have chosen (`Naive` or `Hybrid`).
The other tabs allow you to solve the problem using different semantics and optimizations. Some of them (e.g. `complete`) may produce multiple models that you can cycle through.
To get a better idea of the differences, you can have a look at the [command line tool](https://github.com/ellmau/adf-obdd/tree/main/bin).

Binary file not shown.

After

Width:  |  Height:  |  Size: 51 KiB

View File

@ -324,6 +324,13 @@
dependencies: dependencies:
regenerator-runtime "^0.13.11" regenerator-runtime "^0.13.11"
"@babel/runtime@^7.21.0":
version "7.21.0"
resolved "https://registry.yarnpkg.com/@babel/runtime/-/runtime-7.21.0.tgz#5b55c9d394e5fcf304909a8b00c07dc217b56673"
integrity sha512-xwII0//EObnq89Ji5AKYQaRYiW/nZ3llSv29d49IuxPhKbtJoLP+9QUUZ4nVragQVtaVGeZrpB+ZtG/Pdy/POw==
dependencies:
regenerator-runtime "^0.13.11"
"@babel/types@^7.18.6": "@babel/types@^7.18.6":
version "7.18.13" version "7.18.13"
resolved "https://registry.yarnpkg.com/@babel/types/-/types-7.18.13.tgz#30aeb9e514f4100f7c1cb6e5ba472b30e48f519a" resolved "https://registry.yarnpkg.com/@babel/types/-/types-7.18.13.tgz#30aeb9e514f4100f7c1cb6e5ba472b30e48f519a"
@ -620,6 +627,13 @@
resolved "https://registry.yarnpkg.com/@mui/core-downloads-tracker/-/core-downloads-tracker-5.11.4.tgz#def5937e21443b197fd1998fd66721bd9c49a1bb" resolved "https://registry.yarnpkg.com/@mui/core-downloads-tracker/-/core-downloads-tracker-5.11.4.tgz#def5937e21443b197fd1998fd66721bd9c49a1bb"
integrity sha512-jWVwGM3vG4O0sXcW0VcIl+njCWbGCBF5vvjRpuKJajrz51AD7D6+fP1SkInZXVk5pRHf6Bnk/Yj9Of9gXxb/hA== integrity sha512-jWVwGM3vG4O0sXcW0VcIl+njCWbGCBF5vvjRpuKJajrz51AD7D6+fP1SkInZXVk5pRHf6Bnk/Yj9Of9gXxb/hA==
"@mui/icons-material@^5.11.16":
version "5.11.16"
resolved "https://registry.yarnpkg.com/@mui/icons-material/-/icons-material-5.11.16.tgz#417fa773c56672e39d6ccfed9ac55591985f0d38"
integrity sha512-oKkx9z9Kwg40NtcIajF9uOXhxiyTZrrm9nmIJ4UjkU2IdHpd4QVLbCc/5hZN/y0C6qzi2Zlxyr9TGddQx2vx2A==
dependencies:
"@babel/runtime" "^7.21.0"
"@mui/material@^5.11.4": "@mui/material@^5.11.4":
version "5.11.4" version "5.11.4"
resolved "https://registry.yarnpkg.com/@mui/material/-/material-5.11.4.tgz#4dda0f993c9aa9678e1b9bce16adfe11e984dbd4" resolved "https://registry.yarnpkg.com/@mui/material/-/material-5.11.4.tgz#4dda0f993c9aa9678e1b9bce16adfe11e984dbd4"
@ -1139,6 +1153,13 @@
"@parcel/workers" "2.8.2" "@parcel/workers" "2.8.2"
nullthrows "^1.1.1" nullthrows "^1.1.1"
"@parcel/transformer-inline-string@2.8.2":
version "2.8.2"
resolved "https://registry.yarnpkg.com/@parcel/transformer-inline-string/-/transformer-inline-string-2.8.2.tgz#c2527b7e2a3d3432ee34044bc7419e9b6d624957"
integrity sha512-140SRnwKktVJB/McYlN0ub4NpdXECu0NesVf3ORPaG1WLF/ZxYVpLl60XBptoze9ezUqR6B6Z34fWXZiOcW09Q==
dependencies:
"@parcel/plugin" "2.8.2"
"@parcel/transformer-js@2.8.2": "@parcel/transformer-js@2.8.2":
version "2.8.2" version "2.8.2"
resolved "https://registry.yarnpkg.com/@parcel/transformer-js/-/transformer-js-2.8.2.tgz#cb7b954836011656f1807b2da1900377ebd16df6" resolved "https://registry.yarnpkg.com/@parcel/transformer-js/-/transformer-js-2.8.2.tgz#cb7b954836011656f1807b2da1900377ebd16df6"
@ -3173,6 +3194,11 @@ lru-cache@^6.0.0:
dependencies: dependencies:
yallist "^4.0.0" yallist "^4.0.0"
markdown-to-jsx@^7.2.0:
version "7.2.0"
resolved "https://registry.yarnpkg.com/markdown-to-jsx/-/markdown-to-jsx-7.2.0.tgz#e7b46b65955f6a04d48a753acd55874a14bdda4b"
integrity sha512-3l4/Bigjm4bEqjCR6Xr+d4DtM1X6vvtGsMGSjJYyep8RjjIvcWtrXBS8Wbfe1/P+atKNMccpsraESIaWVplzVg==
mdn-data@2.0.14: mdn-data@2.0.14:
version "2.0.14" version "2.0.14"
resolved "https://registry.yarnpkg.com/mdn-data/-/mdn-data-2.0.14.tgz#7113fc4281917d63ce29b43446f701e68c25ba50" resolved "https://registry.yarnpkg.com/mdn-data/-/mdn-data-2.0.14.tgz#7113fc4281917d63ce29b43446f701e68c25ba50"