From e2db3be6cdb8307ee4e7f00701a182d521430f87 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sun, 2 Feb 2025 12:22:22 -0800 Subject: [PATCH 1/3] Initial version. Refs #4. This commit introduces an initial version of the copilot-visualizer library that provides both static and dynamic generation features. Co-authored-by: Frank Dedden Co-authored-by: Ryan Scott Co-authored-by: Kyle Beechly --- .gitignore | 25 ++ CHANGELOG | 0 LICENSE | 29 ++ README.md | 34 ++ Setup.hs | 2 + copilot-visualizer.cabal | 130 +++++++ data/static_html/index.html | 255 ++++++++++++++ data/tikz/tikz.tex | 37 ++ examples/gui/Main.hs | 20 ++ examples/gui/copilot.css | 50 +++ examples/gui/copilot.js | 489 ++++++++++++++++++++++++++ examples/gui/main.html | 67 ++++ examples/tikz/Heater.hs | 37 ++ src/Copilot/Visualize/Dynamic.hs | 253 +++++++++++++ src/Copilot/Visualize/Live.hs | 162 +++++++++ src/Copilot/Visualize/Static.hs | 36 ++ src/Copilot/Visualize/TypedTrace.hs | 158 +++++++++ src/Copilot/Visualize/UntypedTrace.hs | 176 +++++++++ 18 files changed, 1960 insertions(+) create mode 100644 .gitignore create mode 100644 CHANGELOG create mode 100644 LICENSE create mode 100644 README.md create mode 100644 Setup.hs create mode 100644 copilot-visualizer.cabal create mode 100644 data/static_html/index.html create mode 100644 data/tikz/tikz.tex create mode 100644 examples/gui/Main.hs create mode 100644 examples/gui/copilot.css create mode 100644 examples/gui/copilot.js create mode 100644 examples/gui/main.html create mode 100644 examples/tikz/Heater.hs create mode 100644 src/Copilot/Visualize/Dynamic.hs create mode 100644 src/Copilot/Visualize/Live.hs create mode 100644 src/Copilot/Visualize/Static.hs create mode 100644 src/Copilot/Visualize/TypedTrace.hs create mode 100644 src/Copilot/Visualize/UntypedTrace.hs diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..f94ebc4 --- /dev/null +++ b/.gitignore @@ -0,0 +1,25 @@ +dist +dist-* +cabal-dev +*.o +*.hi +*.chi +*.chs.h +*.dyn_o +*.dyn_hi +.hpc +.hsenv +.cabal-sandbox/ +cabal.sandbox.config +*.prof +*.aux +*.hp +*.eventlog +.stack-work/ +cabal.project.local +cabal.project.local~ +.HTF/ +.ghc.environment.* +copilot-profiling +.DS_Store +.log diff --git a/CHANGELOG b/CHANGELOG new file mode 100644 index 0000000..e69de29 diff --git a/LICENSE b/LICENSE new file mode 100644 index 0000000..d3c9e46 --- /dev/null +++ b/LICENSE @@ -0,0 +1,29 @@ +2024-2025 (c) NASA +BSD3 License terms + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions +are met: + +Redistributions of source code must retain the above copyright +notice, this list of conditions and the following disclaimer. + +Redistributions in binary form must reproduce the above copyright +notice, this list of conditions and the following disclaimer in the +documentation and/or other materials provided with the distribution. + +Neither the name of the developers nor the names of its contributors +may be used to endorse or promote products derived from this software +without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR +CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. diff --git a/README.md b/README.md new file mode 100644 index 0000000..f4a93c4 --- /dev/null +++ b/README.md @@ -0,0 +1,34 @@ +[![Build Status](https://travis-ci.com/Copilot-Language/copilot.svg?branch=master)](https://app.travis-ci.com/github/Copilot-Language/copilot) + +# Copilot: a stream DSL + +The visualizer, which draws Copilot specifications using different graphical +formats. + +Copilot is a runtime verification framework written in Haskell. It allows the +user to write programs in a simple but powerful way using a stream-based +approach. + +Programs can be interpreted for testing (with the library copilot-interpreter), +or translated C99 code to be incorporated in a project, or as a standalone +application. The C99 backend ensures us that the output is constant in memory +and time, making it suitable for systems with hard realtime requirements. + +## Installation + +Copilot-visualizer can be found on +[Hackage](https://hackage.haskell.org/package/copilot-interpreter). It is +typically only installed as part of the complete Copilot distribution. For +installation instructions, please refer to the [Copilot +website](https://copilot-language.github.io). + +## Further information + +For further information, install instructions and documentation, please visit +the Copilot website: +[https://copilot-language.github.io](https://copilot-language.github.io) + +## License + +Copilot is distributed under the BSD-3-Clause license, which can be found +[here](https://raw.githubusercontent.com/Copilot-Language/copilot/master/copilot-interpreter/LICENSE). diff --git a/Setup.hs b/Setup.hs new file mode 100644 index 0000000..9a994af --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/copilot-visualizer.cabal b/copilot-visualizer.cabal new file mode 100644 index 0000000..e57efd7 --- /dev/null +++ b/copilot-visualizer.cabal @@ -0,0 +1,130 @@ +cabal-version: >= 1.10 +name: copilot-visualizer +version: 4.4 +synopsis: Visualizer for Copilot. +description: + Visualizer for Copilot. + . + Copilot is a stream (i.e., infinite lists) domain-specific language (DSL) in + Haskell that compiles into embedded C. Copilot contains an interpreter, + multiple back-end compilers, and other verification tools. + . + A tutorial, examples, and other information are available at + . + +author: Ivan Perez, Frank Dedden, Ryan Scott, Kyle Beechly +license: BSD3 +license-file: LICENSE +maintainer: Ivan Perez +homepage: https://copilot-language.github.io +bug-reports: https://github.com/Copilot-Language/copilot/issues +stability: Experimental +category: Language, Embedded +build-type: Simple +extra-source-files: README.md + CHANGELOG + examples/gui/Main.hs + examples/gui/main.html + examples/gui/copilot.css + examples/gui/copilot.js + examples/tikz/Heater.hs + +data-files: data/tikz/tikz.tex + data/static_html/index.html + +x-curation: uncurated + +source-repository head + type: git + location: https://github.com/Copilot-Language/copilot.git + subdir: copilot-visualizer + +flag examples + description: Enable examples + default: False + manual: True + +library + + default-language: + Haskell2010 + + hs-source-dirs: + src + + ghc-options: + -Wall + + build-depends: + base >= 4.9 && < 5, + aeson >= 2.0.0.0 && < 2.3, + filepath >= 1.4.2 && < 1.6, + hint >= 0.9.0 && < 1.10, + pretty >= 1.0 && < 1.2, + ogma-extra >= 1.6.0 && < 1.7, + text >= 1.2.3.1 && < 2.2, + websockets >= 0.12.7 && < 0.14, + + copilot >= 4.4 && < 4.5, + copilot-core >= 4.4 && < 4.5, + copilot-interpreter >= 4.4 && < 4.5, + copilot-language >= 4.4 && < 4.5 + + exposed-modules: + + Copilot.Visualize.Live + Copilot.Visualize.Static + + other-modules: + + Copilot.Visualize.Dynamic + Copilot.Visualize.TypedTrace + Copilot.Visualize.UntypedTrace + Paths_copilot_visualizer + +executable gui-example + main-is: + Main.hs + + default-language: + Haskell2010 + + hs-source-dirs: + examples/gui + + ghc-options: + -Wall + + build-depends: + base >= 4.9 && < 5, + + copilot-visualizer + + if flag(examples) + buildable: True + else + buildable: False + +executable tikz-example + main-is: + Heater.hs + + default-language: + Haskell2010 + + hs-source-dirs: + examples/tikz + + ghc-options: + -Wall + + build-depends: + base >= 4.9 && < 5, + + copilot >= 4.4 && < 4.5, + copilot-visualizer + + if flag(examples) + buildable: True + else + buildable: False diff --git a/data/static_html/index.html b/data/static_html/index.html new file mode 100644 index 0000000..2160ec8 --- /dev/null +++ b/data/static_html/index.html @@ -0,0 +1,255 @@ + + + + + + Copilot Visualizer + + + + + + + +
+ +
+ + + + diff --git a/data/tikz/tikz.tex b/data/tikz/tikz.tex new file mode 100644 index 0000000..b05f2c1 --- /dev/null +++ b/data/tikz/tikz.tex @@ -0,0 +1,37 @@ +{{=<% %>=}} +\documentclass{standalone} +\usepackage{tikz} +\usepackage{tikz-timing} +\usepackage{xcolor} +\definecolor{false}{HTML}{ECD9ED} +\definecolor{true}{HTML}{D9ECED} +\begin{document} +\newcommand{\true}{T} +\newcommand{\false}{F} +\tikzset{ +every picture/.style={ + execute at end picture={ + \path (current bounding box.south west) +(-1,-1) (current bounding box.north east) +(1,1); + } +} +} + +\tikzset{ +timing/.style={x=5ex,y=2ex}, +timing/rowdist=4ex, +timing/dslope=0.1, +x=5ex, +timing/coldist=1ex, +timing/name/.style={font=\sffamily\scriptsize}, +timing/d/text/.style={font=\sffamily\tiny}, +} +\begin{tikztimingtable} +<%#adTraceElems%> +<%teName%> & g<%#teValues%><%#tvIsEmpty%>S<%/tvIsEmpty%><%^tvIsEmpty%><%#teIsBoolean%>[fill=<%tvValue%>]D{\<%tvValue%>}<%/teIsBoolean%><%^teIsBoolean%>D{<%tvValue%>}<%/teIsBoolean%><%/tvIsEmpty%><%/teValues%>\\ +<%/adTraceElems%> +\extracode +\begin{background}[shift={(0.05,0)},help lines] +\vertlines[help lines,opacity=0.3]{-0.3ex,...,<%adLastSample%>} +\end{background} +\end{tikztimingtable} +\end{document} diff --git a/examples/gui/Main.hs b/examples/gui/Main.hs new file mode 100644 index 0000000..8b93b7c --- /dev/null +++ b/examples/gui/Main.hs @@ -0,0 +1,20 @@ +import Copilot.Visualize.Live + +main = visualize spec + +spec :: String +spec = unlines + [ "let temperature :: Stream Word8" + , " temperature = extern \"temperature\" (Just [0, 15, 20, 25, 30])" + , "" + , " ctemp :: Stream Float" + , " ctemp = (unsafeCast temperature) * (150.0 / 255.0) - 50.0" + , "" + , " trueFalse :: Stream Bool" + , " trueFalse = [True] ++ not trueFalse" + , "" + , "in do trigger \"heaton\" (temperature < 18) [arg ctemp, arg (constI16 1), arg trueFalse]" + , " trigger \"heatoff\" (temperature > 21) [arg (constI16 1), arg ctemp]" + , " observer \"temperature\" temperature" + , " observer \"temperature2\" (temperature + 1)" + ] diff --git a/examples/gui/copilot.css b/examples/gui/copilot.css new file mode 100644 index 0000000..82a1a0a --- /dev/null +++ b/examples/gui/copilot.css @@ -0,0 +1,50 @@ +/* Timeline */ +/* Timeline decoration: Grid */ +.axis path, +.axis line { + fill: none; + stroke: #000; + shape-rendering: crispEdges; +} +.grid-line { + stroke: #ccc; + stroke-width: 1; + stroke-dasharray: 3,3; +} + +/* Timeline decoration: Labels */ +.label { + font-size: 12px; +} +.time-label { + font-family: sans-serif; + font-size: 12px; + fill: black; +} +.value-text { + font-size: 10px; + text-anchor: middle; + dominant-baseline: middle; +} + +/* Timeline decoration: Values */ +.hexagon { + stroke: black; + stroke-width: 1px; + color: green; +} +.bool-background { + opacity: 0.3; +} + +/* Toolbar buttons */ +button { + width: 100px !important; + height: 48px !important; + border-radius: 24px !important; + background-color: #f1316b !important; + color: #fff !important; + margin-top: 45px !important; + border:none !important; + font-size: 12px !important; +} diff --git a/examples/gui/copilot.js b/examples/gui/copilot.js new file mode 100644 index 0000000..943e3c7 --- /dev/null +++ b/examples/gui/copilot.js @@ -0,0 +1,489 @@ +/* Constants */ + +/* Timeline dimensions */ +const margin = {top: 20, right: 20, bottom: 30, left: 90}; +const width = 960 - margin.left - margin.right; +const height = 200 - margin.top - margin.bottom; +const rowHeight = 40; + +/** + * Position of the stream labels wrt. to the left side of the timeline. + */ +const labelPosX = -90; + +/* Timeline colors */ + +/* Default colors for true and false (just dim green and red). */ +const booleanColorDefaultTrue = "#90EE90"; +const booleanColorDefaultFalse = "#FFB6C1"; + +/* + * Alternative colors for true and false, making colored backgrounds more + * easily distinguishable in conditions with reduced color. Specifically: + * + * - Increase blue content in the 'false' color to increase distinction from + * the 'true' color in protanopic (no red) and deuteranopic (no green). + * + * - Decrease red content in the 'false' color to increase distinction from the + * 'true' color in achromatopsic (no color) conditions. + * + * This does not meaningfully address visibility considerations in reduced + * contrast or blurry conditions. + */ +const booleanColorHighContrastTrue = "#90EE90"; +const booleanColorHighContrastFalse = "#E1B6ED"; + +/* Timeline state */ +let svg; +let data = { adLastSample: 0, adTraceElems: [] }; +let xScale; +let numRows = 0; +let numSteps = 2; +let booleanColorTrue = booleanColorDefaultTrue; +let booleanColorFalse = booleanColorDefaultFalse; + +/** + * Process numeric data, adding duration and y-positions to each trace element. + */ +function processNumericData(data) +{ + // Calculate bounds of stream. + const maxValue = Math.max(...data.map(d => d.tvValue)); + const minValue = Math.min(...data.map(d => d.tvValue)); + + // Vertical scale of the stream. + const yScale = d3.scaleLinear() + .domain([minValue, maxValue]) + .range([rowHeight * 0.8, rowHeight * 0.2]); + + // Return the data augmented with duration for each sample, and the vertical + // scale. + return data.map((d, i) => ({ + ...d, + duration: + i < data.length - 1 ? data[i + 1].time - d.time : numSteps + 1 - d.time, + y: yScale(d.tvValue) + })); +} + +/** + * Create timeline labels. + */ +function createLabels() +{ + document.querySelectorAll(".label").forEach(function(lst) { + lst.remove(); + }); + + // Add row labels. + const labels = data.adTraceElems.map((x) => x.teName); + svg.selectAll(".label") + .data(labels) + .enter() + .append("text") + .attr("class", "label") + .attr("x", labelPosX) + .attr("y", (d, i) => i * rowHeight + rowHeight/2) + .text(d => d); +} + +/** + * Draw numeric row with stretched hexagons. + */ +function drawNumericRow(data, rowIndex) +{ + const rowG = svg.append("g") + .attr("class", "value_list") + .attr("transform", `translate(0,${rowIndex * rowHeight})`); + + const hexHeight = rowHeight * 0.8; + + time = 0; + + // Create hexagon groups. + const hexGroups = rowG.selectAll("g") + .data(data) + .enter() + .append("g") + .attr("transform", d => `translate(${xScale(time++)},${rowHeight * 0.1})`); + + // Add hexagons. + hexGroups.append("path") + .attr("class", "hexagon") + .attr("d", d => hexagonPath(xScale(1) - xScale(0), hexHeight)) + .attr("fill", "#f7fbff"); + + // Add value text. + hexGroups.append("text") + .attr("class", "value-text") + .attr("x", d => (xScale(1) - xScale(0)) / 2) + .attr("y", hexHeight / 2) + .text(d => d.tvValue); +} + +/** + * Draw boolean rows with colored backgrounds. + */ +function drawBooleanRow(data, rowIndex) +{ + const rowG = svg.append("g") + .attr("class", "value_list") + .attr("transform", `translate(0,${rowIndex * rowHeight})`); + + time = 0; + + // Draw colored backgrounds. + rowG.selectAll("rect") + .data(data) + .enter() + .append("rect") + .attr("class", "bool-background") + .attr("x", d => xScale(time++)) + .attr("y", 0) + .attr("width", d => xScale(1) - xScale(0)) + .attr("height", rowHeight) + .attr("fill", d => d.tvValue == "true" ? booleanColorTrue : booleanColorFalse); +} + +/** + * Re-draw complete timeline. + */ +function redraw() +{ + document.querySelectorAll(".value_list").forEach(function(lst) { + lst.remove(); + }); + + // Draw all rows. + i = 0; + data.adTraceElems.forEach(function(traceElem) { + if (traceElem.teIsBoolean) + { + drawBooleanRow(traceElem.teValues, i); + } + else + { + drawNumericRow(processNumericData(traceElem.teValues), i); + } + i++; + }); +} + +/** + * Create SVG for the timeline. + */ +function createSVG() +{ + // Clear all existing elements. + if (typeof svg !== 'undefined' ) { svg.selectAll("*").remove(); } + + // Calculate number of rows and columns (steps) from available data. + numRows = data.adTraceElems.length; + numSteps = data.adLastSample; + + // Create SVG. + svg = d3.select("#timeline") + .attr("width", width + margin.left + margin.right) + .attr("height", (rowHeight * numRows) + margin.top + margin.bottom) + .append("g") + .attr("transform", `translate(${margin.left},${margin.top})`); + + // Create scales. + xScale = d3.scaleLinear() + .domain([0, numSteps + 1]) + .range([0, width]); + + // Create x-axis with ticks at integer positions. + const xAxis = d3.axisBottom(xScale) + .tickValues(Array.from({length: 11}, (_, i) => i)) + .tickFormat(''); + + createLabels(); + redraw(); + + // Add the axis. + const axisGroup = svg.append("g") + .attr("class", "axis") + .attr("transform", `translate(0,${rowHeight * numRows})`) + .call(xAxis); + + // After creating the axis and labels, add vertical grid lines. + // + // Use light gray as color, a dotted line, start from the top (negative + // because we are going up from the axis), and end at the axis. + const gridLines = axisGroup.selectAll(".grid-line") + .data(Array.from({length: 11}, (_, i) => i)) + .enter() + .append("line") + .attr("class", "grid-line") + .attr("x1", d => xScale(d)) + .attr("x2", d => xScale(d)) + .attr("y1", -rowHeight * (numRows + 1)) + .attr("y2", 0) + .style("stroke", "#ccc") + .style("stroke-width", "1") + .style("stroke-dasharray", "3,3"); + + // Add offset labels. + const timeLabels = axisGroup.selectAll(".time-label") + .data(Array.from({length: numRows + 1}, (_, i) => i)) + .enter() + .append("text") + .attr("class", "time-label") + .attr("x", d => xScale(d + 0.5)) + .attr("y", 25) + .attr("text-anchor", "middle") + .text(d => d + ""); + + // Detect clicks on timeline. + svg.on("click", function(event) { + const mouseX = d3.pointer(event)[0]; + const time = Math.floor(xScale.invert(mouseX).toFixed(2)); + const row = Math.floor((event.offsetY - margin.top) / rowHeight); + const label = data.adTraceElems[row].teName; + + console.log("Label:", label , "Time:", time); + ws.send('(Up ' + time + ', "' + label + '")'); + }); + + // Detect mouse wheel on timeline. + svg.on("wheel", function(event) { + // Prevent default scroll behavior. + event.preventDefault(); + + const mouseX = d3.pointer(event)[0]; + const time = Math.floor(xScale.invert(mouseX).toFixed(2)); + const row = Math.floor((event.offsetY - margin.top) / rowHeight); + const label = data.adTraceElems[row].teName; + const dir = event.deltaY < 0 ? 'Up' : 'Down'; + + ws.send('(' + dir + ' ' + time + ', "' + label + '")'); + + console.log ( "Label:", label, "Time:", time, "Direction:", dir); + }); +} + +/** + * Add a step to the simulation. + */ +function stepUp() +{ + ws.send('(StepUp, "")'); +} + +/** + * Reduce the number of steps of the simulation. + */ +function stepDown() +{ + ws.send('(StepDown, "")'); +} + +/** + * Open a dialog requesting information to add a new stream to the simulation. + */ +function addStream() +{ + const popup = document.getElementById("popup"); + popup.classList.remove("hidden"); +} + +/** + * Cancel dialog requesting information to add a new stream to the simulation. + */ +function closePopup() +{ + const popup = document.getElementById("popup"); + popup.classList.add("hidden"); +} + +/** + * Add a new stream to the simulation. The definition provided must be correct + * in the context of the current simulation, and the name given to the new + * stream must be valid in Haskell, unique in the current context, and not + * clash with any existing names. + */ +function addStreamSubmit() +{ + const popup = document.getElementById("popup"); + const inputName = document.getElementById("inputName").value; + const inputExpr = document.getElementById("inputExpr").value; + ws.send('(AddStream "' + inputName + '" "(' + inputExpr + ')", "")'); + popup.classList.add("hidden"); +} + +/** + * Toggle the color scheme of the timeline. + */ +function toggleColors() +{ + const highContrastBtn = document.getElementById('high_contrast'); + if (highContrastBtn.checked) { + booleanColorTrue = booleanColorHighContrastTrue; + booleanColorFalse = booleanColorHighContrastFalse; + } else { + booleanColorTrue = booleanColorDefaultTrue; + booleanColorFalse = booleanColorDefaultFalse; + } + + createSVG(); +} + +/* Attach event handlers to UI elements */ + +// Somehow this does not work if we match the svg element directly, so we match +// the parent div. +document.getElementById("copyPNG").addEventListener("click", () => copyPNG("#timeline-parent")); + +document.getElementById("copySVG").addEventListener("click", () => copySVG("#timeline")); + +// Somehow this does not work if we match the svg element directly, so we match +// the parent div. +document.getElementById("downloadPNG").addEventListener("click", () => downloadPNG("#timeline-parent", "timeline")); + +document.getElementById("downloadSVG").addEventListener("click", () => downloadSVG("#timeline", "timeline")); + +document.getElementById("stepUp").addEventListener("click", stepUp); +document.getElementById("stepDown").addEventListener("click", stepDown); +document.getElementById("addStream").addEventListener("click", addStream); +document.getElementById("closePopup").addEventListener("click", closePopup); +document.getElementById("submitPopup").addEventListener("click", addStreamSubmit); + +// Adjust colors using high-contrast when applicable. +document.getElementById('high_contrast').addEventListener('change', toggleColors); + +createSVG(); + +// Communicate with the backend instance of Copilot via a websocket. +let ws = new WebSocket('ws://localhost:9160'); + +ws.onmessage = function(event) { + data = JSON.parse(event.data); + createSVG(); +}; + +ws.onclose = function() { + console.log('Disconnected from server'); +}; + +ws.onerror = function(error) { + console.log('Error: ' + error.message); +}; + +/* Auxiliary functions */ + +/** + * Create an hexagon path (used for cells or samples). + */ +function hexagonPath(width, height) +{ + return ` + M ${width-10},0 + L ${width},${height/2} + L ${width-10},${height} + L ${10},${height} + L ${0},${height/2} + L ${10},0 + Z + `; +} + +/** + * Download a file containing a given text. + */ +function download(filename, text) +{ + var element = document.createElement('a'); + element.setAttribute('href', 'data:text/plain;charset=utf-8,' + encodeURIComponent(text)); + element.setAttribute('download', filename); + + element.style.display = 'none'; + document.body.appendChild(element); + + element.click(); + + document.body.removeChild(element); +} + +/** + * Copy element as SVG to clipboard as SVG. + * + * @param {svg} queryString - Query string referring to an SVG element in the + * current document. + */ +function copySVG(queryString) +{ + const mySVG = document.querySelector(queryString); + const data = new XMLSerializer().serializeToString(mySVG); + + navigator.clipboard.writeText(data).then( + () => { + console.log("SVG copied to clipboard"); + }, + (err) => { + console.log("Failed to copy SVG to clipboard"); + } + ); +} + +/** + * Copy timeline to clipboard as PNG. + * + * @param {string} queryString - Query string referring to element in the + * current document. + */ +function copyPNG(queryString) +{ + const elem = document.querySelector(queryString); + html2canvas(elem).then(function(canvas) { + canvas.toBlob(function(blob) { + navigator.clipboard + .write([ + new ClipboardItem( + Object.defineProperty({}, blob.type, { + value: blob, + enumerable: true + }) + ) + ]).then(function() { + console.log("Copied to clipboard"); + }); + }); + }); +} + +/** + * Download screenshot of an element as a PNG file. + * + * @param {string} queryString - Query string referring to element in the + * current document. + * + * @param {string} defaultFilename - Default file name used in the save file + * dialog. + */ +function downloadPNG(queryString, defaultFilename) +{ + const mySVG = document.querySelector(queryString); + html2canvas(mySVG).then(function(canvas) { + var a = document.createElement('a'); + a.href = canvas.toDataURL(); + a.download = defaultFilename + ".png"; + a.click(); + }); +} + +/** + * Download screenshot of timeline as SVG file. + * + * @param {string} queryString - Query string referring to element in the + * current document. + * + * @param {string} defaultFilename - Default file name used in the save file + * dialog. + */ +function downloadSVG(queryString, defaultFilename) +{ + const mySVG = document.querySelector(queryString); + const data = new XMLSerializer().serializeToString(mySVG); + download(defaultFilename + ".svg", data); +} diff --git a/examples/gui/main.html b/examples/gui/main.html new file mode 100644 index 0000000..a2003d7 --- /dev/null +++ b/examples/gui/main.html @@ -0,0 +1,67 @@ + + + Copilot Visualizer + + + + + + + + + + + + + + +
+ +
+ + +
+ + + + + + + +
+ + +
+ +
+ + + + + + + + diff --git a/examples/tikz/Heater.hs b/examples/tikz/Heater.hs new file mode 100644 index 0000000..e36cde9 --- /dev/null +++ b/examples/tikz/Heater.hs @@ -0,0 +1,37 @@ +-- Copyright 2025 NASA +-- Copyright 2019 National Institute of Aerospace / Galois, Inc. + +-- This is a simple example with basic usage. It implements a simple home +-- heating system: It heats when temp gets too low, and stops when it is high +-- enough. It read temperature as a byte (range -50C to 100C) and translates +-- this to Celsius. + +module Main where + +import Language.Copilot +import Copilot.Visualize.Static + +import Prelude hiding ((>), (<)) + +-- External temperature as a byte, range of -50C to 100C +temp :: Stream Word8 +temp = extern "temperature" (Just [ 10, 15, 18, 19, 25, 5, 45 ]) + +-- Calculate temperature in Celsius. +-- We need to cast the Word8 to a Float. Note that it is an unsafeCast, as there +-- is no direct relation between Word8 and Float. +ctemp :: Stream Float +ctemp = (unsafeCast temp) * (150.0 / 255.0) - 50.0 + +spec = do + -- Triggers that fire when the ctemp is too low or too high, + -- pass the current ctemp as an argument. + trigger "heaton" (ctemp < 18.0) [arg ctemp] + trigger "heatoff" (ctemp > 21.0) [arg ctemp] + +-- Compile the spec and produce a LaTeX file in the current directory with a +-- Tikz drawing of the spec. +main :: IO () +main = do + spec' <- reify spec + visualize 3 spec' "tikz" "." diff --git a/src/Copilot/Visualize/Dynamic.hs b/src/Copilot/Visualize/Dynamic.hs new file mode 100644 index 0000000..26c535a --- /dev/null +++ b/src/Copilot/Visualize/Dynamic.hs @@ -0,0 +1,253 @@ +{-# LANGUAGE GADTs #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE ScopedTypeVariables #-} +-- | +-- Copyright : (c) NASA, 2024-2025 +-- License : BSD-style (see the LICENSE file in the distribution) +-- +-- Allow loading Copilot specifications from strings and modifying them live. +-- +-- An example of a spec that can be passed as argument to the live simulator +-- follows: +-- +-- @ +-- spec :: String +-- spec = unlines +-- [ "let temperature :: Stream Word8" +-- , " temperature = extern \"temperature\" (Just [0, 15, 20, 25, 30])" +-- , "" +-- , " ctemp :: Stream Float" +-- , " ctemp = (unsafeCast temperature) * (150.0 / 255.0) - 50.0" +-- , "" +-- , " trueFalse :: Stream Bool" +-- , " trueFalse = [True] ++ not trueFalse" +-- , "" +-- , "in do trigger \"heaton\" (temperature < 18) [arg ctemp, arg (constI16 1), arg trueFalse]" +-- , " trigger \"heatoff\" (temperature > 21) [arg (constI16 1), arg ctemp]" +-- , " observer \"temperature\" temperature" +-- , " observer \"temperature2\" (temperature + 1)" +-- ] +-- @ +-- +-- The imports are predefined. +module Copilot.Visualize.Dynamic + ( simInit + , simStep + , SimulationSettings(..) + , mkDefaultSimulationSettings + , SimData(..) + ) + where + +-- External imports +import qualified Language.Haskell.Interpreter as HI +import Prelude hiding (div, not, (++), (<), (>)) +import qualified Prelude + +-- External imports: Copilot +import qualified Copilot.Core as Core +import Copilot.Language hiding (interpret, typeOf) +import Language.Copilot hiding (interpret, typeOf) + +-- Internal imports +import Copilot.Visualize.TypedTrace + +-- | Simulation data. +data SimData = SimData + { simSteps :: Int -- ^ Number of steps to simulate. + , simSpec :: Core.Spec -- ^ Copilot spec to simulate. + , simString :: String -- ^ Textual representation of Copilot spec. + } + +-- | Initialize a simulation. +simInit :: SimulationSettings -> String -> IO SimData +simInit simulationSettings spec = do + -- Load the spec, and save it so that it doesn't need to be reloaded if it + -- doesn't change. + let numSteps = simulationSettingsInitialSteps simulationSettings + spec' <- readSpec simulationSettings spec + let simData = SimData numSteps spec' spec + return simData + +-- | Update the spec based on the input command received. +simStep :: SimulationSettings + -> SimData + -> (Command, String) + -> IO SimData +simStep _ simData (StepUp, _) = + pure simData { simSteps = simSteps simData + 1 } + +simStep _ simData (StepDown, _) = + pure simData { simSteps = simSteps simData + 1 } + +simStep simulationSettings simData (AddStream name expr, _) = do + let specN = concat [ simString simData, "\n", " ", completeExpr] + + completeExpr = concat [ "observer ", show name, " (", expr, ")" ] + + let trace = extractTrace $ simSpec simData + spec2 <- readSpec simulationSettings specN + let spec3 = updateWithTrace trace spec2 + + pure simData { simSpec = spec3, simString = specN } + +simStep simulationSettings simData (command, name) = do + spec' <- apply simulationSettings (simSpec simData) name command + pure simData { simSpec = spec' } + +-- | Settings used for a simulation. +data SimulationSettings = SimulationSettings + { simulationSettingsInitialSteps :: Int + , simulationSettingsImports :: [(String, Maybe String)] + } + +-- | Default settings that simulates 3 steps and provides default imports of +-- the main Copilot modules. +mkDefaultSimulationSettings :: SimulationSettings +mkDefaultSimulationSettings = + SimulationSettings + 3 + [ ("Control.Monad.Writer", Nothing) + , ("Copilot.Language", Nothing) + , ("Copilot.Language.Spec", Nothing) + , ("Data.Functor.Identity", Nothing) + , ("Language.Copilot", Nothing) + , ("Prelude", Just "P") + ] + +-- * Commands + +-- * Load specs from strings + +-- | Read a specification from a string and reify it. +readSpec :: SimulationSettings -> String -> IO Core.Spec +readSpec settings spec = do + r <- HI.runInterpreter (loadSpec settings spec) + case r of + Left err -> do putStrLn $ "Error: " Prelude.++ show err + error $ show err + Right s -> return s + +-- | Load a spec from a string, adding standard imports. +loadSpec :: SimulationSettings -> String -> HI.Interpreter Core.Spec +loadSpec settings spec = do + HI.setImportsQ (simulationSettingsImports settings) + spec' <- HI.interpret spec (HI.as :: Spec) + HI.liftIO $ reify spec' + +-- | Commands to apply to a running simulation. +data Command = StepUp + | StepDown + | Up Int + | Down Int + | AddStream String String + | Noop + deriving (Eq, Read, Show) + +-- | Apply a command to a simulation. +apply :: SimulationSettings -> Core.Spec -> String -> Command -> IO Core.Spec +apply settings spec _name (AddStream sName sExpr) = do + spec' <- addStream settings sName sExpr + -- TODO: I need to bring the streams from the other spec too, otherwise the + -- streams to include may refer to streams by ID that are in a different + -- scope. + let observers' = Core.specObservers spec' + observers = Core.specObservers spec + return $ spec { Core.specObservers = observers Prelude.++ observers' } + +apply _settings spec name command = pure $ spec + { Core.specStreams = + map (updateStream name command) (Core.specStreams spec) + , Core.specObservers = + map (updateObserver name command) (Core.specObservers spec) + , Core.specTriggers = + map (updateTrigger name command) (Core.specTriggers spec) + } + +-- | Apply a command to an observer. +updateObserver :: String -> Command -> Core.Observer -> Core.Observer +updateObserver name command (Core.Observer i e ty) = + Core.Observer i (updateExpr name command e) ty + +-- | Apply a command to a trigger. +updateTrigger :: String -> Command -> Core.Trigger -> Core.Trigger +updateTrigger name command (Core.Trigger i e es) = Core.Trigger i e' es' + where + e' = updateExpr name command e + es' = map (updateUExpr name command) es + +-- | Apply a command to a core expression. +updateExpr :: String -> Command -> Core.Expr a -> Core.Expr a +updateExpr name command expr = case expr of + Core.ExternVar ty nameE vs + | nameE Prelude.== name + -> Core.ExternVar ty nameE (updateValues vs ty command) + + | otherwise + -> expr + + Core.Op1 op expr1 -> + Core.Op1 op (updateExpr name command expr1) + + Core.Op2 op expr1 expr2 -> + Core.Op2 op (updateExpr name command expr1) (updateExpr name command expr2) + + Core.Op3 op expr1 expr2 expr3 -> + Core.Op3 + op + (updateExpr name command expr1) + (updateExpr name command expr2) + (updateExpr name command expr3) + + _ -> expr + +-- | Apply a command to an untyped expression that carries the information +-- about the type of the expression as a value (existential). +updateUExpr :: String -> Command -> Core.UExpr -> Core.UExpr +updateUExpr name cmd (Core.UExpr ty expr) = + Core.UExpr ty (updateExpr name cmd expr) + +-- | Apply a command to a stream. +updateStream :: String -> Command -> Core.Stream -> Core.Stream +updateStream name command (Core.Stream i buf expr ty) = + Core.Stream i buf (updateExpr name command expr) ty + +-- | Apply a command to a series of typed values, if any. +updateValues :: Maybe [a] -> Type a -> Command -> Maybe [a] +updateValues vsM ty command = + fmap (fmap (updateValue command ty) . zip [0..]) vsM + +-- | Apply a command to a typed value. +updateValue :: Command -> Type a -> (Int, a) -> a +updateValue (Up n) Core.Bool (ix, a) = + if n Prelude.== ix then Prelude.not a else a +updateValue (Down n) Core.Bool (ix, a) = + if n Prelude.== ix then Prelude.not a else a +updateValue (Up n) Core.Word8 (ix, a) = + if n Prelude.== ix then a + 1 else a +updateValue (Down n) Core.Word8 (ix, a) = + if n Prelude.== ix then a - 1 else a +updateValue _ _ (_, a) = a + +-- * Sample spec + +-- | Produce a specification from the expression for a stream. +addStream :: SimulationSettings -> String -> String -> IO Core.Spec +addStream settings name expr = do + r <- HI.runInterpreter (addStream' settings name expr) + case r of + Left err -> do putStrLn $ "Error: " Prelude.++ show err + error $ show err + Right spec -> return spec + +-- | Produce a specification from the expression for a stream, in an +-- interpreter context. +-- +-- Observe that Interpreter () is an alias for InterpreterT IO () +addStream' :: SimulationSettings -> String -> String -> HI.Interpreter Core.Spec +addStream' settings name expr = do + HI.setImportsQ (simulationSettingsImports settings) + let completeExpr = concat [ "observer ", show name, " (", expr, ")" ] + + spec <- HI.interpret completeExpr (HI.as :: Spec) + HI.liftIO $ reify spec diff --git a/src/Copilot/Visualize/Live.hs b/src/Copilot/Visualize/Live.hs new file mode 100644 index 0000000..973cd2f --- /dev/null +++ b/src/Copilot/Visualize/Live.hs @@ -0,0 +1,162 @@ +{-# LANGUAGE GADTs #-} +{-# LANGUAGE OverloadedStrings #-} +-- | +-- Copyright : (c) NASA, 2024-2025 +-- License : BSD-style (see the LICENSE file in the distribution) +-- +-- Run a Copilot simulation live and allow interacting with it using a +-- websocket. +-- +-- This visualizer enables adding new streams to a visualization. To do so, the +-- visualizer needs access to the original spec, and needs to be able to +-- interpret new expressions in the same context as the prior expressions. +-- +-- An example of a spec that can be passed as argument to the visualizer +-- follows: +-- +-- @ +-- spec :: String +-- spec = unlines +-- [ "let temperature :: Stream Word8" +-- , " temperature = extern \"temperature\" (Just [0, 15, 20, 25, 30])" +-- , "" +-- , " ctemp :: Stream Float" +-- , " ctemp = (unsafeCast temperature) * (150.0 / 255.0) - 50.0" +-- , "" +-- , " trueFalse :: Stream Bool" +-- , " trueFalse = [True] ++ not trueFalse" +-- , "" +-- , "in do trigger \"heaton\" (temperature < 18) [arg ctemp, arg (constI16 1), arg trueFalse]" +-- , " trigger \"heatoff\" (temperature > 21) [arg (constI16 1), arg ctemp]" +-- , " observer \"temperature\" temperature" +-- , " observer \"temperature2\" (temperature + 1)" +-- ] +-- @ +-- +-- The imports are predefined. +module Copilot.Visualize.Live + ( visualize + , visualizeWith + , VisualSettings(..) + , mkDefaultVisualSettings + , SimulationSettings(..) + , mkDefaultSimulationSettings + ) + where + +-- External imports +import Control.Exception (SomeException (..), handle) +import Data.Aeson (ToJSON (..), encode) +import qualified Data.Text as T +import qualified Network.WebSockets as WS +import Prelude hiding (div, not, (++), (<), (>)) +import qualified Prelude +import Text.Read (readMaybe) + +-- External imports: Copilot +import qualified Copilot.Core as Core +import Copilot.Interpret.Eval (ShowType (Haskell), eval) +import Copilot.Language hiding (interpret, typeOf) +import Copilot.Visualize.UntypedTrace (AppData, makeTraceEval) + +-- Internal imports +import Copilot.Visualize.Dynamic + +-- | Start a simulation for an input spec, listening for commands and +-- communicating the status via a websocket. +visualize :: String -> IO () +visualize = visualizeWith mkDefaultVisualSettings + +-- | Start a simulation for an input spec, listening for commands and +-- communicating the status via a websocket. +visualizeWith :: VisualSettings -> String -> IO () +visualizeWith settings spec = do + putStrLn $ concat + [ "WebSocket server starting on port " + , show (visualSettingsPort settings) + , "..." + ] + WS.runServer + (visualSettingsHost settings) + (visualSettingsPort settings) + (app settings spec) + +-- | Settings used to customize the simulation and interaction. +data VisualSettings = VisualSettings + { visualSettingsHost :: String + -- ^ Host interface to listen to. Use + -- "127.0.0.1" to listen at localhost. + + , visualSettingsPort :: Int + -- ^ Port to listen to. + + , visualSettingsSimulation :: SimulationSettings + -- ^ Settings for the simulation. + } + +-- | Default settings that simulates 3 steps and listens on localhost at port +-- 9160. +mkDefaultVisualSettings :: VisualSettings +mkDefaultVisualSettings = VisualSettings + { visualSettingsHost = "127.0.0.1" + , visualSettingsPort = 9160 + , visualSettingsSimulation = mkDefaultSimulationSettings + } + +-- * Server + +-- | Server application using web sockets. +app :: VisualSettings -> String -> WS.ServerApp +app settings spec pending = do + conn <- WS.acceptRequest pending + WS.withPingThread conn 30 (return ()) $ appInit settings spec conn + +-- | Initialize the backend. +appInit :: VisualSettings -> String -> WS.Connection -> IO () +appInit settings spec conn = handle appException $ do + -- Initialize the simulation. + simData <- simInit (visualSettingsSimulation settings) spec + + -- Communicate the current values of the trace, in JSON, via the web + -- socket. + let appData = mkAppData (simSteps simData) (simSpec simData) + let samples = encode $ toJSON appData + WS.sendTextData conn samples + + -- Start the application loop. + appMainLoop settings conn simData + + where + + appException :: SomeException -> IO () + appException e = do + putStrLn $ "Error:" Prelude.++ show e + error $ show e + +-- | Run the main application, repeatedly reading commands from a web socket +-- and returning results via the same web socket. +appMainLoop :: VisualSettings + -> WS.Connection + -> SimData + -> IO () +appMainLoop settings conn simData = do + -- Read a command from the web socket. + cmdM <- readMaybe . T.unpack <$> WS.receiveData conn + + -- Run a simulation step, if a command has been received. + let simulationSettings = visualSettingsSimulation settings + simData' <- maybe (pure simData) (simStep simulationSettings simData) cmdM + + -- Communicate the current values of the trace, in JSON, via the web socket. + let appData = mkAppData (simSteps simData') (simSpec simData') + samples = encode $ toJSON appData + WS.sendTextData conn samples + + appMainLoop settings conn simData' + +-- * Auxiliary functions + +-- | Obtain the trace data from a Copilot spec for a number of steps. +mkAppData :: Int -> Core.Spec -> AppData +mkAppData numSteps spec' = + makeTraceEval numSteps spec' (eval Haskell numSteps spec') diff --git a/src/Copilot/Visualize/Static.hs b/src/Copilot/Visualize/Static.hs new file mode 100644 index 0000000..bfe5f34 --- /dev/null +++ b/src/Copilot/Visualize/Static.hs @@ -0,0 +1,36 @@ +-- | +-- Copyright : (c) NASA, 2024-2025 +-- License : BSD-style (see the LICENSE file in the distribution) +-- +-- Produce a visual representation of a Copilot specification. +module Copilot.Visualize.Static + ( visualize + ) + where + +-- External imports +import Data.Aeson (ToJSON (..)) +import System.Directory.Extra (copyTemplate) +import System.FilePath (()) + +-- External imports: Copilot +import Copilot.Core (Spec (..)) +import Copilot.Interpret.Eval (ShowType (Haskell), eval) + +-- Internal imports +import Copilot.Visualize.UntypedTrace (makeTraceEval) +import Paths_copilot_visualizer (getDataDir) + +-- | Produce a visual representation of a Copilot specification, for a given +-- number of steps, using a template. +visualize :: Int -- ^ Number of steps to interpret. + -> Spec -- ^ Specification to interpret. + -> String -- ^ Base used to expand the static file (i.e., @"tikz"@, + -- @"static_html"@). + -> FilePath + -> IO () +visualize k spec base target = do + dir <- getDataDir + let f = dir "data" base + let subs = toJSON $ makeTraceEval k spec $ eval Haskell k spec + copyTemplate f subs target diff --git a/src/Copilot/Visualize/TypedTrace.hs b/src/Copilot/Visualize/TypedTrace.hs new file mode 100644 index 0000000..901f428 --- /dev/null +++ b/src/Copilot/Visualize/TypedTrace.hs @@ -0,0 +1,158 @@ +{-# LANGUAGE GADTs #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE ScopedTypeVariables #-} +-- | +-- Copyright : (c) NASA, 2024-2025 +-- License : BSD-style (see the LICENSE file in the distribution) +-- +-- Read and modify traces of specifications. +-- +-- In the context of this module, a trace refers only to the values of +-- externs, since the state of a spec can be reproduced if the values of +-- externs are known. +module Copilot.Visualize.TypedTrace + ( extractTrace + , updateWithTrace + , Trace(..) + , UValues(..) + ) + where + +-- External imports +import Data.List hiding ((++)) +import Data.Maybe (fromMaybe) +import qualified Data.Type.Equality as DE +import Data.Typeable (Typeable) +import Prelude hiding (div, not, (++), (<), (>)) + +-- External imports: Copilot +import qualified Copilot.Core as Core +import Language.Copilot hiding (interpret, typeOf) + +-- | Map stream names to their values. +newtype Trace = Trace + { traceMap :: [ (String, UValues) ] + } + +-- | Existentially typed list of values of a stream. +data UValues = forall a . Typeable a => UValues + { uvType :: Core.Type a + , uvValues :: [ a ] + } + +-- | Extract a trace from a core specification. +extractTrace :: Core.Spec -> Trace +extractTrace spec = Trace $ concat $ concat + [ fmap extractTraceStream (Core.specStreams spec) + , fmap extractTraceObserver (Core.specObservers spec) + , fmap extractTraceTrigger (Core.specTriggers spec) + ] + +-- | Extract the values of a core 'Stream'. +extractTraceStream :: Core.Stream -> [ (String, UValues) ] +extractTraceStream (Core.Stream _id _buf expr _ty) = + extractTraceExpr expr + +-- | Extract the values of a core 'Observer'. +extractTraceObserver :: Core.Observer -> [ (String, UValues) ] +extractTraceObserver (Core.Observer _name expr _ty) = + extractTraceExpr expr + +-- | Extract the values of a core 'Trigger'. +extractTraceTrigger :: Core.Trigger -> [ (String, UValues) ] +extractTraceTrigger (Core.Trigger _name expr args) = concat $ + extractTraceExpr expr + : fmap extractTraceUExpr args + +-- | Extract the values of a core 'Expr'. +extractTraceExpr :: Core.Expr a -> [ (String, UValues) ] +extractTraceExpr (Core.Local _ _ _ expr1 expr2) = concat + [ extractTraceExpr expr1 + , extractTraceExpr expr2 + ] +extractTraceExpr (Core.ExternVar ty name values) = + [ (name, UValues ty (fromMaybe [] values)) ] +extractTraceExpr (Core.Op1 _op expr) = + extractTraceExpr expr +extractTraceExpr (Core.Op2 _op expr1 expr2) = concat + [ extractTraceExpr expr1 + , extractTraceExpr expr2 + ] +extractTraceExpr (Core.Op3 _op expr1 expr2 expr3) = concat + [ extractTraceExpr expr1 + , extractTraceExpr expr2 + , extractTraceExpr expr3 + ] +extractTraceExpr (Core.Label _ty _lbl expr) = + extractTraceExpr expr +extractTraceExpr _ = [] + +-- | Extract the values of a core 'UExpr'. +extractTraceUExpr :: Core.UExpr -> [ (String, UValues) ] +extractTraceUExpr (Core.UExpr ty expr) = extractTraceExpr expr + +-- | Update externs in a spec. +updateWithTrace :: Trace -> Core.Spec -> Core.Spec +updateWithTrace trace spec = spec + { Core.specStreams = + fmap (updateWithTraceStream trace) (Core.specStreams spec) + , Core.specObservers = + fmap (updateWithTraceObserver trace) (Core.specObservers spec) + , Core.specTriggers = + fmap (updateWithTraceTrigger trace) (Core.specTriggers spec) + } + +-- | Update the values of a 'Stream' based on an input trace. +updateWithTraceStream :: Trace -> Core.Stream -> Core.Stream +updateWithTraceStream trace (Core.Stream ident buf expr ty) = + Core.Stream ident buf (updateWithTraceExpr trace expr) ty + +-- | Update the values of an 'Observer' based on an input trace. +updateWithTraceObserver :: Trace -> Core.Observer -> Core.Observer +updateWithTraceObserver trace (Core.Observer name expr ty) = + Core.Observer name (updateWithTraceExpr trace expr) ty + +-- | Update the values of a 'Trigger' based on an input trace. +updateWithTraceTrigger :: Trace -> Core.Trigger -> Core.Trigger +updateWithTraceTrigger trace (Core.Trigger name expr args) = + Core.Trigger + name + (updateWithTraceExpr trace expr) + (fmap (updateWithTraceUExpr trace) args) + +-- | Update the values of an 'Expr' based on an input trace. +updateWithTraceExpr :: Trace -> Core.Expr a -> Core.Expr a +updateWithTraceExpr trace (Core.Local ty1 ty2 name expr1 expr2) = + Core.Local + ty1 + ty2 + name + (updateWithTraceExpr trace expr1) + (updateWithTraceExpr trace expr2) +updateWithTraceExpr trace (Core.ExternVar ty name values) = + Core.ExternVar ty name values' + where + values' | Just (UValues ty2 vals) <- lookup name (traceMap trace) + , Just DE.Refl <- DE.testEquality ty ty2 + = Just vals + | otherwise + = values +updateWithTraceExpr trace (Core.Op1 op expr) = + Core.Op1 op (updateWithTraceExpr trace expr) +updateWithTraceExpr trace (Core.Op2 op expr1 expr2) = + Core.Op2 op + (updateWithTraceExpr trace expr1) + (updateWithTraceExpr trace expr2) +updateWithTraceExpr trace (Core.Op3 op expr1 expr2 expr3) = + Core.Op3 op + (updateWithTraceExpr trace expr1) + (updateWithTraceExpr trace expr2) + (updateWithTraceExpr trace expr3) +updateWithTraceExpr trace (Core.Label ty lbl expr) = + Core.Label ty lbl (updateWithTraceExpr trace expr) +updateWithTraceExpr trace x = x + +-- | Update the values of a 'UExpr' based on an input trace. +updateWithTraceUExpr :: Trace -> Core.UExpr -> Core.UExpr +updateWithTraceUExpr trace (Core.UExpr ty expr) = + Core.UExpr ty (updateWithTraceExpr trace expr) diff --git a/src/Copilot/Visualize/UntypedTrace.hs b/src/Copilot/Visualize/UntypedTrace.hs new file mode 100644 index 0000000..6bbc836 --- /dev/null +++ b/src/Copilot/Visualize/UntypedTrace.hs @@ -0,0 +1,176 @@ +{-# LANGUAGE DeriveGeneric #-} +-- | +-- Copyright : (c) NASA, 2024-2025 +-- License : BSD-style (see the LICENSE file in the distribution) +-- +-- Abstract representation of a trace as a series named streams with their +-- values, together with functions needed to convert a 'Spec' into a trace. +-- +-- This trace is flat (untyped). Information about the types is captured +-- using boolean flags. This kind of trace is most useful to render values +-- on in logicless templates, since they don't have the capability to examine +-- the Haskell types. +module Copilot.Visualize.UntypedTrace + ( AppData(..) + , Trace + , TraceElem(..) + , TraceValue(..) + , makeTraceEval + ) + where + +-- External imports +import Data.Aeson (ToJSON (..)) +import Data.Bifunctor (second) +import Data.List (find, transpose) +import Data.Maybe (isJust, isNothing) +import GHC.Generics (Generic) +import Text.Printf (printf) +import Text.Read (readMaybe) + +-- External imports: Copilot +import Copilot.Core (Spec (..), triggerArgs, triggerName) +import Copilot.Interpret.Eval (ExecTrace, Output, interpObservers, + interpTriggers) + +-- * Abstract representation of a trace + +-- | Data related to a specification. +data AppData = AppData + { adTraceElems :: Trace + , adLastSample :: Int + } + deriving (Generic, Show) + +instance ToJSON AppData + +-- | A trace, defined by a list of trace elements, each defining a stream (in +-- an abstract sense). +type Trace = [ TraceElem ] + +-- | An element of a trace, or stream, with a name, its values, and information +-- about its type, needed to render it correctly. +data TraceElem = TraceElem + { teName :: String + , teIsBoolean :: Bool + , teIsFloat :: Bool + , teValues :: [ TraceValue ] + } + deriving (Generic, Show) + +instance ToJSON TraceElem + +-- | An individual sample, with a value and an indication of whether the sample +-- exists. +data TraceValue = TraceValue + { tvValue :: String + , tvIsEmpty :: Bool + } + deriving (Generic, Show) + +instance ToJSON TraceValue + +-- | Generate an abstract representation of a trace of a specification +-- interpreted for a given number of steps. +makeTraceEval :: Int + -> Spec + -> ExecTrace + -> AppData +makeTraceEval k spec e = + AppData (observerTEs ++ triggerTEs) (k - 1) + where + observerTEs = map mkTraceElem (interpObserversOpt spec e) + triggerTEs = map mkTraceElem (interpTriggersWithArgs spec e) + +-- | Generate an element of a trace from a stream name and its values over +-- time. +mkTraceElem :: (String, [Maybe Output]) -> TraceElem +mkTraceElem (name, outputs) = TraceElem + { teName = name + , teValues = values + , teIsBoolean = any (isBoolean . tvValue) values + , teIsFloat = any (isFloat . tvValue) values + } + where + values = map mkTraceValue outputs + +-- | Generate an individual value (sample) of a trace. +mkTraceValue :: Maybe Output -> TraceValue +mkTraceValue x = TraceValue (showValue x) (isNothing x) + +-- * Auxiliary functions + +-- | Compute the list of values associated to observers. +interpObserversOpt :: Spec -> ExecTrace -> [(String, [Maybe Output])] +interpObserversOpt _spec = map (second (map Just)) . interpObservers + +-- | Compute the list of values associated to triggers and their arguments. +-- +-- For each trigger, we first include the values of the trigger itself, and +-- then the values of the arguments to the trigger. +interpTriggersWithArgs :: Spec -> ExecTrace -> [(String, [Maybe Output])] +interpTriggersWithArgs spec = concatMap triggerOutputs . interpTriggers + where + -- This function adds one more output for the trigger itself. + triggerOutputs :: (String, [Maybe [Output]]) -> [(String, [Maybe Output])] + triggerOutputs (triggerName, triggerArgs) = + (triggerName, triggerValues) : zip argNames argValues + where + triggerValues = map triggerValue triggerArgs + + -- Value for the trigger at a given time, based on the values of its + -- arguments. + triggerValue :: Maybe [Output] -> Maybe Output + triggerValue Nothing = Just "false" + triggerValue (Just _) = Just "true" + + -- Names and values for the arguments. + argNames = map (\ix -> triggerName ++ "Arg" ++ show ix) [0..] + argValues = transpose (transMaybes numArgs triggerArgs) + numArgs = triggerNumArgs spec triggerName + +-- Number of arguments to a trigger in a spec. +-- +-- PRE: name exists as a trigger in spec. +triggerNumArgs :: Spec -> String -> Int +triggerNumArgs spec name = + case find (\t -> triggerName t == name) (specTriggers spec) of + Nothing -> error "Couldn't find given trigger in spec, should never occur!" + Just t -> length $ triggerArgs t + +-- | True if the input value denotes a boolean value. +isBoolean :: String -> Bool +isBoolean "true" = True +isBoolean "false" = True +isBoolean _ = False + +-- | True if the input value denotes a floating point value. +isFloat :: String -> Bool +isFloat s = isJust asInt || isJust asFloat + where + asInt :: Maybe Int + asInt = readMaybe s + + asFloat :: Maybe Float + asFloat = readMaybe s + +-- | Show a value. +showValue :: Maybe Output -> String +showValue Nothing = "--" +showValue (Just s) | isFloat s = showValueFloat s + | otherwise = s + +-- | Show a floating point value. +showValueFloat :: Output -> String +showValueFloat = formatFloat . read + where + formatFloat :: Double -> String + formatFloat = printf "%.2g" + +-- | Given a list of maybe lists of known length, this function creates a list +-- of lists, pushing the Maybe's inside. +transMaybes :: Int -> [Maybe [a]] -> [[Maybe a]] +transMaybes = map . transMaybes' + where + transMaybes' argsLength (Just xs) = map Just xs + transMaybes' argsLength Nothing = replicate argsLength Nothing From eedbe96f8d082f7c78ac53467c8a07a014001e5b Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Fri, 27 Jun 2025 06:14:52 -0700 Subject: [PATCH 2/3] Document changes in CHANGELOG. Refs #4. --- CHANGELOG | 2 ++ 1 file changed, 2 insertions(+) diff --git a/CHANGELOG b/CHANGELOG index e69de29..c902a6e 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -0,0 +1,2 @@ +2025-06-26 + * Initial version. (#4) From 3c0674fd5948572d4d29a3affa0bc3e99547c1fb Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Fri, 27 Jun 2025 06:20:01 -0700 Subject: [PATCH 3/3] Document changes in CHANGELOG. Refs #5. --- CHANGELOG | 1 + 1 file changed, 1 insertion(+) diff --git a/CHANGELOG b/CHANGELOG index c902a6e..44cb9f0 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -1,2 +1,3 @@ 2025-06-26 + * Release 4.4. (#5) * Initial version. (#4)