\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}

