BMSTU/02-iskr-lab-04-report.tex

216 lines
10 KiB
TeX
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

\documentclass[a4paper,fontsize=14bp]{article}
\input{../common-preamble}
\input{../fancy-listings-preamble}
\input{../bmstu-preamble}
\numerationTop
\begin{document}
\thispagestyle{empty}
\makeBMSTUHeader
% ... работе, номер, тема, предмет, ?а, кто
\makeReportTitle{лабораторной}{4}{Исчисление дискретных событий}{Представление знаний в информационных системах}{}{И.И. Лычков}
\newpage
\thispagestyle{empty}
\tableofcontents
\newpage
\pagestyle{fancy}
\section{Цель}
Получение практических навыков моделирования дискретно-событийных систем на языке логического программирования.
\section{Задание}
В качестве исходных данных выдается словесное описание некоторой физической системы, а именно: общие правила её функционирования, состояние системы в начальный момент, список произошедших событий и вопрос относительно состояния одного из объектов системы в определенный момент времени. Также выдаются аксиомы исчисления дискретных событий. Требуется выделить в исходном описании все объекты, события, флюенты, придумать для них идентификаторы в программе, затем представить логику функционирования заданной системы в виде программы на языке ASP программирования наборов решений с помощью аксиом исчисления дискретных событий, отладить работу программы так, чтобы она выдавала ответ на указанный в задании вопрос относительно состояния одного из объектов системы в определенный момент времени.
\section{Выполнение}
\subsection{Словесное описание системы согласно варианту}
Имеется две аксиомы initiates и terminates. Если агент включает нагреватель воздушного шара, то нагреватель более не будет выключен и будет включен. Мы задаем глобальное ограничение о том, что воздушный шар не может находиться одновременно на двух разных высотах в один момент времени.
Когда нагреватель включен, высота воздушного шара изменяется по закону:
\[h(t) = h(0) + V*t\]
Когда нагреватель выключен, высота воздушного шара изменяется по закону:
\[h(t) = h(0) - V*t,\]
где V = 1 - скорость воздушного шара (задана константой)
Высота воздушного шара освобождается от закона инерции по событиям включения и выключения нагревателя. Имеем следующие факты и хронику событий. Воздушный шар изначально находится на нулевой высоте. В момент времени 1 нагреватель включают, а в момент времени 3 нагреватель выключают. Необходимо проверить, что в момент времени 3 высота воздушного шара равна 2V, а в момент времени 4 она равна V.
\subsection{Перечень всех объектов, событий и флюентов с указанием их идентификаторов и смысловой нагрузки}
События и флюенты в программе:
\begin{itemize}
\item \verb|turnOn| - событие включения нагревателя;
\item \verb|turnOff| - событие выключения нагревателя;
\item \verb|heating| - флюент, говорящий о том, что шар нагревается и летит вверх;
\item \verb|falling| - флюент, говорящий о том, что шар охлаждается и падает;
\item \verb|height(X)| - флюент, говорящий о текущей высоте шара.
\end{itemize}
Имеется две аксиомы initiates и terminates.
\begin{verbatim}
initiates(turnOn, heating, Time) :- times(Time).
terminates(turnOff, heating, Time) :- times(Time).
initiates(turnOff, falling, Time) :- times(Time).
terminates(turnOn, falling, Time) :- times(Time).
\end{verbatim}
Мы задаем глобальное ограничение о том, что воздушный шар не может находиться одновременно на двух разных высотах в один момент времени.
\begin{verbatim}
:- holdsAt(height(X1), T), holdsAt(height(X2), T), X1 != X2.
\end{verbatim}
Имеем две аксиомы типа trajectory, описывающие поведение шара при нагревании и охлаждении:
\begin{verbatim}
trajectory(heating, T1, height(X2), T2) :-
times(T1), times(T2), T1 < T2,
holdsAt(height(X),T1),
X2 = X + 1 * (T2 - T1).
trajectory(falling, T1, height(X2), T2) :-
times(T1), times(T2), T1 < T2,
holdsAt(height(X),T1),
X2 = X - 1 * (T2 - T1).
\end{verbatim}
Высота воздушного шара освобождается от закона инерции по событиям включения и выключения нагревателя:
\begin{verbatim}
releases(turnOff, height(X), T) :- holdsAt(height(X), T).
releases(turnOn, height(X), T) :- holdsAt(height(X), T).
\end{verbatim}
Имеем следующие факты и хронику событий. Воздушный шар изначально находится на нулевой высоте, в момент времени 1 нагреватель включают, а в момент времени 3 нагреватель выключают:
\begin{verbatim}
initiallyP(height(0)).
initiallyN(heating).
happens(turnOn, 1).
happens(turnOff, 3).
\end{verbatim}
Необходимо проверить, что в момент времени 3 высота воздушного шара равна 2V, а в момент времени 4 она равна V.
\begin{verbatim}
info(F1, T1, F2, T2) :-
holdsAt(height(F1), T1), holdsAt(height(F2), T2),
F1==2, T1==3, F2 == 1, T2 == 4.
#show info/4.
\end{verbatim}
\subsection{Результат выполнение программы}
Результат выполнения программы представлен на рисунке \hrf{pic:result}.
\begin{figure}[H]
\centering
\includegraphics[height=6cm]{04-lab-result.png}
\caption{Результаты работы программы}
\label{pic:result}
\end{figure}
На рисунке \hrf{pic:result} видно, что программа нашла одно сочетание флюентов и временных отметок: в момент времени 3 высота воздушного шара равна 2, а в момент времени 4 она равна 1.
\newpage
\appendix
\setcounter{secnumdepth}{0}
\section*{Приложения}
\addcontentsline{toc}{section}{Приложения}
\renewcommand{\thesubsection}{\Alph{subsection}}
\setcounter{secnumdepth}{5}
\subsection{Полный листинг приложения по индивидуальному заданию}
\begin{lstlisting}[language=C,style=CCodeStyle]
%*
********************************************************************
Стандартные аксиомы исчисления дискретных событий.
********************************************************************
*%
%% BEC1 - StoppedIn(t1,f,t2)
stoppedIn(T1,Fluent,T2) :-
times(T1), times(T2), T1<T2,
terminates(Event,Fluent,T),
happens(Event,T), T1<T, T<T2.
stoppedIn(T1,Fluent,T2) :-
times(T1), times(T2), T1<T2,
releases(Event,Fluent,T),
happens(Event,T), T1<T, T<T2.
%% BEC2 - StartedIn(t1,f,t2)
startedIn(T1,Fluent,T2) :-
times(T1), times(T2), T1<T2,
initiates(Event,Fluent,T),
happens(Event,T), T1<T, T<T2.
startedIn(T1,Fluent,T2) :-
times(T1), times(T2), T1<T2,
releases(Event,Fluent,T),
happens(Event,T), T1<T, T<T2.
%% BEC3 - HoldsAt(f,t)
holdsAt(Fluent2,T2) :-
times(T1),
happens(Event,T1),
initiates(Event,Fluent1,T1),
trajectory(Fluent1,T1,Fluent2,T2),
not stoppedIn(T1,Fluent1,T2).
%% BEC4 - HoldsAt(f,t)
holdsAt(Fluent,T) :-
times(T),
initiallyP(Fluent),
not stoppedIn(0,Fluent,T).
%% BEC5 - not HoldsAt(f,t)
-holdsAt(Fluent,T):-
times(T),
initiallyN(Fluent),
not startedIn(0,Fluent,T).
%% BEC6 - HoldsAt(f,t)
holdsAt(Fluent,T) :-
times(T),
happens(Event,T1),
initiates(Event,Fluent,T1), T1<T,
not stoppedIn(T1,Fluent,T).
%% BEC7 - not HoldsAt(f,t)
-holdsAt(Fluent,T):-
times(T),
happens(Event,T1),
terminates(Event,Fluent,T1), T1<T,
not startedIn(T1,Fluent,T).
times(0..5).
initiates(turnOn, heating, Time) :- times(Time).
terminates(turnOff, heating, Time) :- times(Time).
initiates(turnOff, falling, Time) :- times(Time).
terminates(turnOn, falling, Time) :- times(Time).
releases(turnOff, height(X), Time) :- holdsAt(height(X), Time).
releases(turnOn, height(X), Time) :- holdsAt(height(X), Time).
trajectory(heating, T1, height(X2), T2) :-
times(T1), times(T2), T1 < T2,
holdsAt(height(X),T1),
X2 = X + 1 * (T2 - T1).
trajectory(falling, T1, height(X2), T2) :-
times(T1), times(T2), T1 < T2,
holdsAt(height(X),T1),
X2 = X - 1 * (T2 - T1).
:- holdsAt(height(X1), T), holdsAt(height(X2), T), X1 != X2.
releases(turnOn, heating, Time) :- times(Time).
releases(turnOff, heating, Time) :- times(Time).
initiallyP(height(0)).
initiallyN(heating).
happens(turnOn, 1).
happens(turnOff, 3).
info(F1, T1, F2, T2) :- holdsAt(height(F1), T1), holdsAt(height(F2), T2), F1==2, T1==3, F2 == 1, T2 == 4.
#show info/4.
\end{lstlisting}
\end{document}