diff --git a/frontend/index.d.ts b/frontend/index.d.ts new file mode 100644 index 0000000..52e4387 --- /dev/null +++ b/frontend/index.d.ts @@ -0,0 +1,5 @@ +declare module 'bundle-text:*' { + const s: string + export default s +} + diff --git a/frontend/package.json b/frontend/package.json index 5914cb1..e530577 100644 --- a/frontend/package.json +++ b/frontend/package.json @@ -9,6 +9,7 @@ "build": "parcel build" }, "devDependencies": { + "@parcel/transformer-inline-string": "2.8.2", "@types/node": "^18.15.11", "@types/react": "^18.0.26", "@types/react-dom": "^18.0.10", @@ -29,7 +30,9 @@ "@emotion/react": "^11.10.5", "@emotion/styled": "^11.10.5", "@fontsource/roboto": "^4.5.8", + "@mui/icons-material": "^5.11.16", "@mui/material": "^5.11.4", + "markdown-to-jsx": "^7.2.0", "react": "^18.2.0", "react-dom": "^18.2.0", "react-router-dom": "^6.10.0" diff --git a/frontend/src/components/adf-details.tsx b/frontend/src/components/adf-details.tsx index f540cca..18659e8 100644 --- a/frontend/src/components/adf-details.tsx +++ b/frontend/src/components/adf-details.tsx @@ -3,11 +3,15 @@ import React, { } from 'react'; import { useParams, useNavigate } from 'react-router-dom'; import { + Accordion, + AccordionDetails, + AccordionSummary, Alert, AlertColor, Button, Chip, Container, + Grid, Paper, Pagination, Skeleton, @@ -18,6 +22,11 @@ import { Typography, } 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 LoadingContext from './loading-context'; import SnackbarContext from './snackbar-context'; @@ -218,6 +227,27 @@ function AdfDetails() { ADF-BDD.DEV + + + }> + What can I do with the ADF now? + + + + + {DetailInfoMd} + + + Example BDD + + + + + {problem ? ( <> diff --git a/frontend/src/components/adf-new-form.tsx b/frontend/src/components/adf-new-form.tsx index e254bd1..af2841c 100644 --- a/frontend/src/components/adf-new-form.tsx +++ b/frontend/src/components/adf-new-form.tsx @@ -122,7 +122,7 @@ function AdfNewForm({ fetchProblems }: { fetchProblems: () => void; }) { For more info on the syntax, have a look {' '} - here + here . )} diff --git a/frontend/src/components/adf-overview.tsx b/frontend/src/components/adf-overview.tsx index 3b5f813..d7f3a8a 100644 --- a/frontend/src/components/adf-overview.tsx +++ b/frontend/src/components/adf-overview.tsx @@ -7,6 +7,9 @@ import { } from 'react-router-dom'; import { + Accordion, + AccordionDetails, + AccordionSummary, Chip, Container, Paper, @@ -19,6 +22,11 @@ import { Typography, } 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 { @@ -102,6 +110,16 @@ function AdfOverview() { ADF-BDD.DEV + + + }> + What is this webapp doing and how should I use it? + + + {AddInfoMd} + + + {problems.length > 0 && ( diff --git a/frontend/src/components/graph-g6.tsx b/frontend/src/components/graph-g6.tsx index 6c4b9b8..4551f78 100644 --- a/frontend/src/components/graph-g6.tsx +++ b/frontend/src/components/graph-g6.tsx @@ -367,6 +367,12 @@ function GraphG6(props: Props) { hi edge (condition is true) {' '} Click nodes to hightlight paths! (You can also drag and zoom.) +
+ The + {' '} + Root for: X + {' '} + labels indicate where to start looking to determine the truth value of statement X. ); diff --git a/frontend/src/components/markdown.tsx b/frontend/src/components/markdown.tsx new file mode 100644 index 0000000..3c26603 --- /dev/null +++ b/frontend/src/components/markdown.tsx @@ -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 + + ), + }, + li: { + component: (props: any) => ( + + {/* eslint-disable-next-line react/jsx-props-no-spreading */} + + + ), + }, + }, +}; + +export default function Markdown(props: any) { + // eslint-disable-next-line react/jsx-props-no-spreading + return ; +} diff --git a/frontend/src/help-texts/add-info.md b/frontend/src/help-texts/add-info.md new file mode 100644 index 0000000..3466016 --- /dev/null +++ b/frontend/src/help-texts/add-info.md @@ -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). diff --git a/frontend/src/help-texts/detail-info.md b/frontend/src/help-texts/detail-info.md new file mode 100644 index 0000000..2b87ab3 --- /dev/null +++ b/frontend/src/help-texts/detail-info.md @@ -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). + diff --git a/frontend/src/help-texts/example-bdd.png b/frontend/src/help-texts/example-bdd.png new file mode 100644 index 0000000..b09499e Binary files /dev/null and b/frontend/src/help-texts/example-bdd.png differ diff --git a/frontend/yarn.lock b/frontend/yarn.lock index b7063c0..daaf9d6 100644 --- a/frontend/yarn.lock +++ b/frontend/yarn.lock @@ -324,6 +324,13 @@ dependencies: 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": version "7.18.13" 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" 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": version "5.11.4" resolved "https://registry.yarnpkg.com/@mui/material/-/material-5.11.4.tgz#4dda0f993c9aa9678e1b9bce16adfe11e984dbd4" @@ -1139,6 +1153,13 @@ "@parcel/workers" "2.8.2" 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": version "2.8.2" 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: 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: version "2.0.14" resolved "https://registry.yarnpkg.com/mdn-data/-/mdn-data-2.0.14.tgz#7113fc4281917d63ce29b43446f701e68c25ba50"