mirror of
https://github.com/ellmau/adf-obdd.git
synced 2025-12-20 09:39:38 +01:00
Support more options and multiple models
This commit is contained in:
monsterkrampe
parent
3f3659a98f
commit
783cdec878
@ -2,7 +2,21 @@ import * as React from 'react';
|
||||
|
||||
import { ThemeProvider, createTheme } from '@mui/material/styles';
|
||||
import {
|
||||
Backdrop, Button, CircularProgress, CssBaseline, Container, Link, Paper, Typography, TextField,
|
||||
Backdrop,
|
||||
Button,
|
||||
CircularProgress,
|
||||
CssBaseline,
|
||||
Container,
|
||||
FormControl,
|
||||
FormControlLabel,
|
||||
FormLabel,
|
||||
Link,
|
||||
Pagination,
|
||||
Paper,
|
||||
Radio,
|
||||
RadioGroup,
|
||||
Typography,
|
||||
TextField,
|
||||
} from '@mui/material';
|
||||
|
||||
import Graph from './graph.tsx';
|
||||
@ -35,18 +49,27 @@ ac(10,and(neg(2),6)).
|
||||
ac(1,and(neg(7),2)).
|
||||
ac(6,neg(7)).ac(2,and(neg(9),neg(6))).`;
|
||||
|
||||
enum Parsing {
|
||||
Naive = 'Naive',
|
||||
Hybrid = 'Hybrid',
|
||||
}
|
||||
|
||||
enum Strategy {
|
||||
ParseOnly = 'ParseOnly',
|
||||
Ground = 'Ground',
|
||||
FirstComplete = 'FirstComplete',
|
||||
FirstStable = 'FirstStable',
|
||||
FirstStableNogood = 'FirstStableNogood',
|
||||
Complete = 'Complete',
|
||||
Stable = 'Stable',
|
||||
StableCountingA = 'StableCountingA',
|
||||
StableCountingB = 'StableCountingB',
|
||||
StableNogood = 'StableNogood',
|
||||
}
|
||||
|
||||
function App() {
|
||||
const [loading, setLoading] = useState(false);
|
||||
const [code, setCode] = useState(placeholder);
|
||||
const [graph, setGraph] = useState();
|
||||
const [parsing, setParsing] = useState(Parsing.Naive);
|
||||
const [graphs, setGraphs] = useState();
|
||||
const [graphIndex, setGraphIndex] = useState(0);
|
||||
|
||||
const submitHandler = useCallback(
|
||||
(strategy: Strategy) => {
|
||||
@ -57,18 +80,19 @@ function App() {
|
||||
headers: {
|
||||
'Content-Type': 'application/json',
|
||||
},
|
||||
body: JSON.stringify({ code, strategy }),
|
||||
body: JSON.stringify({ code, strategy, parsing }),
|
||||
})
|
||||
.then((res) => res.json())
|
||||
.then((data) => setGraph(data))
|
||||
.then((data) => {
|
||||
setGraphs(data);
|
||||
setGraphIndex(0);
|
||||
})
|
||||
.finally(() => setLoading(false));
|
||||
// TODO: error handling
|
||||
},
|
||||
[code],
|
||||
[code, parsing],
|
||||
);
|
||||
|
||||
console.log(graph);
|
||||
|
||||
return (
|
||||
<ThemeProvider theme={darkTheme}>
|
||||
<CssBaseline />
|
||||
@ -97,24 +121,56 @@ function App() {
|
||||
onChange={(event) => { setCode(event.target.value); }}
|
||||
/>
|
||||
</Container>
|
||||
<Container>
|
||||
<Container sx={{ marginTop: 2, marginBottom: 2 }}>
|
||||
<FormControl>
|
||||
<FormLabel id="parsing-radio-group">Parsing Strategy</FormLabel>
|
||||
<RadioGroup
|
||||
row
|
||||
aria-labelledby="parsing-radio-group"
|
||||
name="parsing"
|
||||
value={parsing}
|
||||
onChange={(e) => setParsing((e.target as HTMLInputElement).value)}
|
||||
>
|
||||
<FormControlLabel value={Parsing.Naive} control={<Radio />} label="Naive" />
|
||||
<FormControlLabel value={Parsing.Hybrid} control={<Radio />} label="Hybrid" />
|
||||
</RadioGroup>
|
||||
</FormControl>
|
||||
<br />
|
||||
<br />
|
||||
<Button variant="outlined" onClick={() => submitHandler(Strategy.ParseOnly)}>Parse only</Button>
|
||||
{' '}
|
||||
<Button variant="outlined" onClick={() => submitHandler(Strategy.Ground)}>Grounded Model</Button>
|
||||
{' '}
|
||||
<Button variant="outlined" onClick={() => submitHandler(Strategy.FirstComplete)}>(First) Complete Model</Button>
|
||||
<Button variant="outlined" onClick={() => submitHandler(Strategy.Complete)}>Complete Models</Button>
|
||||
{' '}
|
||||
<Button variant="outlined" onClick={() => submitHandler(Strategy.FirstStable)}>(First) Stable Model</Button>
|
||||
<Button variant="outlined" onClick={() => submitHandler(Strategy.Stable)}>Stable Models (naive heuristics)</Button>
|
||||
{' '}
|
||||
<Button variant="outlined" onClick={() => submitHandler(Strategy.FirstStableNogood)}>(First) Stable Model using nogoods</Button>
|
||||
<Button disabled={parsing !== Parsing.Hybrid} variant="outlined" onClick={() => submitHandler(Strategy.StableCountingA)}>Stable Models (counting heuristic A)</Button>
|
||||
{' '}
|
||||
<Button disabled={parsing !== Parsing.Hybrid} variant="outlined" onClick={() => submitHandler(Strategy.StableCountingB)}>Stable Models (counting heuristic B)</Button>
|
||||
{' '}
|
||||
<Button variant="outlined" onClick={() => submitHandler(Strategy.StableNogood)}>Stable Models using nogoods (Simple Heuristic)</Button>
|
||||
</Container>
|
||||
|
||||
{graph
|
||||
{graphs
|
||||
&& (
|
||||
<Container>
|
||||
<Paper elevation={3} square sx={{ marginTop: 4, marginBottom: 4 }}>
|
||||
<Graph graph={graph} />
|
||||
</Paper>
|
||||
<Container sx={{ marginTop: 4, marginBottom: 4 }}>
|
||||
{graphs.length > 1
|
||||
&& (
|
||||
<>
|
||||
Models:
|
||||
<br />
|
||||
<Pagination variant="outlined" shape="rounded" count={graphs.length} page={graphIndex + 1} onChange={(e, value) => setGraphIndex(value - 1)} />
|
||||
</>
|
||||
)}
|
||||
{graphs.length > 0
|
||||
&& (
|
||||
<Paper elevation={3} square sx={{ marginTop: 4, marginBottom: 4 }}>
|
||||
<Graph graph={graphs[graphIndex]} />
|
||||
</Paper>
|
||||
)}
|
||||
{graphs.length === 0
|
||||
&& <>No models!</>}
|
||||
</Container>
|
||||
)}
|
||||
</main>
|
||||
|
||||
@ -4,8 +4,6 @@ import G6 from '@antv/g6';
|
||||
|
||||
G6.registerNode('nodeWithFlag', {
|
||||
draw(cfg, group) {
|
||||
console.log('cfg', cfg);
|
||||
|
||||
const mainWidth = Math.max(30, 5 * cfg.mainLabel.length + 10);
|
||||
const mainHeight = 30;
|
||||
|
||||
@ -14,10 +12,9 @@ G6.registerNode('nodeWithFlag', {
|
||||
width: mainWidth,
|
||||
height: mainHeight,
|
||||
radius: 2,
|
||||
fill: cfg.fill || 'white',
|
||||
fill: 'white',
|
||||
stroke: 'black',
|
||||
lineWidth: cfg.lineWidth,
|
||||
opacity: cfg.opacity,
|
||||
cursor: 'pointer',
|
||||
},
|
||||
name: 'rectMainLabel',
|
||||
draggable: true,
|
||||
@ -32,6 +29,7 @@ G6.registerNode('nodeWithFlag', {
|
||||
text: cfg.mainLabel,
|
||||
fill: '#212121',
|
||||
fontFamily: 'Roboto',
|
||||
cursor: 'pointer',
|
||||
},
|
||||
// must be assigned in G6 3.3 and later versions. it can be any value you want
|
||||
name: 'textMailLabel',
|
||||
@ -55,7 +53,7 @@ G6.registerNode('nodeWithFlag', {
|
||||
radius: 1,
|
||||
fill: '#4caf50',
|
||||
stroke: '#1b5e20',
|
||||
opacity: cfg.opacity,
|
||||
cursor: 'pointer',
|
||||
},
|
||||
name: 'rectMainLabel',
|
||||
draggable: true,
|
||||
@ -71,6 +69,7 @@ G6.registerNode('nodeWithFlag', {
|
||||
fill: '#212121',
|
||||
fontFamily: 'Roboto',
|
||||
fontSize: 10,
|
||||
cursor: 'pointer',
|
||||
},
|
||||
// must be assigned in G6 3.3 and later versions. it can be any value you want
|
||||
name: 'textMailLabel',
|
||||
@ -97,29 +96,36 @@ G6.registerNode('nodeWithFlag', {
|
||||
// },
|
||||
setState(name, value, item) {
|
||||
const group = item.getContainer();
|
||||
const shape = group.get('children')[0]; // Find the first graphics shape of the node. It is determined by the order of being added
|
||||
const mainShape = group.get('children')[0]; // Find the first graphics shape of the node. It is determined by the order of being added
|
||||
const subShape = group.get('children')[2];
|
||||
|
||||
if (name === 'hover') {
|
||||
if (value) {
|
||||
shape.attr('fill', 'lightsteelblue');
|
||||
mainShape.attr('fill', 'lightsteelblue');
|
||||
} else {
|
||||
shape.attr('fill', 'white');
|
||||
mainShape.attr('fill', 'white');
|
||||
}
|
||||
}
|
||||
|
||||
if (name === 'highlight') {
|
||||
if (value) {
|
||||
shape.attr('lineWidth', 3);
|
||||
mainShape.attr('lineWidth', 3);
|
||||
} else {
|
||||
shape.attr('lineWidth', 1);
|
||||
mainShape.attr('lineWidth', 1);
|
||||
}
|
||||
}
|
||||
|
||||
if (name === 'lowlight') {
|
||||
if (value) {
|
||||
shape.attr('opacity', 0.3);
|
||||
mainShape.attr('opacity', 0.3);
|
||||
if (subShape) {
|
||||
subShape.attr('opacity', 0.3);
|
||||
}
|
||||
} else {
|
||||
shape.attr('opacity', 1);
|
||||
mainShape.attr('opacity', 1);
|
||||
if (subShape) {
|
||||
subShape.attr('opacity', 1);
|
||||
}
|
||||
}
|
||||
}
|
||||
},
|
||||
@ -282,9 +288,6 @@ function Graph(props: Props) {
|
||||
.map(([source, target]) => `HI_${source}_${target}`),
|
||||
);
|
||||
|
||||
console.log(relevantNodeIds);
|
||||
console.log(relevantEdgeIds);
|
||||
|
||||
relevantNodeIds
|
||||
.forEach((id) => {
|
||||
graph.setItemState(id, 'lowlight', false);
|
||||
@ -347,8 +350,8 @@ function Graph(props: Props) {
|
||||
return (
|
||||
<>
|
||||
<div ref={ref} style={{ overflow: 'hidden' }} />
|
||||
<div>
|
||||
<span style={{ color: '#ed6c02' }}>lo edge (condition is false)</span>
|
||||
<div style={{ padding: 4 }}>
|
||||
<span style={{ color: '#ed6c02', marginRight: 8 }}>lo edge (condition is false)</span>
|
||||
{' '}
|
||||
<span style={{ color: '#1976d2' }}>hi edge (condition is true)</span>
|
||||
</div>
|
||||
|
||||
@ -8,20 +8,30 @@ use actix_cors::Cors;
|
||||
use actix_web::http;
|
||||
|
||||
use adf_bdd::adf::{Adf, DoubleLabeledGraph};
|
||||
use adf_bdd::adfbiodivine::Adf as BdAdf;
|
||||
use adf_bdd::parser::AdfParser;
|
||||
|
||||
#[derive(Deserialize)]
|
||||
enum Parsing {
|
||||
Naive,
|
||||
Hybrid,
|
||||
}
|
||||
|
||||
#[derive(Deserialize)]
|
||||
enum Strategy {
|
||||
ParseOnly,
|
||||
Ground,
|
||||
FirstComplete,
|
||||
FirstStable,
|
||||
FirstStableNogood,
|
||||
Complete,
|
||||
Stable,
|
||||
StableCountingA,
|
||||
StableCountingB,
|
||||
StableNogood,
|
||||
}
|
||||
|
||||
#[derive(Deserialize)]
|
||||
struct SolveReqBody {
|
||||
code: String,
|
||||
parsing: Parsing,
|
||||
strategy: Strategy,
|
||||
}
|
||||
|
||||
@ -33,6 +43,7 @@ struct SolveResBody {
|
||||
#[post("/solve")]
|
||||
async fn solve(req_body: web::Json<SolveReqBody>) -> impl Responder {
|
||||
let input = &req_body.code;
|
||||
let parsing = &req_body.parsing;
|
||||
let strategy = &req_body.strategy;
|
||||
|
||||
let parser = AdfParser::default();
|
||||
@ -43,29 +54,41 @@ async fn solve(req_body: web::Json<SolveReqBody>) -> impl Responder {
|
||||
panic!("Parsing failed, see log for further details")
|
||||
}
|
||||
}
|
||||
log::info!("[Done] parsing");
|
||||
|
||||
let mut adf = Adf::from_parser(&parser);
|
||||
let mut adf = match parsing {
|
||||
Parsing::Naive => Adf::from_parser(&parser),
|
||||
Parsing::Hybrid => {
|
||||
let bd_adf = BdAdf::from_parser(&parser);
|
||||
log::info!("[Start] translate into naive representation");
|
||||
let naive_adf = bd_adf.hybrid_step();
|
||||
log::info!("[Done] translate into naive representation");
|
||||
|
||||
naive_adf
|
||||
}
|
||||
};
|
||||
|
||||
log::debug!("{:?}", adf);
|
||||
|
||||
let ac = match strategy {
|
||||
Strategy::ParseOnly => None,
|
||||
Strategy::Ground => Some(adf.grounded()),
|
||||
// TODO: error handling if no such model exists!
|
||||
Strategy::FirstComplete => Some(adf.complete().next().unwrap()),
|
||||
// TODO: error handling if no such model exists!
|
||||
Strategy::FirstStable => Some(adf.stable().next().unwrap()),
|
||||
// TODO: error handling if no such model exists!
|
||||
let acs = match strategy {
|
||||
Strategy::ParseOnly => vec![None],
|
||||
Strategy::Ground => vec![Some(adf.grounded())],
|
||||
Strategy::Complete => adf.complete().map(Some).collect(),
|
||||
Strategy::Stable => adf.stable().map(Some).collect(),
|
||||
// TODO: INPUT VALIDATION: only allow this for hybrid parsing
|
||||
Strategy::StableCountingA => adf.stable_count_optimisation_heu_a().map(Some).collect(),
|
||||
// TODO: INPUT VALIDATION: only allow this for hybrid parsing
|
||||
Strategy::StableCountingB => adf.stable_count_optimisation_heu_b().map(Some).collect(),
|
||||
// TODO: support more than just default heuristics
|
||||
Strategy::FirstStableNogood => Some(
|
||||
adf.stable_nogood(adf_bdd::adf::heuristics::Heuristic::default())
|
||||
.next()
|
||||
.unwrap(),
|
||||
),
|
||||
Strategy::StableNogood => adf
|
||||
.stable_nogood(adf_bdd::adf::heuristics::Heuristic::default())
|
||||
.map(Some)
|
||||
.collect(),
|
||||
};
|
||||
|
||||
let dto = adf.into_double_labeled_graph(ac.as_ref());
|
||||
let dto: Vec<DoubleLabeledGraph> = acs
|
||||
.iter()
|
||||
.map(|ac| adf.into_double_labeled_graph(ac.as_ref()))
|
||||
.collect();
|
||||
|
||||
web::Json(dto)
|
||||
}
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user