goals.tex revision bb1a72b84b087ebe2aae9e73ecf3caaefcb8a206
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder% Ligatur-Problem (z.b. bei specific wird aus dem fi eine ligatur
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder% gemacht, danach nicht mehr suchbar im acrobat-reader) wird mit
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder% diesem Eintrag behoben. Toll!
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder%%%%%%%%%%%%%%%%%%%%%%%%%%
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian Maeder\RequirePackage{ifpdf}
b4fbc96e05117839ca409f5f20f97b3ac872d1edTill Mossakowski\RequirePackage{cmap}% Improve PDF text search.
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder%%%%%%%%%%%%%%%%%%%%%%%%%%
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder\documentclass[11pt,draft,a4paper]{article}%{scrartcl}%{report}
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder\usepackage{xspace}
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder\usepackage{amsmath}
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder\newcommand{\freecad}{FreeCAD\xspace}
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder\newcommand{\opencasc}{Open CASCADE\xspace}
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder\newcommand{\hets}{Hets\xspace}
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder\newcommand{\bash}[1]{{\tt #1}}
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder\newcommand{\haskell}[1]{{\tt #1}}
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder\newcommand{\setsep}[2]{\{#1~|~#2\}}
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder\newcommand{\leftsem}{[\![} %%
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder\newcommand{\rightsem}{]\!]} %%
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder\newcommand{\setsem}[1]{\leftsem #1 \rightsem} %% set semantics
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder\begin{document}
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder\title{Internship Goals for Robert Savu}
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder\author{Ewaryst Schulz}
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder\section{Reading \freecad documents}
9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaederGiven a document containing a \freecad design (typically a *.fcstd-file) we want to import it into \hets. This requires the following:
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder\begin{description}
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder \item[Abstract Syntax:] an appropriate representation in \hets for \freecad designs,
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder i.e., the \freecad abstract syntax (mostly done)
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder \item[Semantics:] \freecad terms should have a semantics in the sense of 3D Pointsets (see section \ref{sec:semantics})
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder \item[Import:] an import method translating \freecad documents into this
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder representation (partly done, has to be integrated into one method)
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder \item[\hets Integration:] a complete integration of the \freecad logic into the \hets
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder logic-graph (partly done, signature and simple static analysis missing)
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder \item[\hets tool:] a hook into the hets program to open \freecad documents from there, i.e., \bash{hets -g test.fcstd} should work
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder \item[Pretty printing] for basic \freecad specs, i.e.,
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder \haskell{Pretty}-instances for the \freecad abstract syntax
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder\end{description}
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder\subsection{Semantics}
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder\label{sec:semantics}
9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaederWe first give the semantics of some base objects such as rectangles,
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederboxes, and cylinders. The goal is to specify the semantics for each of
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederthe base objects used in the abstract syntax of \freecad and also for
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederthe transformation by rotations and translations as well as for
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maedercompound objects such as \haskell{Cut}, \haskell{Common},
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder\haskell{Fusion}, etc..
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder\setsem{Rectangle(w, l)} & = \text{The set consisting of the four sides of the }\notag\\
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder & \qquad \text{rectangle in the x-y-plane}\notag\\
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder & = \setsep{(x,y,0)}{x\in[0,l], y\in\{0,w\}}\notag\\
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder & \quad \cup \setsep{(x,y,0)}{x\in\{0,l\}, y\in[0,w]}\\
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder\setsem{Box(h, l, w)} & = \text{The solid bounded by the faces of the box}\notag\\
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder & = [0,l]\times[0,w]\times[0,h]\\
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder\setsem{Cylinder(a, h, r)} & = \text{The ``pac-man'' cylinder along z-axis}\notag\\
2eb84fc82d3ffa9116bc471fda3742bd9e5a24bbChristian Maeder & = circle\times[0,h]\\
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder \text{where}~ circle &=\setsep{(\rho\cdot cos(\alpha),\rho\cdot sin(\alpha))}{\alpha \in [0,a], \rho \in [0,r]}\notag\\
2eb84fc82d3ffa9116bc471fda3742bd9e5a24bbChristian Maeder\setsem{Sphere(a_1, a_2, a_3, r)} & = \text{The intersection between a full sphere and a 'pac-man' cylinder}\notag\\
2eb84fc82d3ffa9116bc471fda3742bd9e5a24bbChristian Maeder& \text {on the z-axis (which may cut a 'cake-slice' and also the nort-pole/south-pole caps)}\notag\\
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski& = \setsep{(x,y,z)}{x + y + z \leq r} \cap \notag\\
35db0960aa2e2a13652381c756fae5fb2b27213bChristian Maeder& \setsep{(\rho\cdot cos(\alpha),\rho\cdot sin(\alpha),z)}{z \in [sin(a_1),sin(a_2)]. \rho \in [0, \infty], \alpha \in [0, a_3]}\\
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder\setsem{Cone(a, r_1, r_2, h)} & = \text{The intersection between a fullright circular cone and a 'pac-man' cylinder}\notag\\
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski& = \setsep{(\rho \cdot cos(\alpha), \rho \cdot sin(\alpha), z)}{\rho \leq r_1 + {{z}\over{h}} \cdot (r_2 - r_1). z \in [0,h],\alpha \in [0, a]} \\
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder\setsem{Torus(a_1, a_2, a_3, r_1, r_2)} & = \text{a bit trickier: union between a torus and a cylinder with the same center and the}\notag\\
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder& \text {same symmetry axis all intersected with an infinite-radius z-axis centered 'pac-man' cylinder}\notag\\
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder& = \{(x,y,z)\} \cup \{(x_2,y_2,z_2)\}\notag\\
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder& \text{where:}\notag\\
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder& circle = \setsep{(\rho\cdot cos(\alpha), \rho\cdot sin(\alpha))}{\alpha \in [a_1, a_2], \rho \in [0,r_2]}\notag\\
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder& (rad, z) \in \setsep{(m,n)}{(-(m-r_1), n)\in circle}\notag\\
7325bbe03797fd413af504fb3fac109b2c652a7bChristian Maeder& x = rad\cdot cos (ang) \notag\\
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder& y = rad\cdot sin (ang) \notag\\
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder& ang \in [0, a_3] \notag\\
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder& \text{if } (a_1 \geq -180) \text{or} (a_2 \leq 180) \text {then} \notag\\
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder& (x_2,y_2,z_2 - r_2 \cdot sin(a_1)) \in \notag\\
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder&\setsem{Cone(a_3, r_1 - r_2 \cdot cos(a_1), r_1 - r_2 \cdot cos(a_2), sin(a_2) - sin(a_1))}\\
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder\setsem{Circle(sa, ea, r)} & = \setsep{(x,y,z)}{x = r\cdot cos(\alpha), y = r \cdot sin(\alpha), z = 0, \alpha \in [sa, ea]}\\
083679daeba30fce9d60f7170a2cfd9f9c80bfb2Till Mossakowski\end{document}